-code-behavior-specifications

Карта неточно анализируемая функция к стандартной функции для точного анализа

Синтаксис

-code-behavior-specifications file1[, file2, [...]]

Описание

-code-behavior-specifications file1[, file2, [...]] задает XML-файлы, которые позволяют вам сопоставлять поведения с элементами вашего кода. Например, вы можете:

Сопоставьте свои библиотечные функции с соответствующими стандартными функциями, которые распознает Polyspace^®. Отображение со стандартными библиотечными функциями может помочь с улучшением точности или автоматическим обнаружением новых потоков.
Укажите, что функция имеет специальное поведение или должна быть подвергнута специальным проверкам.
Например, можно указать, что функция должна только взять адреса инициализированных переменных в качестве аргументов, или что функция не должна использоваться в целом.

Если при запуске верификацию из командной строки, задаете абсолютный путь к XML-файлам или пути относительно папки, от которой вы запускаете команду. Если при запуске верификацию от пользовательского интерфейса (только десктопные решения), задаете опцию наряду с абсолютным путем к XML-файлу в поле Other. Смотрите Other.

Демонстрационный файл шаблона code-behavior-specifications-sample.xml показывает синтаксис XML. Файл находится в polyspaceroot\polyspace\verifier\cxx\ где polyspaceroot папка установки Polyspace.

Используя опцию для улучшения точности

Синтаксис XML: <имя функции = "custom_function"станд. = "std_function"> </функция>

Используйте эту запись в XML-файле, чтобы сократить количество оранжевых проверок от неточного анализа Программы автоматического доказательства Кода вашей функции (или ложные отрицательные стороны от неточного анализа Средства поиска Ошибки). Иногда, верификация не анализирует определенные виды функций точно из-за свойственных ограничений в статической верификации. В тех случаях, если вы находите стандартную функцию, которая является близким аналогом вашей функции, используйте это отображение. Хотя ваша функция сама не анализируется, анализ более точен в местоположениях, где вы вызываете функцию. Например, если верификация не может анализировать ваш функциональный cos32 точно и рассматривает полный спектр для его возвращаемого значения, сопоставьте его с cos функция для возвращаемого значения в [-1,1].

Верификация игнорирует тело вашей функции. Однако верификация эмулирует ваше функциональное поведение следующими способами:

Верификация принимает те же возвращаемые значения для вашей функции как стандартная функция.
Например, если вы сопоставляете свой функциональный cos32 к стандартной функции cos, верификация принимает тот cos32 возвращает значения в [-1,1].
Верификация проверяет на те же проблемы, как она сверяется со стандартной функцией.
Например, если вы сопоставляете свой функциональный acos32 к стандартной функции acos, Invalid use of standard library routine (Polyspace Code Prover Access) проверка определяет если аргумент acos32 находится в [-1,1].

Функции, которые можно сопоставить, чтобы включать:

Стандартные библиотечные функции от math.h.
Управление памятью функционирует от string.h.
__ps_meminit: Функционально-специализированное к Polyspace, который инициализирует область памяти.
Иногда, верификация не распознает, что ваша инициализация памяти функционирует, и производит оранжевый Non-initialized local variable (Polyspace Code Prover Access) проверяет переменную, которую вы инициализировали через эту функцию. Если вы знаете, что ваша функция инициализации памяти инициализирует переменную через свой адрес, сопоставьте свою функцию с __ps_meminit. Проверка становится зеленой.
__ps_lookup_table_clip: Функционально-специализированное к Polyspace, который возвращает значение в области значений входного массива.
Иногда, верификация рассматривает полный спектр для возвращаемых значений функций, которые ищут значения в больших массивах (функции интерполяционной таблицы). Если вы знаете, что возвращаемое значение функции интерполяционной таблицы должно быть в области значений значений в ее входном массиве, сопоставьте функцию с __ps_lookup_table_clip.
В коде, сгенерированном из моделей, верификация по умолчанию делает это предположение для функций интерполяционной таблицы. Чтобы идентифицировать, использует ли интерполяционная таблица линейную интерполяцию и никакую экстраполяцию, верификация использует имена функций. Используйте отображение только для рукописных функций, например, функций в блоке S-Function (Simulink) C/C++. Имена тех функций не следуют определенным соглашениям. Необходимо явным образом задать их.

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

Используя опцию для обнаружения параллелизма

Синтаксис XML: <имя функции = "custom_function"станд. = "std_function"> </функция>

Используйте эту запись в XML-файле для автоматического обнаружения функций создания потока и функций, которые начинают и заканчивают критические разделы. Polyspace поддерживает автоматическое обнаружение для определенных семейств многозадачных примитивов только. Расширьте поддержку с помощью этой записи XML.

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

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

