lab4
Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| lab4 [2017/01/27 21:43] – franck | lab4 [2017/01/30 13:56] (current) – franck | ||
|---|---|---|---|
| Line 1: | Line 1: | ||
| + | ~~NOTOC~~ | ||
| + | |||
| ====== LAB 4 ====== | ====== LAB 4 ====== | ||
| Line 67: | Line 69: | ||
| * vt.methods | * vt.methods | ||
| - | To receive feedback, submit your work as a text file using the submit command before Tuesday January 31: | + | To receive feedback, submit your work as a text file using the submit command before Tuesday January 31:\\ |
| submit 4315 lab4 <name of the listener> | submit 4315 lab4 <name of the listener> | ||
| Line 154: | Line 156: | ||
| We can assign any long value to the property budget.max_heap. | We can assign any long value to the property budget.max_heap. | ||
| + | < | ||
| target=Constraints | target=Constraints | ||
| classpath=. | classpath=. | ||
| Line 159: | Line 162: | ||
| listener=gov.nasa.jpf.listener.BudgetChecker | listener=gov.nasa.jpf.listener.BudgetChecker | ||
| budget.max_heap=10000000 | budget.max_heap=10000000 | ||
| + | </ | ||
| Note that 10000000 bits = 10000000 / (1024 * 1024) megabytes = 9.5 megabytes. | Note that 10000000 bits = 10000000 / (1024 * 1024) megabytes = 9.5 megabytes. | ||
| JPF needs more heap space, it stops and produces the following output. | JPF needs more heap space, it stops and produces the following output. | ||
| + | < | ||
| JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | ||
| Line 174: | Line 178: | ||
| ====================================================== search constraint | ====================================================== search constraint | ||
| max heap exceeded: 10MB >= 9MB | max heap exceeded: 10MB >= 9MB | ||
| + | ... | ||
| + | </ | ||
| One can constrain JPF from checking more than 100 bytecode instructions as follows. | One can constrain JPF from checking more than 100 bytecode instructions as follows. | ||
| - | We can assign any int value to the property budget.max_insn. | + | We can assign any long value to the property budget.max_insn. |
| + | < | ||
| target=Constraints | target=Constraints | ||
| classpath=. | classpath=. | ||
| Line 183: | Line 190: | ||
| listener=gov.nasa.jpf.listener.BudgetChecker | listener=gov.nasa.jpf.listener.BudgetChecker | ||
| budget.max_insn=100 | budget.max_insn=100 | ||
| + | </ | ||
| Since this constraint is violated, JPF produces the following output. | Since this constraint is violated, JPF produces the following output. | ||
| + | < | ||
| JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | ||
| Line 196: | Line 205: | ||
| ====================================================== search constraint | ====================================================== search constraint | ||
| max instruction count exceeded: 100 | max instruction count exceeded: 100 | ||
| + | ... | ||
| + | </ | ||
| + | We can also limit the number of states that JPF explores by setting the property budget.max_state. | ||
| + | < | ||
| target=Constraints | target=Constraints | ||
| classpath=. | classpath=. | ||
| Line 203: | Line 216: | ||
| listener=gov.nasa.jpf.listener.BudgetChecker | listener=gov.nasa.jpf.listener.BudgetChecker | ||
| budget.max_state=100 | budget.max_state=100 | ||
| + | </ | ||
| + | Since the statespace of this app consists of more than 100 states, JPF stops and produces the following output. | ||
| - | + | < | |
| - | + | ||
| JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | ||
| Line 218: | Line 231: | ||
| ====================================================== search constraint | ====================================================== search constraint | ||
| max states exceeded: 100 | max states exceeded: 100 | ||
| + | ... | ||
| + | </ | ||
| + | We can also constrain the depth of the search. | ||
| + | |||
| + | < | ||
| target=Constraints | target=Constraints | ||
| classpath=. | classpath=. | ||
| Line 224: | Line 242: | ||
| listener=gov.nasa.jpf.listener.BudgetChecker | listener=gov.nasa.jpf.listener.BudgetChecker | ||
| budget.max_depth=100 | budget.max_depth=100 | ||
| + | </ | ||
| + | Since the depth of the search is greater than 100 for this app, JPF stops and produces the following output. | ||
| + | < | ||
| JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | ||
| Line 236: | Line 257: | ||
| ====================================================== search constraint | ====================================================== search constraint | ||
| max search depth exceeded: 100 | max search depth exceeded: 100 | ||
| + | ... | ||
| + | </ | ||
| + | |||
lab4.1485553433.txt.gz · Last modified: 2017/01/27 21:43 by franck