~~NOTOC~~ ====== Lab 5 ====== Consider the following app. public class Main { public static void main(String[] args) { System.out.println(StrictMath.exp(23.7)); } } If we run JPF with the following configuration file target=Main classpath=(directory that contains Main.class) then we obtain output similar to the following. JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved. ====================================================== system under test Main.main() ====================================================== search started: 2/29/20 4:01 PM ====================================================== error 1 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty java.lang.UnsatisfiedLinkError: cannot find native java.lang.StrictMath.exp at java.lang.StrictMath.exp(gov.nasa.jpf.vm.JPF_java_lang_StrictMath) at Main.main(Main.java:3) ====================================================== snapshot #1 thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at java.lang.StrictMath.exp(StrictMath.java) at Main.main(Main.java:3) ====================================================== results error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: cannot find native..." ====================================================== statistics elapsed time: 00:00:00 states: new=1,visited=0,backtracked=0,end=0 search: maxDepth=1,constraints=0 choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0 heap: new=369,released=0,maxLive=0,gcCycles=0 instructions: 3182 max memory: 240MB loaded code: classes=66,methods=1427 ====================================================== search finished: 2/29/20 4:01 PM ===== Approach 1: native peer ===== Implement a native peer class. Add to the native peer a call to println with "native peer" so that JPF produces the following output for the above app. JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved. ====================================================== system under test Main.main() ====================================================== search started: 2/29/20 4:02 PM native peer 1.9623624323651344E10 ====================================================== 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=11,maxLive=0,gcCycles=1 instructions: 3189 max memory: 240MB loaded code: classes=62,methods=1399 ====================================================== search finished: 2/29/20 4:02 PM To compile your class, you may want to use javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. (class name).java or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse. Submit your native peer class **and** your configuration file (name it Main-native-peer.jpf). ===== Approach 2: peer ===== Implement a peer class. Add to the peer class a call to println with "peer" so that JPF produces output for the above app similar to the following. To model exp, you may want to use a [[https://en.wikipedia.org/wiki/Taylor_series|Taylor series]]. Ensure that the modelled exp method satisfies the specification given in the API of the StrictMath class. Some methods in the Double class might be useful. JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved. ====================================================== system under test Main.main() ====================================================== search started: 2/29/20 4:05 PM [WARNING] orphan NativePeer method: java.lang.StrictMath.log(D)D peer 1.9623624323651325E10 ====================================================== 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=355,released=11,maxLive=0,gcCycles=1 instructions: 5184 max memory: 240MB loaded code: classes=62,methods=1331 ====================================================== search finished: 2/29/20 4:05 PM Submit your peer class **and** your configuration file (name it Main-peer.jpf). ===== Approach 3: jpf-nhandler ===== Use jpf-nhandler so that JPF produces the following output. JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved. ====================================================== system under test Main.main() ====================================================== search started: 2/29/20 4:10 PM * DELEGATING Unhandled Native -> java.lang.StrictMath.exp 1.9623624323651344E10 ====================================================== 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=555,released=13,maxLive=0,gcCycles=1 instructions: 9955 max memory: 240MB loaded code: classes=62,methods=1399 ====================================================== search finished: 2/29/20 4:10 PM Submit your configuration file (name it Main-nhandler.jpf). To receive feedback, submit your classes and configuration files using submit 4315 lab5 (name of file) before Thursday March 12.