## Setup

In order to use JPF/SPF, one needs a setup file in "~/.jpf/site.properties" file. This setup file is a pointer that points where all the core files and extensions are located.
# JPF site configuration
user.home = DIRECTORY
jpf.home = ${user.home}/DIR1 jpf.libraries = DIR2 # can only expand system properties jpf-core =${jpf.libraries}/jpf-core

jpf-symbc = ${jpf.libraries}/jpf-symbc extensions+=,${jpf-symbc}

The pointed directory has another "jpf.proterites" configuration files. Inside the file, we have all the directory information that points to the jar file and others.
...

jpf-core = ${config_path} jpf-core.native_classpath=\${jpf-core}/build/jpf.jar;\
${jpf-core}/build/jpf-annotations.jar;\${jpf-core}/lib/junit-4.10.jar

jpf-core.classpath=\
${jpf-core}/build/jpf-classes.jar;\${jpf-core}/build/examples

jpf-core.sourcepath=\
${jpf-core}/src/examples jpf-core.test_classpath=\${jpf-core}/build/tests

jpf-core.peer_packages = gov.nasa.jpf.jvm,,

...


## Java code with package

This is the sample code.
package a.b;

public class HelloA {
public int testRefactored (int refs, int flags) {
if (flags != 0)
return flags;
else if (refs != 0)
return refs;
return 10;
}

public static void main(String[] args) {
HelloA ex = new HelloA();
int ret = ex.testRefactored(0,0);
System.out.print(ret);
}
}

We need to compile this java code using debug flag "-g", and move the generated class file where the java can find it.
javac -g HelloA.java
mkdir -p a/b

Then, we need the setup file. In this setup file, one needs to specify the listener. In this listener example, it specifies the listener class, and it should be located in somewhere where the "site.properties" can point to.
target = a.b.HelloA

basedir = PATH
rse.testFile = ${basedir}/HelloA.txt symbolic.method= a.b.HelloA.testRefactored(sym#sym) rse.testCases = true listener = gov.nasa.jpf.porting.listener.RSESymbolicListener #If we don't set the bounds then one of the constraints times out. symbolic.min_int=-100 symbolic.max_int=100 symbolic.min_double=-1000.0 symbolic.max_double=1000.0 symbolic.undefined=0  Then we can execute the JPF jar binary. JPF_JAR_DIR=/Users/smcho/Dropbox/smcho/research/jpf/jpf-core/build java -jar${JPF_JAR_DIR}/RunJPF.jar ./HelloA.jpf

This is an example to get two summary files to execute the software equivalence checker.
mkdir -p a/b
#
javac -g HelloA.java
mv HelloA.class a/b
#
JPF_JAR_DIR=/Users/smcho/Dropbox/smcho/research/jpf/jpf-core/build
java -jar ${JPF_JAR_DIR}/RunJPF.jar HelloA.jpf # mkdir -p c/d # javac -g HelloB.java mv HelloB.class c/d JPF_JAR_DIR=/Users/smcho/Dropbox/smcho/research/jpf/jpf-core/build java -jar${JPF_JAR_DIR}/RunJPF.jar HelloB.jpf


## Java code with no package

With the java source without package, everything is the same except
• No need to move the class file into the directory.
• No need to prepend the package info in the configuration files.