lab8
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
lab8 [2018/02/25 14:58] – franck | lab8 [2020/02/29 21:15] (current) – franck | ||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Lab 6 ====== | + | ~~NOTOC~~ |
+ | |||
+ | ====== Lab 5 ====== | ||
Consider the following app. | Consider the following app. | ||
Line 5: | Line 7: | ||
public class Main { | public class Main { | ||
public static void main(String[] args) { | public static void main(String[] args) { | ||
- | | + | System.out.println(StrictMath.exp(23.7)); |
} | } | ||
} | } | ||
Line 17: | Line 19: | ||
then we obtain output similar to the following. | then we obtain output similar to the following. | ||
< | < | ||
- | JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved. | + | JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved. |
Line 23: | Line 25: | ||
Main.main() | Main.main() | ||
- | ====================================================== search started: | + | ====================================================== search started: |
====================================================== error 1 | ====================================================== error 1 | ||
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty | gov.nasa.jpf.vm.NoUncaughtExceptionsProperty | ||
- | java.lang.UnsatisfiedLinkError: | + | java.lang.UnsatisfiedLinkError: |
- | at java.lang.StrictMath.cbrt(no peer) | + | at java.lang.StrictMath.exp(gov.nasa.jpf.vm.JPF_java_lang_StrictMath) |
- | at Main.main(Main.java: | + | at Main.main(Main.java: |
- | ... | + | |
+ | |||
+ | ====================================================== snapshot #1 | ||
+ | thread java.lang.Thread: | ||
+ | call stack: | ||
+ | at java.lang.StrictMath.exp(StrictMath.java) | ||
+ | at Main.main(Main.java: | ||
+ | |||
+ | |||
+ | ====================================================== results | ||
+ | error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty " | ||
+ | |||
+ | ====================================================== statistics | ||
+ | elapsed time: | ||
+ | states: | ||
+ | search: | ||
+ | choice generators: | ||
+ | heap: | ||
+ | instructions: | ||
+ | max memory: | ||
+ | loaded code: classes=66, | ||
+ | |||
+ | ====================================================== search finished: 2/29/20 4:01 PM | ||
</ | </ | ||
- | * Implement a native peer class. | + | ===== Approach 1: native peer ===== |
- | JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved. | + | |
+ | Implement a native peer class. | ||
+ | |||
+ | < | ||
+ | JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved. | ||
Line 40: | Line 68: | ||
Main.main() | Main.main() | ||
- | ====================================================== search started: | + | ====================================================== search started: |
- | native peer class | + | native peer |
- | 1.6386425412012917 | + | 1.9623624323651344E10 |
====================================================== results | ====================================================== results | ||
no errors detected | no errors detected | ||
- | ... | + | |
- | </ | + | ====================================================== statistics |
- | | + | elapsed time: |
- | JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved. | + | states: |
+ | search: | ||
+ | choice generators: | ||
+ | heap: | ||
+ | instructions: | ||
+ | max memory: | ||
+ | loaded code: classes=62, | ||
+ | |||
+ | ====================================================== search finished: 2/29/20 4:02 PM | ||
+ | </ | ||
+ | |||
+ | To compile your class, you may want to use | ||
+ | < | ||
+ | javac -cp / | ||
+ | </ | ||
+ | or add / | ||
+ | |||
+ | Submit your native peer class **and** your configuration file (name it Main-native-peer.jpf). | ||
+ | |||
+ | ===== Approach 2: peer ===== | ||
+ | |||
+ | Implement a peer class. | ||
+ | |||
+ | < | ||
+ | JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved. | ||
Line 55: | Line 107: | ||
Main.main() | Main.main() | ||
- | ====================================================== search started: | + | ====================================================== search started: |
- | peer class | + | [WARNING] orphan NativePeer method: java.lang.StrictMath.log(D)D |
- | 1.6386425412012982 | + | peer |
+ | 1.9623624323651325E10 | ||
====================================================== results | ====================================================== results | ||
no errors detected | no errors detected | ||
- | ... | ||
- | </ | ||
- | To compile your classes, | + | ====================================================== statistics |
+ | elapsed time: | ||
+ | states: | ||
+ | search: | ||
+ | choice generators: | ||
+ | heap: | ||
+ | instructions: | ||
+ | max memory: | ||
+ | loaded code: | ||
+ | |||
+ | ====================================================== 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. | ||
< | < | ||
- | javac -cp / | + | JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) |
+ | |||
+ | |||
+ | ====================================================== 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: | ||
+ | states: | ||
+ | search: | ||
+ | choice generators: | ||
+ | heap: | ||
+ | instructions: | ||
+ | max memory: | ||
+ | loaded code: classes=62, | ||
+ | |||
+ | ====================================================== search finished: 2/29/20 4:10 PM | ||
</ | </ | ||
- | or add / | ||
- | To receive feedback, submit | + | Submit your configuration file (name it Main-nhandler.jpf). |
+ | |||
+ | To receive feedback, submit | ||
< | < | ||
- | submit 4315 lab6 (name of file) | + | submit 4315 lab5 (name of file) |
</ | </ | ||
- | before | + | before |
lab8.1519570698.txt.gz · Last modified: 2018/02/25 14:58 by franck