В этом разделе показано, как найти возможные дефекты из определенных значений системных входных данных. В отличие от Code Prover, 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 не предоставляет звуковой и исчерпывающий анализ 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 это в конечном итоге приводит к текущему дефекту (нулевое значение знаменателя).
В подсказках по дефекту показано, как входное значение распространяется по коду, что в конечном итоге приводит к одному набору значений, вызывающих дефект.
Следующие шашки зависят от числовых значений входных данных и могут быть расширены с помощью предыдущих опций: