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.
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
Inside the "TestA" element, we have multiple "Source" elements.
The "Source" element has three attributes.
Maybe the most convenient way to parse this XML is using ElementTree with Python. You can get the root with getroot() method.
import xml.etree.ElementTree as ET
tree = ET.parse('setup.xml')
root = tree.getroot()
From the root (or any element object), you can get the element with find() method with the element name as parameter. You can get the element whatever you want likewise.
The interesting thing you notice is that the element object returns iterator that gives all the sub elements.
The element object also has the attrib dictionary that contains the attributes.
testA = root.find('TestA')
sources = testA.find('Source')
for source in testA: # testA returns all the sub elements.
print source.attrib
print source.attrib['numberOfParams']
print source.attrib['filePath']
print source.attrib['method']
This is the result to run the script.
{'numberOfParams': '2', 'method': 'method', 'filePath': 'Charlie'}
2
Charlie
method
Generating XML
You can crete the Element object with Element() with name of the element as a parameter.
root = ET.Element('data')
With SubElement with first parameter as the element object, and the second as the element name, one can
add sub elements. As element object has the attrib dictionary, by filling in the dictionary one can add attributes.
Inside the file, we have all the directory information that points to the jar file and others.
This is an example to get two summary files to execute the software equivalence checker.
