Exponenta Banner

Внешние ограничения для анализа Polyspace

Для более точного анализа с Polyspace® можно задать внешние ограничения на:

  • Глобальные переменные.

  • Пользовательские функции.

    Ограничения на пользовательские функции не применяются к анализу Средства поиска Ошибки.

  • Заблокированные функции.

    Ограничения на заблокированные функции не применяются к анализу Средства поиска Ошибки.

Для получения дополнительной информации смотрите, Задают Внешние Ограничения. Для частичного списка ограничений смотрите Ограничительные Ограничения Спецификации.

В пользовательском интерфейсе десктопных решений Polyspace можно задать ограничения через окно Constraint Specification. Ограничения сохранены в XML-файле, который можно снова использовать для других проектов.

Эта таблица объясняет различные столбцы в окне Constraint Specification. Если вы непосредственно редактируете ограничительный XML-файл, чтобы задать ограничение (например, в Серверных продуктах Polyspace), эта таблица также показывает соответствие между столбцами в пользовательском интерфейсе и записями в XML-файле. Запись XML, подсвеченная полужирным, появляется в соответствующем столбце окна Constraint Specification.

СтолбецНастройкиЗапись XML-файла
Name

Отображает список переменных и функций в вашем Проекте, для которого можно указать диапазоны данных.

Это Отображения столбца три расширяемых пункта меню:

  • Глобальные переменные – глобальные переменные Отображений в проекте.

  • Определяемые пользователем функции – Отображения пользовательские функции в проекте. Расширьте имя функции, чтобы видеть его входные параметры.

  • Заблокированные функции – Отображения список интерфейсных функций в проекте. Расширьте имя функции, чтобы видеть входные параметры и возвращаемые значения.

<function name = "funcName" ...>

<scalar name = "arg1" ...>

<pointer name = "arg2" ...>

FileОтображает имя исходного файла, содержащего переменную или функцию. 
<file name = "C:\Project1\Sources\file.c" ...>
Attributes

Информация об отображениях о переменной или функции.

Например, статические переменные отображают static. Невостребованные функции отображают unused.

 
<function name="funcName" attributes="unused" ...>
Data TypeОтображает тип переменной. 
<scalar name="arg1" complete_type="int32" ...>
Main Generator Called

Применимый только для пользовательских функций.

Задает, вызывает ли основной генератор функцию:

  • MAIN GENERATOR – Основной генератор может вызвать эту функцию, в зависимости от значения -functions-called-in-loop (C) или -main-generator-calls (C++) параметр.

  • NO – Основной генератор не вызовет эту функцию.

  • YES – Основной генератор вызовет эту функцию. 

<function name="funcName" main_generator_called="MAIN_GENERATOR" ...>
Init Mode

Задает, как программное обеспечение присваивает область значений переменной:

  • MAIN GENERATOR – Переменный диапазон присвоен в зависимости от настроек основных опций генератора -main-generator-writes-variables и -no-def-init-glob.

  • IGNORE – Переменная не присвоена никакой области значений, даже если диапазон указан.

  • INIT – Переменная присвоена заданной области только при инициализации и сохраняет область значений до первой записи.

  • PERMANENT – Переменная постоянно присвоена заданной области. Если переменная присвоена вне этой области значений во время программы, никакое предупреждение не обеспечивается. Используйте globalassert режим, если вам нужно предупреждение.

Пользовательские функции поддерживают только INIT режим.

Интерфейсные функции поддерживают только PERMANENT режим.

Для верификаций C глобальные указатели поддерживают MAIN GENERATOR, IGNORE, или INIT режим.

  • MAIN GENERATOR – Указатель следует опциям основного генератора.

  • IGNORE – Указатель не инициализируется

  • INIT – Задайте, является ли указателем NULL, и как резкий объект выделяется (Инициализируйте Указатель и Init Выделенные опции).

 
<scalar name="arg1" init_mode="INIT" ...>
Init Range

Задает минимальные и максимальные значения для переменной.

Можно использовать ключевые слова min и max обозначить минимальные и максимальные значения типа переменной. Например, для типа долго, min и max соответствуйте-2^31 и 2^31-1 соответственно.

Можно также использовать шестнадцатеричные значения. Например: 0x12..0x100

Для enum переменные, вы не можете указать диапазоны непосредственно с помощью констант перечислителя. Вместо этого используйте значения, представленные константами.

