AssertionProperty

AssertionProperty

This listener adds some special capabilities for java.lang.AssertionError processing:

• report AssertionErrors that are otherwise carelessly caught in ... catch (Throwable t) {..} clauses
• ignore AssertionErrors if ap.go_on is set

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.

Example 1: catch-all

public class CatchAll {
  public static void main(String[] args){
    try {
      int d = 42;
      //.. some stuff
      assert d > 50 : "d below threshold";
      int x = d - 50;
      //.. some more stuff
    } catch (Throwable t) { // bad
      // ..I'm careless
    }
  }
}

Checked with:

>jpf +listener=.listener.AssertionProperty CatchAll

Produces:

JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center
====================================================== system under test
application: CatchAll.java

====================================================== search started: 10/13/09 1:33 PM

====================================================== error #1
gov.nasa.jpf.listener.AssertionProperty
d below threshold
...

Example 2: go-on

public class GoOn {
  public static void main (String[] args){
    int d = 42;
    // lots of computations...
    assert d > 50 : "d below threshold";
    int x = Math.max(0, d - 50);
    // lots of more computations...
    int y = 42000 / x;
  }
}

Checked with

>jpf +listener=.listener.AssertionProperty +ap.go_on GoOn

Produces:

JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center

====================================================== system under test
application: GoOn.java

====================================================== search started: 10/13/09 1:59 PM
WARNING - AssertionError: d below threshold
	at GoOn.main(GoOn.java:5)

====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: division by zero
	at GoOn.main(GoOn.java:8)
...