javapath-findingjpf

Java Path Finder NumericValueChecker

I am trying to learn Java Path Finder (JPF). I downloaded the JPF and build it. Currently I have jpf-core folder which has example .java files together with their corresponding .jpf files. My goal is to create a new basic .java file and check whether a specific value in this file exceeds the max-bound I specified in the .jpf file.

In the examples folder there is .java file called NumericValueCheck.java which is exactly what I want, and it works as expected. (finds when the value exceeds the bound)

NumericValueCheck.java

public class NumericValueCheck {
  public static void main (String[] args){
    double someVariable;
    someVariable = 42;  
    someVariable = 60; 
  }
}

NumericValueCheck.jpf

target = NumericValueCheck

listener = .listener.NumericValueChecker

# NumericValueChecker configuration
range.vars = 1
range.1.var = NumericValueCheck.main(java.lang.String[]):someVariable
range.1.min = 0
range.1.max = 42

However, I created a new .java file and named it "BasicCheck.java". Here is the code inside it;

public class BasicCheck {
public static void main(String[] args){
    double result;
    result = 60;
    result = 110;
    }
}

Here are the properties in BasicCheck.jpf;

target = BasicCheck

listener = .listener.NumericValueChecker

# NumericValueChecker configuration
range.vars = 1
range.1.var = BasicCheck.main(java.lang.String[]):result
range.1.min = 0
range.1.max = 60

I compiled the BasicCheck.java using javac BasicCheck.java in a separate directory. Then I copy "BasicCheck.java" and "BasicCheck.jpf" to examples folder of jpf-core where NumericValueCheck.java and NumericValueCheck.jpf also in the same place. I also copy "BasicCheck.class" to jpf-core/build/examples directory where "NumericValueCheck.class" also in the same place.

However, when I run the command java -jar build/RunJPF.jar src/examples/BasicCheck.jpf, it can't find any error. The result is "no error detected". It should detect 110 which is bigger than the upper bound 60.

Why is it not working? Do I need to add something extra to my new BasicCheck.java or BasicCheck.jpf ?

Thanks in advance.

Solution

  • I found the solution after a long effort. The solution is simple.

    Put BasicCheck.java and BasicCheck.jpf under the directory jpf-core/src/examples.

    Do NOT compile to source using javac. Open the terminal and cd to jpf-core directory. Then type the following command: ./gradlew buildJars.

    That's it. Now you can use the command java -jar build/RunJPF.jar src/examples/BasicCheck.jpf to run Java Path Finder.