Используя опцию для помещения в черный список функций

Этот раздел применяется только к анализу Средства поиска Ошибки.

Синтаксис XML:

<function name="function_name">
   <behavior name="FORBIDDEN_FUNC">
</function>

Используйте эту запись в XML-файле, чтобы задать, не должна ли функция использоваться в вашем исходном коде.

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

Используя опцию для расширения проверок инициализации

Синтаксис XML:

<function name="function_name">
   <check name="ARGUMENT_POINTS_TO_INITIALIZED_VALUE" arg="n"/>
</function>

Номер n задает, какой аргумент должен проверяться на буферную инициализацию.

Используйте эту запись в XML-файле, чтобы задать, должен ли аргумент указателя к функции указать на инициализированный буфер.

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

Примеры

Примеры в следующих разделах относятся к анализу Программы автоматического доказательства Кода. Для примеров Средства поиска Ошибки см.:

Задайте отображение со стандартной функцией

Можно адаптировать демонстрационный XML-файл отображения, которому предоставляют установку Polyspace, и сопоставить функцию со стандартной функцией.

Предположим, что верификация по умолчанию производит оранжевый User assertion (Polyspace Code Prover Access) проверяет этот код:

double x = acos32(1.0) ;  
assert(x <= 2.0);

Предположим, что вы знаете что функциональный acos32 ведет себя как функциональный acos и возвращаемое значение 0. Вы ожидаете проверку на assert оператор, чтобы быть зеленым. Однако верификация рассматривает тот acos32 возвращает любое значение в области значений типа double потому что acos32 точно не анализируется. Проверка является оранжевой. Сопоставлять ваш функциональный acos32 к acos:

Скопируйте файл code-behavior-specifications-sample.xml от polyspaceroot\polyspace\verifier\cxx\ к другому местоположению, например, "C:\Polyspace_projects\Common\Config_files". Измените полномочия записи на файле.
Чтобы сопоставить вашу функцию со стандартной функцией, измените содержимое XML-файла. Сопоставлять ваш функциональный acos32 к стандартной библиотечной функции acos, измените следующий код:
```
<function name="my_lib_cos" std="acos"> </function>
```
К:
```
<function name="acos32" std="acos"> </function>
```

Задайте местоположение файла для верификации:

Программа автоматического доказательства кода:

polyspace-code-prover -code-behavior-specifications "C:\Polyspace_projects\Common\Config_files\code-behavior-specifications-sample.xml"

Сервер программы автоматического доказательства кода:

polyspace-code-prover-server -code-behavior-specifications "C:\Polyspace_projects\Common\Config_files\code-behavior-specifications-sample.xml"

Задайте отображение со стандартной функцией с переотображением аргумента

Иногда, аргументы вашей функции не сопоставляют непосредственный с аргументами стандартной функции. В тех случаях повторно сопоставьте свой аргумент функции с аргументом стандартной функции. Например:

__ps_lookup_table_clip:
Это функционально-специализированное к Polyspace берет только массив интерполяционной таблицы в качестве аргумента и возвращает значения в области значений интерполяционной таблицы. Ваша интерполяционная таблица функциональная сила имеет дополнительные аргументы помимо самого массива интерполяционной таблицы. В этом случае используйте переотображение аргумента, чтобы задать, какой аргумент вашей функции является массивом интерполяционной таблицы.
Например, предположите функциональный my_lookup_table имеет следующее объявление:
```
double my_lookup_table(double u0, const real_T *table,
                                     const double *bp0);
```
Второй аргумент вашего функционального my_lookup_table массив интерполяционной таблицы. В файле code-behavior-specifications-sample.xml, добавьте этот код:
```
<function name="my_lookup_table" std="__ps_lookup_table_clip">
    <mapping std_arg="1" arg="2"></mapping>
</function>
```
Когда вы вызываете функцию:
```
res = my_lookup_table(u, table10, bp);
```
Верификация интерпретирует вызов как:
```
res =__ps_lookup_table_clip(table10);
```
Верификация принимает что значение res находится в области значений значений в table10.
__ps_meminit:
Это функционально-специализированное к Polyspace берет адрес памяти в качестве первого аргумента и многие байты в качестве второго аргумента. Функция принимает, что байты в памяти, начинающей с адреса памяти, инициализируются допустимым значением. Ваша инициализация памяти функциональная сила имеет дополнительные аргументы. В этом случае используйте переотображение аргумента, чтобы задать, какой аргумент вашей функции является начальным адресом и какой аргумент является количеством байтов.
Например, предположите функциональный my_meminit имеет следующее объявление:
```
     void my_meminit(enum InitKind k, void* dest, int is_aligned, unsigned int size);
```
Второй аргумент вашей функции является начальным адресом, и четвертый аргумент является количеством байтов. В файле code-behavior-specifications-sample.xml, добавьте этот код:
```
<function name="my_meminit" std="__ps_meminit">
    <mapping std_arg="1" arg="2"></mapping>
    <mapping std_arg="2" arg="4"></mapping>
</function>
```
Когда вы вызываете функцию:
```
my_meminit(INIT_START_BY_END, &buffer, 0, sizeof(buffer));
```
Верификация интерпретирует вызов как:
```
__ps_meminit(&buffer, sizeof(buffer));
```
Верификация принимает тот sizeof(buffer) количество байтов, начинающих с &buffer инициализируются.
memset: Переменное количество аргументов.
Если ваша функция имеет переменное количество аргументов, вы не можете сопоставить его непосредственно со стандартной функцией без явного переотображения аргумента. Например, скажите, что ваша функция объявляется как:
```
void* my_memset(void*, int, size_t, ...)
```
Сопоставлять функцию с memset функция, используйте следующее отображение:
```
<function name="my_memset" std="memset">
    <mapping std_arg="1" arg="1"></mapping>
    <mapping std_arg="2" arg="2"></mapping>
    <mapping std_arg="3" arg="3"></mapping>
</function>
```

