Ограничения входных параметров функции

Для более точного анализа Code Prover можно задать ограничения (также известные как спецификации области значений данных или DRS) на входных параметрах функции. Code Prover проверяет определение функции на ошибки времени выполнения относительно ограниченных входов. Общие рабочие процессы см. в разделе «Задание внешних ограничений».

Например, для функции, заданной следующим образом, можно задать, что аргумент val имеет значения в области значений [1..10]. Можно также задать, что аргумент ptr указывает на массив с 3 элементами, где каждый элемент инициализируется:

int func(int val, int* ptr) {
     .
     .
}

Пользовательский интерфейс (только для настольных Продуктов)

Чтобы задать ограничения на входные параметры функции:

В строение проекта выберите Inputs & Stubbing. Нажмите кнопку для Constraint setup.
В окне Спецификация ограничений (Constraint Specification) щелкните.
Под узлом User Defined Functions вы видите список функций, входы которых могут быть ограничены.
Разверните узел для каждой функции.
Каждый входной параметр функции отображается в отдельной строке. Входы имеют синтаксис function_name.arg1, function_name.arg2, и т.д.
Задайте свои ограничения на один или несколько входных параметров функции. Для получения дополнительной информации смотрите Внешние ограничения для анализа Polyspace.
Для примера в предыдущем коде:
- Чтобы ограничить val в область значений [1..10], выберите INIT для Init Mode и ввода 1..10 для Init Range.
- Чтобы указать, что ptr указывает на массив с 3 элементами, где каждый элемент инициализируется, выберите MULTI для Init Allocated и ввода 3 для # Allocated Objects.
Запустите верификацию и откройте результаты. На панели Source установите курсор на входных параметрах функции.
На подсказках отображаются ограничения. Для примера в предыдущем коде подсказка отображений, что val имеет значения в 1..10.

Командная строка

Используйте опцию Constraint setup (-data-range-specifications) с помощью XML- файла, задающей ваше ограничение.

Для образца, для анализа с Polyspace^® Кодируйте Prover™ Server™, задайте опцию следующим образом:

polyspace-code-prover-server -sources filename -data-range-specifications "C:\Polyspace\drs_project1.xml"

Создайте пустой шаблон ограничения, как описано в разделе «Задание внешних ограничений». В файле XML найдите и ограничьте входные параметры функции. Входные параметры функции появляются как scalar или pointer тег в function тег. Входы называются как arg1, arg2 и так далее. Например, для предыдущего кода, XML-структура для входов func появляются следующим образом:

<function name="func" line="1" attributes="unused" main_generator_called="MAIN_GENERATOR" comment="">
     <scalar name="arg1" line="1" base_type="int32" complete_type="int32" init_mode="INIT" init_range="1..10" />
     <pointer name="arg2" line="1" complete_type="int32 *" init_mode="INIT" initialize_pointer="Not NULL" number_allocated="3" init_pointed="MULTI">  
         <scalar line="1" base_type="int32" complete_type="int32" init_mode="MAIN_GENERATOR" init_range=""/>
    </pointer>
     <scalar name="return" line="1" base_type="int32" complete_type="int32" init_mode="disabled" init_range="disabled"/>
</function>

Чтобы задать ограничение на входной параметр функции, установите атрибуты init_mode и init_range для скалярных переменных и init_pointed и number_allocated для переменных.

Чтобы ограничить val в область значений [1..10], установите init_mode атрибут тега с именем arg1 на INIT и init_range на 1..10.
Чтобы указать, что ptr указывает на массив с 3 элементами, где каждый элемент инициализируется, задайте init_mode атрибут тега с именем arg2 на INIT, init_pointed на MULTI и number_allocated на 3.

См. также

Constraint setup (-data-range-specifications)

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