Lab 2

# JPF site configuration
jpf-core=/eecs/fac/pkg/jpf/jpf-core
extensions=${jpf-core}
import java.util.Random;
 
public class RandomFraction {
  public static void run() {
    Random random = new Random(System.currentTimeMillis());
    System.out.println(1 / random.nextInt(1000000));
  }
}
public class RandomFractionTest {
  public static void main(String[] args) {
    RandomFraction.run();
  }
}
target=RandomFractionTest
classpath=.
jpf RandomFractionTest.jpf

It should produce output similar to the following.

JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
RandomFractionTest.main()

====================================================== search started: 1/14/17 12:06 PM
0
====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=1,end=1
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=353,released=12,maxLive=0,gcCycles=1
instructions:       3181
max memory:         299MB
loaded code:        classes=62,methods=1334

====================================================== search finished: 1/14/17 12:06 PM
cg.enumerate_random=true
JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
RandomFractionTest.main()

====================================================== search started: 1/14/17 12:19 PM

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: division by zero
        at RandomFraction.run(RandomFraction.java:8)
        at RandomFractionTest.main(RandomFractionTest.java:5)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
        at RandomFraction.run(RandomFraction.java:8)
        at RandomFractionTest.main(RandomFractionTest.java:5)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArithmeticException: division by zero  a..."

====================================================== statistics
elapsed time:       00:00:00
states:             new=2,visited=0,backtracked=0,end=0
search:             maxDepth=2,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=1
heap:               new=369,released=2,maxLive=0,gcCycles=1
instructions:       3175
max memory:         299MB
loaded code:        classes=66,methods=1364

====================================================== search finished: 1/14/17 12:19 PM