Ограничить входы функций

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

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

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

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

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

В конфигурации проекта выберите «Входы и заглушки». Нажмите кнопку настройки зависимости.
В окне Спецификация ограничения (Constraint Specification) щелкните значок.
В узле Пользовательские функции (User Defined Functions) отображается список функций, входные данные которых могут быть ограничены.
Разверните узел для каждой функции.
Каждая функция вводится в отдельной строке. Входные данные имеют синтаксис function_name.arg1, function_name.arg2и т.д.
Укажите ограничения для одного или нескольких входов функции. Дополнительные сведения см. в разделе Внешние зависимости для анализа в пространстве.
Например, в предыдущем коде:
- Ограничить val в диапазон [1..10], выберите INIT для параметра «Режим инициализации» и введите 1..10 для диапазона Init.
- Чтобы указать, что ptr указывает на 3-элементный массив, где инициализируется каждый элемент, выберите MULTI для параметра «Init Allocated» и введите 3 для # Присвоенные объекты.
Выполните проверку и откройте результаты. На панели «Источник» установите курсор на вводы функций.
В подсказках отображаются зависимости. Например, в предыдущем коде в подсказке отображается следующее: 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)

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