Exponenta Banner

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

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

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

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

Например, средство проверки Средства поиска Ошибки Integer division by zero (Polyspace Bug Finder Access) обнаруживает, если операция деления может иметь нулевой знаменатель. Предположим, библиотечная функция имеет возможность деления на нуль после нескольких числовых операций. Например, рассмотрите функциональный 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;
}
Предположим, что вы видите спорадическую ошибку времени выполнения, когда ваше выполнение программы вводит эту функцию, и анализ Средства поиска Ошибки по умолчанию не обнаруживает проблему. Чтобы минимизировать ложные положительные стороны, анализ по умолчанию может подавить проблемы от определенных значений неизвестного входа (что, если это значение не произошло на практике во время выполнения?). См. также Входные параметры в Polyspace Bug Finder (Polyspace Bug Finder Access). Чтобы найти первопричину спорадической ошибки, можно запустить более строгий анализ Средства поиска Ошибки для только этой функции.

Обратите внимание на то, что даже после расширения средств проверки, Средство поиска Ошибки не обеспечивает звуковой и исчерпывающий анализ Программы автоматического доказательства Кода. Например, если Средство поиска Ошибки не обнаруживает ошибки после расширения средств проверки, это отсутствие обнаруженных ошибок не имеет тех же гарантий как зеленые регистрации Программы автоматического доказательства Кода.

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

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

  • 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 опции.

Когда вы запускаете анализ Средства поиска Ошибки, вы видите возможное целочисленное деление на нуль на операции деления. Результат показывает пример входного значения к функциональному 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.

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

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

Похожие темы

Документация Polyspace Bug Finder Server

Поддержка