Exponenta Banner

Внешние ограничения для анализа Polyspace

Polyspace® использует код, который вы предоставляете, чтобы сделать предположения об элементах, таких как переменные диапазоны и позволенный buffer size для указателей. Иногда предположения, что Polyspace делает, более широки, чем, что вы ожидаете, который может привести к ложным положительным сторонам Bug Finder или большему количеству Code Prover оранжевые проверки. Чтобы уменьшать такие ложные положительные стороны или оранжевые проверки, можно задать внешние ограничения на:

  • Глобальные переменные.

  • Пользовательские функции.

    Ограничения на пользовательские функции не применяются к анализу Bug Finder.

  • Заблокированные функции.

    Ограничения на заблокированные функции не применяются к анализу Bug Finder.

Для получения дополнительной информации смотрите, Задают Внешние Ограничения. Для частичного списка ограничений смотрите Ограничительные Ограничения Спецификации.

Внешние ограничения в Bug Finder

В Bug Finder можно ограничить только глобальные переменные.

Чтобы уменьшать ложные положительные стороны, дефекты от неограниченных входных параметров подавлены во время анализа Bug Finder. Чтобы найти эти виды дефектов, не используйте внешние ограничения. Вместо этого чтобы запустить более строгий анализ Bug Finder, который рассматривает возможные пути к выполнению кода, используйте Run stricter checks considering all values of system inputs (-checks-using-system-input-values). Смотрите расширяют средства проверки Bug Finder, чтобы найти дефекты от определенных системных входных значений.

Ограничительная спецификация

В пользовательском интерфейсе десктопных решений Polyspace можно задать ограничения через окно Constraint Specification. Ограничения сохранены в XML-файле, который можно снова использовать для других проектов.

Эта таблица описывает различные столбцы в окне Constraint Specification. Если вы непосредственно редактируете ограничительный XML-файл, чтобы задать ограничение (например, в Серверных продуктах Polyspace), эта таблица также показывает соответствие между столбцами в пользовательском интерфейсе и записями в XML-файле. Запись XML, подсвеченная полужирным, появляется в соответствующем столбце окна Constraint Specification.

СтолбецНастройкиЗапись XML-файла
Name

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

Это Отображения столбца три расширяемых пункта меню:

  • Глобальные переменные – глобальные переменные Отображений в проекте.

  • Определяемые пользователем функции – Отображения пользовательские функции в проекте. Расширьте имя функции, чтобы видеть его входные параметры.

  • Заблокированные функции – Отображения список интерфейсных функций в проекте. Расширьте имя функции, чтобы видеть входные параметры и возвращаемые значения.

<function name = "funcName" ...>

<scalar name = "arg1" ...>

<pointer name = "arg2" ...>

FileОтображает имя исходного файла, содержащего переменную или функцию. 
<file name = "C:\Project1\Sources\file.c" ...>
Attributes

Информация об отображениях о переменной или функции.

Например, статические переменные отображают static. Невостребованные функции отображают unused.

 
<function name="funcName" attributes="unused" ...>
Data TypeОтображает тип переменной. 
<scalar name="arg1" complete_type="int32" ...>
Main Generator Called

Применимый только для пользовательских функций.

Задает, вызывает ли основной генератор функцию:

  • MAIN GENERATOR – Основной генератор может вызвать эту функцию, в зависимости от значения -functions-called-in-loop (C) или -main-generator-calls (C++) параметр.

  • NO – Основной генератор не вызовет эту функцию.

  • YES – Основной генератор вызовет эту функцию. 

<function name="funcName" main_generator_called="MAIN_GENERATOR" ...>
Init Mode

Задает, как программное обеспечение присваивает область значений переменной:

  • MAIN GENERATOR – Переменный диапазон присвоен в зависимости от настроек основных опций генератора -main-generator-writes-variables и -no-def-init-glob.

  • IGNORE – Переменная не присвоена никакой области значений, даже если диапазон указан.

  • INIT – Переменная присвоена заданной области только при инициализации и сохраняет область значений до первой записи. Когда INIT используется в Bug Finder, области значений распространены, только если любое из этих условий верно:

    • Глобальная переменная используется в функции, которая вызвана от main() функция.

    • Глобальная переменная задана как const.

  • PERMANENT – Переменная постоянно присвоена заданной области. Если переменная присвоена вне этой области значений во время программы, никакое предупреждение не обеспечивается. Используйте globalassert режим, если вам нужно предупреждение.

Пользовательские функции поддерживают только INIT режим.

Интерфейсные функции поддерживают только PERMANENT режим.

Для верификаций C глобальные указатели поддерживают MAIN GENERATOR, IGNORE, или INIT режим.

  • MAIN GENERATOR – Указатель следует опциям основного генератора.

  • IGNORE – Указатель не инициализируется.

  • INIT – Задайте, является ли указателем NULL, и как резкий объект выделяется (Инициализируйте Указатель и Init Выделенные опции).

 
