Java 路径查找器 NumericValueChecker答案

【问题标题】：Java Path Finder NumericValueCheckerJava 路径查找器 NumericValueChecker
【发布时间】：2018-11-27 08:06:30
【问题描述】：

我正在尝试学习 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 时，它找不到任何错误。结果是“未检测到错误”。它应该检测到大于上限 60 的 110。

为什么它不起作用？我需要在我的新 BasicCheck.java 或 BasicCheck.jpf 中添加一些额外的东西吗？

提前致谢。

【问题讨论】：

标签： java path-finding jpf

【解决方案1】：

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

将BasicCheck.java和BasicCheck.jpf放在jpf-core/src/examples目录下。

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

就是这样。现在您可以使用命令java -jar build/RunJPF.jar src/examples/BasicCheck.jpf 来运行Java Path Finder。

【讨论】：