Differences

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

--- lab2 [2016/01/13 17:13] – franck
+++ lab2 [2018/01/02 22:03] (current) – franck
@@ Line 1: / Line 1: @@
-Read the notes.  Install Java PathFinder (JPF), either on your own machine or in your EECS account.  Create the HelloWorld example.  Run JPF on the example, both from the command line and from either Eclipse or NetBeans.  If you use your own machine, bring it to the lab on Thursday for the Quiz.
+====== 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>
-Bonus marks: for each mistake in the notes that is first reported by email before Saturday January 16, you receive 0.1 bonus mark, up to a maximum of 1.5 in total.  (The ?? following Chapter and Section are references to chapters and sections that have not yet been written.)