Ограничьте область значений глобальной переменной

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

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

Чтобы ограничить глобальную переменную располагаются и также проверять на нарушение ограничения:

В вашей настройке проекта выберите Inputs & Stubbing. Нажмите кнопку рядом с полем Constraint setup.
В окне Constraint Specification щелкнуть.
Под узлом Global Variables вы видите список глобальных переменных.
Для глобальной переменной, которую вы хотите ограничить:
- Из выпадающего списка в столбце Global Assert выберите YES.
- В столбце Global Assert Range введите область значений в формат min..max. min является минимальным значением и max максимальное значение для глобальной переменной.
Чтобы сохранить ваши спецификации, нажмите кнопку.
В окне Save a Constraint File сохраните свои записи как файл xml.
Запустите верификацию и откройте результаты.
Для каждой операции записи на глобальной переменной вы видите зеленую, оранжевую, или красную проверку Correctness condition. Если проверка:
- Зеленый, переменная в области значений, которую вы задали.
- Оранжевый, переменная может быть вне области значений, которую вы задали.
- Красный, переменная вне области значений, которую вы задали.
Когда две или больше задачи пишут в ту же глобальную переменную, проверка Correctness condition может казаться оранжевой на всех операциях записи к переменной, даже когда только одна операция записи берет переменную вне области значений 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..max, например, 0..10.

В предыдущем примере переменная PowerLevel ограничивается этот путь.

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