Для более точного анализа Программы автоматического доказательства Кода можно задать ограничения (также известный как спецификации области значений данных или DRS) на входных параметрах функции. Программа автоматического доказательства кода проверяет ваше функциональное определение на ошибки времени выполнения относительно ограниченных входных параметров. Для общего рабочего процесса смотрите, Задают Внешние Ограничения.
Например, для функции, определяемой можно следующим образом, можно указать что аргумент val имеет значения в области значений [1..10]. Можно также указать что аргумент ptr точки к массиву с 3 элементами, где каждый элемент инициализируется:
int func(int val, int* ptr) {
.
.
}
Задавать ограничения на входные параметры функции:
В вашей настройке проекта выберите Inputs & Stubbing. Нажмите
кнопку для Constraint setup.
В окне Constraint Specification щелкнуть
.
Под узлом User Defined Functions вы видите список функций, входные параметры которых могут быть ограничены.
Расширьте узел для каждой функции.
Вы видите каждый входной параметр функции на отдельной строке. Входные параметры имеют синтаксис function_name.arg1FunctionName .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® 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)