Расширение Bug Finder Checkers, чтобы найти дефекты из значений Входа конкретной системы

В этом разделе показано, как найти возможные дефекты из определенных значений входов системы. В отличие от Кода Prover, Bug Finder не проверяет полностью на ошибки времени выполнения для всех комбинаций системных входов. Однако можно расширить некоторые шашки Bug Finder и найти, есть ли определенные системные входные значения, которые могут привести к ошибкам времени выполнения.

Идентифицируйте необходимость расширения средства проверки

Сначала определите, является ли существующая проверка достаточной для ваших требований.

Для образца - шашка Bug Finder Integer division by zero определяет, может ли операция деления иметь нулевой знаменатель. Предположим, что функция библиотеки имеет возможность деления на нуль после нескольких числовых операций. Например, рассмотрите функцию speed здесь:

#include <assert.h>

int speed(int k) {
    int i,j,v;
    i=2;
    j=k+5;
    while (i <10) {
            i++;
            j+=3;
    }

    v = 1 / (i-j); 
    return v+k;
}

Предположим, что вы видите спорадическую ошибку времени выполнения, когда выполнение программы вводит эту функцию, и анализ Bug Finder по умолчанию не обнаруживает проблему. Чтобы минимизировать ложные срабатывания, анализ по умолчанию может подавить проблемы из определенных значений неизвестного входа (что, если это значение не произошло на практике во время исполнения?). Смотрите также Входы в Polyspace Bug Finder. Чтобы найти первопричину спорадической ошибки, можно запустить более строгий анализ Bug Finder именно для этой функции.

Обратите внимание, что даже после продления шашек Bug Finder не обеспечивает звукового и исчерпывающего анализа Code Prover. Например, если Bug Finder не обнаруживает ошибки после расширения шашек, это отсутствие обнаруженных ошибок не имеет тех же гарантий, что и зеленые проверки в Code Prover.

Расширение шашки

Чтобы расширить шашку и обнаружить вышеуказанную проблему, используйте следующие опции:

Run stricter checks considering all values of system inputs (-checks-using-system-input-values): Включить эту опцию. Шашки, которые полагаются на числовые значения, теперь могут рассматривать все входные значения для функций с, по крайней мере, одной тележкой. Можно изменить, какие функции рассматриваются при помощи следующей опции.
Consider inputs to these functions (-system-inputs-from): Используйте значение custom и введите имя функции, входы которой должны быть рассмотрены, в данном случае speed. В командной строке используйте аргумент option custom=speed.

Когда вы запускаете анализ Bug Finder, вы видите возможное целое деление на нуль на операции деления. Результат показывает пример входного значения функции speed это в конечном счете приводит к дефекту тока (нулевое значение знаменателя).

Подсказки о дефекте показывают, как входное значение распространяется через код, в конечном счете приводя к одному множеству значений, которые вызывают дефект.

Tooltips on variables in source code show how the input value of -19 leads to the final values that cause the division by zero defect.

Шашки, которые могут быть расширены

Следующие шашки затронуты числовыми значениями входов и могут быть расширены с помощью предыдущих опций:

Документация