doc/jpf-core/AssertionProperty.md

   1 # AssertionProperty #
   2
   3 This listener adds some special capabilities for `java.lang.AssertionError` processing:
   4
   5  * report `AssertionErrors` that are otherwise carelessly caught in `... catch (Throwable t) {..}` clauses
   6  * ignore AssertionErrors if `ap.go_on` is set
   7
   8 `AssertionErrors` differ a bit from other exceptions - they should never be handled, and they usually represent functional properties (as opposed to non-functionals like `NullPointerExceptions` and `ArithmeticExceptions`). Consequently, it can be regarded as an error if an `AssertionError` is swallowed by a 'catch-all', and it is at least an option to ignore an unhandled `AssertionError`, e.g. to see what non-functional defects - if any - it might cause downstream.
   9
  10 ### Example 1: catch-all ###
  11
  12 ~~~~~~~~ {.java}
  13 public class CatchAll {
  14   public static void main(String[] args){
  15     try {
  16       int d = 42;
  17       //.. some stuff
  18       assert d > 50 : "d below threshold";
  19       int x = d - 50;
  20       //.. some more stuff
  21     } catch (Throwable t) { // bad
  22       // ..I'm careless
  23     }
  24   }
  25 }
  26 ~~~~~~~~
  27
  28 Checked with:
  29
  30 ~~~~~~~~ {.bash}
  31 >jpf +listener=.listener.AssertionProperty CatchAll
  32 ~~~~~~~~
  33
  34 Produces:
  35
  36 ~~~~~~~~
  37 JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center
  38 ====================================================== system under test
  39 application: CatchAll.java
  40
  41 ====================================================== search started: 10/13/09 1:33 PM
  42
  43 ====================================================== error #1
  44 gov.nasa.jpf.listener.AssertionProperty
  45 d below threshold
  46 ...
  47 ~~~~~~~~
  48
  49
  50 ### Example 2: go-on ###
  51
  52 ~~~~~~~~ {.java}
  53 public class GoOn {
  54   public static void main (String[] args){
  55     int d = 42;
  56     // lots of computations...
  57     assert d > 50 : "d below threshold";
  58     int x = Math.max(0, d - 50);
  59     // lots of more computations...
  60     int y = 42000 / x;
  61   }
  62 }
  63 ~~~~~~~~
  64
  65 Checked with
  66
  67 ~~~~~~~~ {.bash}
  68 >jpf +listener=.listener.AssertionProperty +ap.go_on GoOn
  69 ~~~~~~~~
  70
  71 Produces:
  72
  73 ~~~~~~~~ {.bash}
  74 JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center
  75
  76 ====================================================== system under test
  77 application: GoOn.java
  78
  79 ====================================================== search started: 10/13/09 1:59 PM
  80 WARNING - AssertionError: d below threshold
  81         at GoOn.main(GoOn.java:5)
  82
  83 ====================================================== error #1
  84 gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
  85 java.lang.ArithmeticException: division by zero
  86         at GoOn.main(GoOn.java:8)
  87 ...
  88 ~~~~~~~~