0

我是JBMC（有界模型检查器）的新手。我们需要找出在不运行Java程序的情况下可能发生在Java程序中的RunTime Exception的可能性。我们搜索了一些抽象解释框架，发现 JBMC 在这种情况下会有所帮助。

例如 ：

public class SampleClass {

    public static void main(String[] args) 
    { 
        int ar[] = {1, 2, 3, 4, 5}; 
        for (int i=0; i<=ar.length; i++) 
          System.out.println(ar[i]); 
    } 

}

在上面的程序中，当循环在第 6 次迭代期间运行时，我们将得到 ArrayIndexOutOfBoundException。但是如何使用 JBMC 来预测呢？我们找到了提供 JBMC 中命令行选项详细信息的命令表，但我们无法找到命令组合以及如何使用它。是否有可用于 JBMC 的 Java API 或文档？

请推荐！！

4

1 回答 1

0

与 CBMC 不同，JBMC 不支持此处列出的所有选项。您可以通过运行来注意到这一点jbmc --help。如果你运行类似的东西，jbmc <class> --bounds-check你会得到一个“使用错误”。

关于您的 java 类： jbmc 适用于.jar或.class。尝试先生成一个 .class，如下所示：

javac SampleClass.java

SampleClass.class然后按如下方式运行 jbmc ：

jbmc SampleClass.class --unwind N（尝试使用不同的 N 值变得更有信心）

在 N=6 的结果下方：

JBMC version 5.12 (cbmc-5.11-3477-gcd70727ed) 64-bit x86_64 linux
Parsing SampleClass.class

...

** Results:
[array-create-negative-size.1] Array size should be >= 0: SUCCESS
[array-create-negative-size.2] Array size should be >= 0: SUCCESS
[array-create-negative-size.3] Array size should be >= 0: SUCCESS
[array-create-negative-size.4] Array size should be >= 0: SUCCESS
[array-create-negative-size.5] Array size should be >= 0: SUCCESS
[array-create-negative-size.6] Array size should be >= 0: SUCCESS
[array-create-negative-size.7] Array size should be >= 0: SUCCESS
[array-create-negative-size.8] Array size should be >= 0: SUCCESS
[array-create-negative-size.9] Array size should be >= 0: SUCCESS
SampleClass.java function java::SampleClass.main:([Ljava/lang/String;)V
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.1] line 4 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.5] line 4 Array index should be < length: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.2] line 4 Array index should be < length: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.3] line 4 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.3] line 4 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.3] line 4 Array index should be < length: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.4] line 4 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.4] line 4 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.4] line 4 Array index should be < length: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.5] line 4 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.1] line 4 no uncaught exception: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.5] line 4 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-create-negative-size.1] line 4 Array size should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.2] line 4 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.1] line 4 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.1] line 4 Array index should be < length: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.2] line 4 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.6] line 5 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.7] line 6 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.6] line 6 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.6] line 6 Array index should be < length: FAILURE
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.8] line 6 Null pointer check: SUCCESS

** 1 of 31 failed (2 iterations)
VERIFICATION FAILED

我希望这有帮助。我也是jbmc的新手。我过去使用过 cbmc，可以在此处和此处找到更多文档，但很少有可用于jbmc的文档。

于 2019-06-26T13:50:33.910 回答