Расширьте средства проверки Bug Finder, чтобы найти дефекты от определенных системных входных значений

Эта тема показывает, как найти возможные дефекты от определенных значений системных входных параметров. В отличие от Программы автоматического доказательства Кода, 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 не обеспечивает звуковой и исчерпывающий анализ Программы автоматического доказательства Кода. Например, если Bug Finder не обнаруживает ошибки после расширения средств проверки, это отсутствие обнаруженных ошибок не имеет тех же гарантий как зеленые регистрации Программы автоматического доказательства Кода.

Расширьте средство проверки

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

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

Средства проверки, которые могут быть расширены

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

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