Для enum переменные, можно также использовать ключевые слова enum_min и enum_max обозначить минимальные и максимальные значения, которые может принять переменная. Например, для enum переменная типа, заданного ниже, enum_min 0 и enum_max 5:

enum week{ sunday, monday=0, tuesday, wednesday, thursday, friday, saturday};

 
<scalar name="arg1" init_range="-1..0"...>
Initialize Pointer

Применимый только к указателям. Enabled только, когда вы задаете Init Mode:INIT.

Задает, должен ли указателем быть NULL:

  • May-be NULL – Указателем мог потенциально быть Нулевой указатель (или не).

  • Not Null – Указатель никогда не инициализируется как нулевой указатель.

  • Null – Указатель инициализируется как NULL.

Примечание

Не применимый для проектов C++. Смотрите Ограничительные Ограничения Спецификации.

 
<pointer name="arg1" initialize_pointer="Not NULL"...>
Init Allocated

Применимый только к указателям. Enabled только, когда вы задаете Init Mode:INIT.

Задает, как резкий объект выделяется:

  • MAIN GENERATOR – Резкий объект выделяется основным генератором.

  • NONE – Резкий объект не записан.

  • SINGLE – Резкий объект или первый элемент массива инициализируются.

  • MULTI – Все объекты (или элементы массива) инициализируются.

Кроме того, две других опции доступны для аргументов указателя к заблокированным функциям:

  • SINGLE_CERTAIN_WRITE – Резкий объект или первый элемент массива инициализируются заблокированной функцией.

  • MULTI_CERTAIN_WRITE – Все резкие объекты (или элементы массива) инициализируются заблокированной функцией.

Для заблокированных функций, опции SINGLE и MULTI означайте вероятную инициализацию вместо определенной инициализации.

Примечание

Не применимый для проектов C++. Смотрите Ограничительные Ограничения Спецификации.

 
<pointer name="arg1" init_pointed="MAIN_GENERATOR"...>
# Allocated Objects

Применимый только к указателям.

Задает, на сколько объектов указывает указатель (резкий объект рассматривается как массив).

Параметр Init Allocated задает, сколько выделенных объектов на самом деле инициализируется. Например, рассмотрите этот код:

void func(int *ptr) {
    assert(ptr[0]==1);
    assert(ptr[1]==1);
}
Если вы задаете эти ограничения:

  • ptr установили Init Allocated на MULTI и набор # Allocated Objects к 2,

  • *ptr установили Init Range на 1..1,

оба утверждения являются зелеными. Однако, если вы задаете эти ограничения:

  • ptr установили Init Allocated на SINGLE

  • *ptr установили Init Range на 1..1,

второе утверждение является оранжевым. Только первый объект, что ptr точки к инициализированному к 1. Объекты вне первого могут быть потенциально полным спектром.

Примечание

Не применимый для проектов C++. Смотрите Ограничительные Ограничения Спецификации.

 
<pointer name="arg1" number_allocated="10"...>
Global AssertЗадает, выполнить ли утверждение, проверяют переменную при глобальной инициализации, и после каждого присвоения. 
<scalar name="glob" global_assert="YES"...>
Global Assert RangeЗадает минимальные и максимальные значения для области значений, которую вы хотите проверять. 
<scalar name="glob" assert_range="0..200"...>
CommentКомментарии, что вы вводите, например, выравнивание для своих значений DRS. 
<scalar name="glob" comment="Speed Range"...>

Ограничительные ограничения спецификации

Вы не можете задать эти ограничения:

  • Указатели C++ не могут быть ограничены:

    На C++ вы не можете ограничить аргументы указателя функций. Функции, которые имеют аргументы указателя только, не появляются в ограничительном интерфейсе спецификации.

    Из-за полиморфизма указатель C++ может указать на объекты нескольких классов в иерархии классов и может потребовать вызывающих различных конструкторов. Предварительный анализ для ограничительной спецификации не может определить который тип объекта ограничить или который конструктор вызвать.

  • Ограничения не могут быть отношениями:

    Вы не можете задать ограничение, которое связывает возвращаемое значение функции к ее входным параметрам. Можно только указать постоянный диапазон для ограничений.

  • Несколько областей значений, не возможных:

    Вы не можете указать несколько диапазонов для ограничения. Например, вы не можете указать, что аргумент функции имеет или значение-1 или значение в области значений [1,100]. Вместо этого укажите диапазон [-1 100] или выполните два отдельных исследования, однажды со значением-1 и однажды с областью значений [1,100].

Похожие темы

Документация Polyspace Code Prover Server

Поддержка