15-414 Bug Catching:
Automated Program Verification and Testing
|
|
Main
Page
|
|
|
|
Syllabus
|
Assignments
|
|
|
Grading
|
Reading
|
|
Professor
|
|
15-414 Assignments, Java Pathfinder Information
The Java Pathfinder Website
Location for using Java Pathfinder on unix.andrew.cmu.edu:
/afs/andrew.cmu.edu/usr24/mtschant/15414-f07/jpf-release/bin/jpf
If you want to check the file Test.java first run javac on it to get Test.class. Second run Java Pathfinder as follows:
/afs/andrew.cmu.edu/usr24/mtschant/15414-f07/jpf-release/bin/jpf Test
in the directory that holds Test.class
Note that /afs/andrew.cmu.edu/usr24/mtschant/15414-f07/jpf-release/bin/jpf is a script that calls java on the correct class of Java Pathfinder. If you want to adjust the options passed to java, you might consider editing your own copy of this script. Note that this directory holds other scripts for using Java Pathfinder in other ways. I have not tested these scripts for compatibility with unix.andrew.cmu.edu.
|