Java 探路者数值检查器

Question

我正在努力学习 Java 路径查找器 (JPF)。我下载了 JPF 并构建了它。目前我有 jpf-core 文件夹，其中包含示例 .java 文件及其相应的 .jpf 文件。我的目标是创建一个新的基本 .java 文件并检查此文件中的特定值是否超过我在 .jpf 文件中指定的最大范围。

示例文件夹 中有一个名为 NumericValueCheck.java 的 .java 文件，这正是我想要的，并且按预期工作。（当值超过边界时发现）

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

但是，我创建了一个新的.java 文件并将其命名为“BasicCheck.java”。这是其中的代码；

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

这是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

我在单独的目录中使用 javac BasicCheck.java 编译了 BasicCheck.java。然后我将 "BasicCheck.java" 和 "BasicCheck.jpf" 复制到 jpf-core 的 examples 文件夹，其中 NumericValueCheck.java 和 NumericValueCheck.jpf 也在同一个地方。我还将 "BasicCheck.class" 复制到 jpf-core/build/examples 目录，其中 "NumericValueCheck.class" 也在同一位置。

但是，当我运行命令java -jar build/RunJPF.jar src/examples/BasicCheck.jpf时，它找不到任何错误。结果是"no error detected"。它应该检测到大于上限 60 的 110。

为什么不起作用？我是否需要向我的新 BasicCheck.java 或 BasicCheck.jpf 添加一些额外的东西？

提前致谢。

Answer 1

经过长时间的努力，我找到了解决方案。解决方法很简单。

将BasicCheck.java和BasicCheck.jpf放在目录jpf-core/src/examples.[=16=下]

不要使用javac 编译为源代码。打开终端和 cd 到 jpf-core 目录。然后键入以下命令：./gradlew buildJars.

就是这样。现在您可以使用命令 java -jar build/RunJPF.jar src/examples/BasicCheck.jpf 到运行 Java 路径查找器。

Java 探路者数值检查器

Java Path Finder NumericValueChecker

java

path-finding

jpf