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

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

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

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

В строение проекта выберите 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^® Кодируйте Prover™ Server™, задайте опцию следующим образом:

polyspace-code-prover-server -sources filename -data-range-specifications "C:\Polyspace\drs_project1.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>

Чтобы задать ограничение для глобальной переменной и проверить во время анализа Code Prover, если ограничение нарушено:

Установите global_assert атрибут scalar переменной тег к YES.
Установите assert_range атрибут области значений в форме min. max, для образца, 0..10.

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

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