How JPF finds the files

site.properties

~/.jpf/site.properties file is the one where all the directory information is located.

# JPF site configuration
user.home = /Users/smcho/
jpf.home = ${user.home}/Dropbox/smcho/workspace/jpf

# can only expand system properties
jpf-core = ${jpf.home}/jpf-core

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

jpf-guided-test = ${jpf.home}/jpf-guided-test
extensions+=,${jpf-guided-test}

jpf-regression = ${jpf.home}/jpf-regression
extensions+=,${jpf-regression}

jpf-porting = ${jpf.home}/jpf-porting
extensions+=,${jpf-porting}

It points to where all the jpf related information are located.

jpf.properties

Now, you can set up your jpf.properties so that you can point to where ever you want.

#--- project specific host VM classpath (used by Java to load classes)
# NOTE: you have to replace the wildcard jar specs with explicit jar pathnames
# if this property file is used from within a build.xml or NetBeans project.xml,
# since both do not support wildcard patterns in classpath specs
jpf-porting.native_classpath =\
   ${jpf-porting}/build/jpf-porting.jar;\
   ${jpf-porting}/lib/*.jar;\
   ${jpf-symbc}/lib/commons-lang-2.4.jar;
   

#--- project specific JPF classpath (used by JPF to load system-under-test classes)
jpf-porting.classpath =\
   ${jpf-porting}/build/examples;

#--- where are the classes for the JPF regression tests (used by host VM and JPF)
jpf-porting.test_classpath =\
   ${jpf-porting}/build/tests
   
#--- project specific JPF sourcepath (used by JPF to locate sources for system-under-test classes)
jpf-porting.sourcepath =\
   ${jpf-porting}/src

#--- other project specific options go here (e.g. 'vm.insn_factory.class' or 'peer_packages')
peer_packages= gov.nasa.jpf.symbc,${peer_packages}
vm.storage.class=nil
search.multiple_errors=true
symbolic.dp=choco

From RunJPF.jar you can specify the file path of properties file.

java -jar /Users/smcho/Dropbox/smcho/workspace/jpf/jpf-core/build/RunJPF.jar \
+shell.port=4242 \
/Users/smcho/Dropbox/smcho/works/tasks/2012/seal/refactoringChecker/tests/case_ini_is_generated_from_ref_finder/TestA/A.jpf -v\
-c jpf.properties

Now, you can modify the properties file to point to the example directory.