<scalar name="arg1" init_mode="INIT" ...>
Init Range

Задает минимальные и максимальные значения для переменной.

Можно использовать ключевые слова min и max обозначить минимальные и максимальные значения типа переменной. Например, для типа долго, min и max соответствуйте-2^31 и 2^31-1 соответственно.

Можно также использовать шестнадцатеричные значения. Например: 0x12..0x100.

Для enum переменные, вы не можете указать диапазоны непосредственно при помощи констант перечислителя. Вместо этого используйте значения, представленные константами.

Для enum переменные, можно также использовать ключевые слова enum_min и enum_max обозначить минимальные и максимальные значения, которые может принять переменная. Например, для enum переменная типа, заданного ниже, enum_min 0 и enum_max 5:

enum week{ sunday, monday=0, tuesday, wednesday, thursday, friday, saturday};

 
<scalar name="arg1" init_range="-1..0"...>
Initialize Pointer

Применимый только к указателям. Enabled только, когда вы задаете Init Mode:INIT.

Задает, должен ли указателем быть NULL:

  • May-be NULL – Указателем мог потенциально быть Нулевой указатель (или не).

  • Not Null – Указатель никогда не инициализируется как нулевой указатель.

  • Null – Указатель инициализируется как NULL.

Примечание

Не применимый для проектов C++. Смотрите Ограничительные Ограничения Спецификации.

 
<pointer name="arg1" initialize_pointer="Not NULL"...>
Init Allocated

Применимый только к указателям. Enabled только, когда вы задаете Init Mode:INIT.

Задает, как резкий объект выделяется:

  • MAIN GENERATOR – Резкий объект выделяется основным генератором.

  • NONE – Резкий объект не записан.

  • SINGLE – Резкий объект или первый элемент массива инициализируются.

  • MULTI – Все объекты (или элементы массива) инициализируются.

Две других опции доступны для аргументов указателя к заблокированным функциям:

  • SINGLE_CERTAIN_WRITE – Резкий объект или первый элемент массива инициализируются заблокированной функцией.

  • MULTI_CERTAIN_WRITE – Все резкие объекты (или элементы массива) инициализируются заблокированной функцией.

Для заблокированных функций, опции SINGLE и MULTI означайте вероятную инициализацию вместо определенной инициализации.

Примечание

Не применимый для проектов C++. Смотрите Ограничительные Ограничения Спецификации.

 
<pointer name="arg1" init_pointed="MAIN_GENERATOR"...>
# Allocated Objects

Применимый только к указателям.

Задает, на сколько объектов указывает указатель (резкий объект рассматривается как массив).

Параметр Init Allocated задает, сколько выделенных объектов на самом деле инициализируется. Например, рассмотрите этот код:

void func(int *ptr) {
    assert(ptr[0]==1);
    assert(ptr[1]==1);
}
Если вы задаете эти ограничения:

  • ptr установили Init Allocated на MULTI и набор # Allocated Objects к 2,

  • *ptr установили Init Range на 1..1,

оба утверждения являются зелеными. Если вы задаете эти ограничения:

  • ptr установили Init Allocated на SINGLE

  • *ptr установили Init Range на 1..1,

второе утверждение является оранжевым. Только первый объект, что ptr точки к инициализированному к 1. Объекты вне первого могут быть потенциально полным спектром.

Примечание

Не применимый для проектов C++. Смотрите Ограничительные Ограничения Спецификации.

 
<pointer name="arg1" number_allocated="10"...>
Global AssertЗадает, выполнить ли утверждение, проверяют переменную при глобальной инициализации, и после каждого присвоения. 
<scalar name="glob" global_assert="YES"...>
Global Assert RangeЗадает минимальные и максимальные значения для области значений, которую вы хотите проверять. 
<scalar name="glob" assert_range="0..200"...>
CommentКомментарии, что вы вводите, например, выравнивание для своих значений DRS. 
<scalar name="glob" comment="Speed Range"...>

Ограничительные ограничения спецификации

Вы не можете задать эти ограничения:

  • Указатели C++ или ссылки не могут быть ограничены:

    На C++ вы не можете ограничить указатель или ссылочные аргументы функций.

    Из-за полиморфизма указатель C++ или ссылка могут указать на объекты нескольких классов в иерархии классов и могут потребовать вызывающих различных конструкторов. Предварительный анализ для ограничительной спецификации не может определить который тип объекта ограничить или который конструктор вызвать.

  • Ограничения не могут быть отношениями:

    Вы не можете задать ограничение, которое связывает возвращаемое значение функции к ее входным параметрам. Можно указать только постоянный диапазон для ограничений.

  • Несколько областей значений, не возможных:

    Вы не можете указать несколько диапазонов для ограничения. Например, вы не можете указать, что аргумент функции имеет или значение-1 или значение в области значений [1,100]. Вместо этого укажите диапазон [-1 100] или выполните два отдельных исследования, однажды со значением-1 и однажды с областью значений [1,100].

Похожие темы

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

Поддержка