view doc/jpf-core/AssertionProperty.md @ 0:61d41facf527

initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
line wrap: on
line source

# 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 ###

~~~~~~~~ {.java}
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:

~~~~~~~~ {.bash}
>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 ###

~~~~~~~~ {.java}
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 

~~~~~~~~ {.bash}
>jpf +listener=.listener.AssertionProperty +ap.go_on GoOn
~~~~~~~~

Produces:

~~~~~~~~ {.bash}
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)
...
~~~~~~~~