Для более точного анализа Программы автоматического доказательства Кода можно задать ограничения (также известный как спецификации области значений данных или DRS) на входных параметрах функции. Программа автоматического доказательства кода проверяет ваше функциональное определение на ошибки времени выполнения относительно ограниченных входных параметров. Для общего рабочего процесса смотрите, Задают Внешние Ограничения.
Например, для функции, определяемой можно следующим образом, можно указать, что аргумент val имеет значения в области значений [1..10]. Можно также указать, что аргумент ptr указывает на массив с 3 элементами, где каждый элемент инициализируется:
int func(int val, int* ptr) {
.
.
}
Задавать ограничения на входные параметры функции:
В вашей настройке проекта выберите Inputs & Stubbing. Нажмите
кнопку для Constraint setup.
В окне Constraint Specification щелкнуть
.
Под узлом User Defined Functions вы видите список функций, входные параметры которых могут быть ограничены.
Расширьте узел для каждой функции.
Вы видите каждый входной параметр функции на отдельной строке. Входные параметры имеют синтаксис function_name.arg1function_name.arg2
Задайте свои ограничения на один или несколько входных параметров функции. Для получения дополнительной информации смотрите Внешние Ограничения для Анализа Polyspace.
Например, в предыдущем коде:
Чтобы ограничить val к области значений [1..10], выберите INIT for Init Mode и введите 1..10 для Init Range.
Чтобы указать, что ptr указывает на массив с 3 элементами, где каждый элемент инициализируется, выберите MULTI for Init Allocated и введите 3 для # Allocated Objects.
Запустите верификацию и откройте результаты. На панели Source установите свой курсор на входные параметры функции.
Подсказки отображают ограничения. Например, в предыдущем коде, отображения подсказки, что val имеет значения в 1..10.
Используйте опцию Constraint setup (-data-range-specifications) с XML-файлом, задающим ваше ограничение.
Например, для анализа с Polyspace® Code Prover™ Server™, задайте опцию можно следующим образом:
polyspace-code-prover-server -sources filename -data-range-specifications "C:\Polyspace\drs_project1.xml"
Создайте пустой ограничительный шаблон 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)