EECS4315

This is an old revision of the document!

In your home directory create a directory named .jpf (note that the name of the directory starts with a dot).
In the created directory, create a file named site.properties with the following contents.

# JPF site configuration
jpf-core=/eecs/fac/pkg/jpf/jpf-core
extensions=${jpf-core}

In your home directory create a directory name 4315.
In the created directory 4315, create a directory named lab2.
In the created directory lab2, create the class RandomFraction with the following content.

import java.util.Random;
 
public class RandomFraction 
{
	public static void run() 
	{
		Random random = new Random(System.currentTimeMillis());
		System.out.println(1 / random.nextInt(1000000));
	}
}

Compile the RandomFraction class.
In the created directory lab2, create the class RandomFractionTest with the following content.

public class RandomFractionTest 
{
	public static void main(String[] args) 
	{
		RandomFraction.run();
	}
}

Compile the RandomFractionTest class.
Run the RandomFractionTest class.
Create the file RandomFractionTest.jpf with the following content.

target=RandomFractionTest
classpath=.

Run Java PathFinder (JPF) on RandomFractionTest by running

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

To the file RandomFractionTest.jpf add the following.

cg.enumerate_random=true

Run JPF on RandomFractionTest again. 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: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