时间戳

首页 > 解决方案 > Java 路径查找器 NumericValueChecker

java - Java 路径查找器 NumericValueChecker

问题描述

我正在尝试学习 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 的示例文件夹，其中 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 中添加一些额外的东西吗？

提前致谢。

标签： javapath-findingjpf

解决方案

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

将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。

推荐阅读