Можно наложить ограничения (также известные как спецификации диапазона данных или DRS) на диапазон глобальной переменной и проверить с помощью средства проверки кода, нарушают ли операции записи для переменной ограничение. Общие сведения о рабочем процессе см. в разделе Указание внешних ограничений.
Чтобы ограничить диапазон глобальных переменных, а также проверить нарушение ограничения:
В конфигурации проекта выберите «Входы и заглушки». Нажмите
кнопку рядом с полем Настройка ограничения.
В окне Спецификация ограничения (Constraint Specification) щелкните значок.
В узле Глобальные переменные (Global Variables) отображается список глобальных переменных.
Для глобальной переменной, которую требуется ограничить:
В раскрывающемся списке в столбце Global Assert выберите YES.
В столбце Глобальный диапазон подтверждения введите диапазон в формате min..maxmin - минимальное значение и max максимальное значение для глобальной переменной.
Для сохранения спецификаций нажмите
кнопку.
В окне Сохранить файл ограничений сохраните записи как xml файл.
Выполните проверку и откройте результаты.
Для каждой операции записи глобальной переменной отображается зеленая, оранжевая или красная проверка состояния корректности. Если проверка:
Зеленая, переменная находится в указанном диапазоне.
Оранжевая, переменная может находиться вне указанного диапазона.
Красный, переменная находится вне указанного диапазона.
При записи двух или более задач в одну и ту же глобальную переменную проверка условия Корректность может выглядеть оранжевым на всех операциях записи в переменную, даже если только одна операция записи выводит переменную за пределы диапазона Global Assert.
Использовать опцию 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-файле найдите и ограничьте глобальные переменные. XML-теги для глобальных переменных отображаются непосредственно в пределах file тег без вложенного function тег. Например, в этом ограничении XML, PowerLevel и SHR являются глобальными переменными:
<file name="\\\\home\\johndoe\\Documents\\Polyspace_Workspace\\Examples\\Code_Prover_Example\\sources\\tasks1.c">
<scalar name="PowerLevel" line="26" ... global_assert="YES" assert_range="0..10" />
<scalar name="SHR" line="30" ... global_assert="NO" assert_range="" />
<function name="Tserver" line="73" .../>
<function name="initregulate" line="47" .../>
<function name="orderregulate" line="35" ...>
<scalar name="return" ... global_assert="unsupported" assert_range="unsupported" />
</function>
<function name="proc1" line="101" .../>
</file>Чтобы задать ограничение для глобальной переменной и проверить во время анализа проверки кода, нарушено ли ограничение, выполните следующие действия.
Установите global_assert атрибут переменной scalar тег для YES.
Установите assert_range атрибут диапазону в форме min..max0..10.
В предыдущем примере переменная PowerLevel ограничивается таким образом.