Эффект отображения на точности

Эти примеры показывают результат отображения определенных функций к стандартным функциям:

my_acos → acos:
Если вы используете отображение, User assertion (Polyspace Code Prover Access) проверка становится зеленым. Верификация принимает что возвращаемое значение my_acos 0.
- Перед отображением:
```
double x = my_acos(1.0);  
assert(x <= 2.0);
```
- Отображение спецификации:
```
<function name="my_acos" std="acos">
</function>
```
- После отображения:
```
double x = my_acos(1.0);  
assert(x <= 2.0);
```
my_sqrt → sqrt:
Если вы используете отображение, Invalid use of standard library routine (Polyspace Code Prover Access) проверка покраснел. В противном случае верификация не проверяет ли аргумент my_sqrt является неотрицательным.
- Перед отображением:
```
res = my_sqrt(-1.0);
```
- Отображение спецификации:
```
<function name="my_sqrt" std="sqrt"> 
</function>
```
- После отображения:
```
res = my_sqrt(-1.0);
```
my_lookup_table (аргумент 2) →__ps_lookup_table_clip (аргумент 1):
Если вы используете отображение, User assertion (Polyspace Code Prover Access) проверка становится зеленым. Верификация принимает что возвращаемое значение my_lookup_table в области значений массива интерполяционной таблицы table.
- Перед отображением:
```
double table[3] = {1.1, 2.2, 3.3}
.
.
double res = my_lookup_table(u, table, bp);
assert(res >= 1.1 && res <= 3.3);
```
- Отображение спецификации:
```
<function name="my_lookup_table" std="__ps_lookup_table_clip">
    <mapping std_arg="1" arg="2"></mapping>
</function>
```
- После отображения:
```
double table[3] = {1.1, 2.2, 3.3}
.
.
res_real = my_lookup_table(u, table9, bp);
assert(res_real >= 1.1 && res_real <= 3.3);
```
my_meminit →__ps_meminit:
Если вы используете отображение, Non-initialized local variable (Polyspace Code Prover) проверка становится зеленым. Верификация принимает что все поля структуры x инициализируются допустимыми значениями.
- Перед отображением:
```
struct X {
  int field1 ;
  int field2 ;
};
.
.
struct X x;
my_meminit(&x, sizeof(struct X));
return x.field1;
```
- Отображение спецификации:
```
<function name="my_meminit" std="__ps_meminit">
     <mapping std_arg="1" arg="1"></mapping>
     <mapping std_arg="2" arg="2"></mapping>
</function>
```
- После отображения:
```
struct X {
  int field1 ;
  int field2 ;
};
.
.
struct X x;
my_meminit(&x, sizeof(struct X));
return x.field1;
```
my_meminit →__ps_meminit:
Если вы используете отображение, Non-initialized local variable (Polyspace Code Prover Access) проверка покраснел. Верификация принимает это только поле field1 из структуры x инициализируется допустимыми значениями.
- Перед отображением:
```
struct X {
  int field1 ;
  int field2 ;
};
.
.
struct X x;
my_meminit(&x, sizeof(int));
return x.field2;
```
- Отображение спецификации:
```
<function name="my_meminit" std="__ps_meminit">
</function>
```
- После отображения:
```
struct X {
  int field1 ;
  int field2 ;
};
.
.
struct X x;
my_meminit(&x, sizeof(int));
return x.field2;
```

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