Run stricter checks considering all values of system inputs (-checks-using-system-input-values)

Включите более строгие проверки и обеспечьте примеры значений, которые приводят к обнаруженному дефекту

Описание

Эта опция влияет на анализ Bug Finder только.

Эта опция не доступна для кода, сгенерированного из кода MATLAB® или моделей Simulink®.

Включите более строгий статический анализ для подмножества средств проверки дефекта числового и статического ЗУ. Polyspace® полагает, что все возможные значения системы вводят и обеспечивают примеры значений, которые могут привести к обнаруженным дефектам. Для каждого функционального foo то, что вы задаете с Consider inputs to these functions (-system-inputs-from), это системные входные параметры.

  • Каждый аргумент foo.

  • Каждое чтение глобальной переменной foo или один из его вызываемых.

    Для main() функция, анализ принимает, что глобальные переменные инициализируются значением 0.

  • Каждое чтение энергозависимой переменной foo или один из его вызываемых.

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

Более строгие проверки включены для этого подмножества дефектных средств проверки.

 Дефектное подмножество средств проверки

Можно просмотреть примеры значений, которые приводят к обнаруженным дефектам в столбце Events панели Results Details в настольном интерфейсе или Polyspace доступ к веб-интерфейсу.

Установите опцию

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

Командная строка и файл опций: Используйте опцию -checks-using-system-input-values. Смотрите информацию о командной строке.

Почему использование эта опция

Анализ Bug Finder по умолчанию не отмечает дефекты, которые вызываются определенными значениями неизвестных входных параметров. Поскольку входные параметры могут быть ограничены или инициализированы в исходном файле, который вы не анализируете, или определенное значение, вызывающее дефектную силу не, происходит на практике, аналитическое поведение по умолчанию помогает минимизировать ложные положительные стороны.

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

Настройки

On

Polyspace рассматривает все возможные значения системных входных параметров для подмножества средств проверки дефекта числового и статического ЗУ и обеспечивает примеры значений, которые приводят к обнаруженным дефектам.

От (значения по умолчанию)

Polyspace рассматривает возможные значения системного входа, только если вход ограничен ограничениями в вашем коде, такими как assert или if. Анализ не обеспечивает примеров значений, которые приводят к обнаруженным дефектам.

Зависимости

Советы

  • Если вы устанавливаете внешние ограничения на глобальные переменные, анализ показывает примеры значений глобальной переменной, вызывающих дефекты только в рамках этих ограничений. Смотрите Constraint setup (-data-range-specifications).

  • Если вход является указателем p, анализ принимает, что указатель не является пустым и может быть безопасно разыменован. Значение в качестве примера входа, вызывающего дефект, является значением *p. Это значение представлено как массив в панели Results Details. Например, в этом фрагменте кода:

    void func(int* x){
    	int tmp= *(x+3);
    	
    	if(1/(tmp-4))
    		return;
    }
    Значение в качестве примера входа, вызывающего дефект, {0,0,0,4}, где массив представляет *x, *(x+1), *(x+2), и *(x+3). Значение *(x+3)=4 вызывает деление на нуль.

  • Анализ обрабатывает эти стандартные библиотечные функции, которые читают значения из внешних источников как заблокированные функции.

    • getchar

    • getc

    • fgetc

    • scanf

  • Более строгий анализ рассматривает все возможные значения системных входных параметров, но это не исчерпывающий анализ. Если Bug Finder не может определить, вызывает ли конкретный вход дефект, никакой дефект не показывают. Для больше согласно исчерпывающему анализу, смотрите, Выбирают Between Polyspace Bug Finder и Polyspace Code Prover.

Информация о командной строке

Параметр: -checks-using-system-input-values
Значение по умолчанию: Off
Пример (Bug Finder): Polyspace Bug Finder - источники file_name - числовые средства проверки, static_memory "проверки с помощью системных входных значений"
Пример (Сервер Bug Finder): сервер средства поиска ошибки полипробела - источники file_name - числовые средства проверки, static_memory "проверки с помощью системных входных значений"
Введенный в R2020a