A sample execution case: Avl Tree

In this page you can find all the required steps to perform symbolic execution with different techniques over the bfs routine in the Avl Tree case study using 8 as the scope. Below you can find the instructions for the following techniques:

• • LI

  • LI+NN

Symbolic Execution over the BFS routine with LI

In order to perform symbolic execution we need to configure the java file of the target structure and a .jpf file containing the symbolic execution parameters. For the AvlTree case study you need to:

• 1. Go to the project jpf-symbc-bounded

  2. In the source folder src/examples go to the package symbolicheap.bounded.

  3. Copy the content of the file AvlTree-bfs.java.proto.LI to the file AvlTree.java. Replace all the occurrences of __SIZE__ by the desired scope, in our case 8.

  4. Copy the content of the file AvlTree.jpf.proto.LI to the file AvlTree.jpf. Replace all the occurrences of __SIZE__ by 8

  5. Finally, open the AvlTree.java file, left click over the file AvlTree.jpf in the Project Explorer and from the dropdown next to the Run symbol select the option run-JPF-symbc-bounded (use run-jpf-symbc-bounded-mac if your are using Mac OS or run-jpf-symbc-bounded if you are using Linux):

If you want to perform symbolic execution over any other method of the AvlTree case study, you just need to find the corresponding java.proto.LI file, and copy it to the AvlTree.java file. If you want to change the scope, just replace all the occurrences of __SIZE__ by the desired number. At the end of the execution the console should looks this. To analyze any other method use any file which name matches AvlTree*.java.proto.LI

Symbolic Execution over the BFS routine with LI+NN

Similarly, to use LI+NN instead of LI, the java file of the target structure and the .jpf file containing the symbolic execution parameters needs to be configured. For the AvlTree case study you need to:

• 1. Go to the project jpf-symbc-bounded

  2. In the source folder src/examples go to the package symbolicheap.bounded.

  3. Copy the content of the file AvlTree-bfs.java.proto.LINN to the file AvlTree.java. Replace all the occurrences of __SIZE__ by the desired scope, in our case 8.

  4. Copy the content of the file AvlTree.jpf.proto.LINN to the file AvlTree.jpf. Replace all the occurrences of __SIZE__ by 8

  5. Finally, open the AvlTree.java file, left click over the file AvlTree.jpf in the Project Explorer and from the dropdown next to the Run symbol select the option run-JPF-symbc-bounded (use run-jpf-symbc-bounded-mac if your are using Mac OS or run-jpf-symbc-bounded if you are using Linux).

See the execution result. To analyze any other method use any file which name matches AvlTree*.java.proto.LINN