Невозможно использовать команды JBMC (Bounded Model Checker) для Java - PullRequest
Новая
       106

Невозможно использовать команды JBMC (Bounded Model Checker) для Java

0 голосов
/ 19 июня 2019

Я новичок в JBMC (Проверка ограниченной модели) . У нас есть требование выяснить возможности исключения RunTime, которое может возникнуть в Java-программе, без ее запуска. Мы искали некоторые абстрактные рамки интерпретации и обнаружили, что 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]); 
    } 

}

В приведенной выше программе мы получим ArrayIndexOutOfBoundException, когда цикл будет выполняться во время 6-й итерации. Но как предсказать это, используя JBMC? Мы нашли лист команд, который предоставляет подробную информацию о Опции командной строки в JBMC, но мы не смогли найти комбинации команд и то, как их использовать. Есть ли какой-нибудь Java API или Документы, доступные для JBMC?

Пожалуйста, предложите !!.

1 Ответ

0 голосов
/ 26 июня 2019

В отличие от CBMC, JBMC не поддерживает все перечисленные опции здесь .Вы можете заметить это, запустив jbmc --help.Если вы запустите что-то вроде jbmc <class> --bounds-check, вы получите «ошибку использования».

О вашем классе java: jbmc работает на .jar или .class .Попробуйте сначала сгенерировать .class следующим образом:

javac SampleClass.java

, затем запустите jbmc на SampleClass.class следующим образом:

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 .

...