Mercurial > hg > Members > kono > jpf-core
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) ... ~~~~~~~~