Differences

This shows you the differences between two versions of the page.

--- lab2 [2017/01/13 19:56] – franck
+++ lab2 [2017/01/30 13:51] (current) – franck
@@ Line 1: / Line 1: @@
-TBA
+====== Lab 2 ======
+  * 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.
+<code>
+# JPF site configuration
+jpf-core=/eecs/fac/pkg/jpf/jpf-core
+extensions=${jpf-core}
+</code>
+  * 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.
+<code java>
+import java.util.Random;
+public class RandomFraction
+{
+	public static void run()
+	{
+		Random random = new Random(System.currentTimeMillis());
+		System.out.println(1 / random.nextInt(1000000));
+	}
+}
+</code>
+  * Compile the RandomFraction  class.
+  * In the created directory lab2, create the class RandomFractionTest with the following content.
+<code java>
+public class RandomFractionTest
+{
+	public static void main(String[] args)
+	{
+		RandomFraction.run();
+	}
+}
+</code>
+  * Compile the RandomFractionTest class.
+  * Run the RandomFractionTest class.
+  * Create the file RandomFractionTest.jpf with the following content.
+<code>
+target=RandomFractionTest
+classpath=.
+</code>
+  * Run Java PathFinder (JPF) on RandomFractionTest by running
+<code>
+jpf RandomFractionTest.jpf
+</code>
+It should produce output similar to the following.
+<code>
+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
+
+====================================================== 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
+</code>
+  * To the file RandomFractionTest.jpf add the following.
+<code>
+cg.enumerate_random=true
+</code>
+  * Run JPF on RandomFractionTest again.  It should produce output similar to the following.
+<code>
+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
+</code>