Карта неточно анализируемая функция к стандартной функции для точного анализа
-code-behavior-specifications
file1
[, file2
, [...]]
-code-behavior-specifications
задает XML-файлы, которые позволяют вам сопоставлять поведения с элементами вашего кода. Например, вы можете:file1
[, file2
, [...]]
Сопоставьте свои библиотечные функции с соответствующими стандартными функциями, которые распознает Polyspace®. Отображение со стандартными библиотечными функциями может помочь с улучшением точности или автоматическим обнаружением новых потоков.
Задайте функцию, как запрещено.
Если при запуске верификацию из командной строки, задаете абсолютный путь к XML-файлам или пути относительно папки, от которой вы запускаете команду. Если при запуске верификацию от пользовательского интерфейса (только десктопные решения), задаете опцию наряду с абсолютным путем к XML-файлу в поле Other. Смотрите Other
.
Демонстрационный файл шаблона code-behavior-specifications-sample.xml
показывает синтаксис XML. Файл находится в
где polyspaceroot
\polyspace\verifier\cxx\
папка установки Polyspace. polyspaceroot
Синтаксис XML: <имя функции = "
custom_function
"станд. = "std_function
"> </функция>
Используйте эту запись в XML-файле, чтобы сократить количество оранжевых проверок от неточного анализа Программы автоматического доказательства Кода вашей функции (или ложные отрицательные стороны от неточного анализа Средства поиска Ошибки). Иногда, верификация не анализирует определенные виды функций точно из-за свойственных ограничений в статической верификации. В тех случаях, если вы находите стандартную функцию, которая является близким аналогом вашей функции, используйте это отображение. Хотя ваша функция сама не анализируется, анализ более точен в местоположениях, где вы вызываете функцию. Например, если верификация не может анализировать ваш функциональный cos32
точно и рассматривает полный спектр для его возвращаемого значения, сопоставьте его с cos
функция для возвращаемого значения в [-1,1].
Верификация игнорирует тело вашей функции. Однако верификация эмулирует ваше функциональное поведение следующими способами:
Верификация принимает те же возвращаемые значения для вашей функции как стандартная функция.
Например, если вы сопоставляете свой функциональный cos32
к стандартной функции cos
, верификация принимает тот cos32
возвращает значения в [-1,1].
Верификация проверяет на те же проблемы, как она сверяется со стандартной функцией.
Например, если вы сопоставляете свой функциональный acos32
к стандартной функции acos
, Invalid use of standard library routine
проверка определяет если аргумент acos32
находится в [-1,1].
Функции, которые можно сопоставить, чтобы включать:
Стандартные библиотечные функции от math.h
.
Управление памятью функционирует от string.h
.
__ps_meminit
: Функционально-специализированное к Polyspace, который инициализирует область памяти.
Иногда, верификация не распознает, что ваша инициализация памяти функционирует, и производит оранжевый Non-initialized local variable
проверьте переменную, которую вы инициализировали через эту функцию. Если вы знаете, что ваша функция инициализации памяти инициализирует переменную через свой адрес, сопоставьте свою функцию с __ps_meminit
. Проверка становится зеленой.
__ps_lookup_table_clip
: Функционально-специализированное к Polyspace, который возвращает значение в области значений входного массива.
Иногда, верификация рассматривает полный спектр для возвращаемых значений функций, которые ищут значения в больших массивах (функции интерполяционной таблицы). Если вы знаете, что возвращаемое значение функции интерполяционной таблицы должно быть в области значений значений в ее входном массиве, сопоставьте функцию с __ps_lookup_table_clip
.
В коде, сгенерированном из моделей, верификация по умолчанию делает это предположение для функций интерполяционной таблицы. Чтобы идентифицировать, использует ли интерполяционная таблица линейную интерполяцию и никакую экстраполяцию, верификация использует имена функций. Используйте отображение только в рукописных функциях, например, функциях в блоке S-Function C/C++. Имена тех функций не следуют определенным соглашениям. Необходимо явным образом задать их.
См. также Расширяют Средства проверки Средства поиска Ошибки для Стандартных Библиотечных функций к Пользовательским Библиотекам (Polyspace Bug Finder).
Синтаксис XML: <имя функции = "
custom_function
"станд. = "std_function
"> </функция>
Используйте эту запись в XML-файле для автоматического обнаружения функций создания потока и функций, которые начинают и заканчивают критические разделы. Polyspace поддерживает автоматическое обнаружение для определенных семейств многозадачных примитивов только. Расширьте поддержку с помощью этой записи XML.
Если ваша функция создания потока, например, не принадлежит одному из поддерживаемых семейств, сопоставьте свою функцию с поддерживаемым примитивным параллелизмом.
Смотрите расширяют средства проверки дефекта параллелизма к неподдерживаемым средам многопоточности (Polyspace Bug Finder).
Этот раздел применяется только к анализу Средства поиска Ошибки.
Синтаксис XML: <имя функции = "
function_name
"поведение = "FORBIDDEN_FUNC"> </функция>
Используйте эту запись в XML-файле, чтобы задать список функций, которые вы хотите запретить из своего исходного кода.
Смотрите флаг или небезопасные функции устаревшие Используя средства проверки средства поиска ошибки (Polyspace Bug Finder).
Примеры в следующих разделах относятся к анализу Программы автоматического доказательства Кода. Для примеров Средства поиска Ошибки см.:
Расширьте средства проверки средства поиска ошибки для стандартных библиотечных функций к пользовательским библиотекам (Polyspace Bug Finder)
Отметьте или небезопасные функции устаревшие Используя средства проверки средства поиска ошибки (Polyspace Bug Finder)
Расширьте средства проверки дефекта параллелизма к неподдерживаемым средам многопоточности (Polyspace Bug Finder)
Можно адаптировать демонстрационный XML-файл отображения, которому предоставляют установку Polyspace, и сопоставить функцию со стандартной функцией.
Предположим, что верификация по умолчанию производит оранжевый User assertion
проверьте этот код:
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
проверяйте зеленые повороты. Верификация принимает что возвращаемое значение 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
проверка покраснела. В противном случае верификация не проверяет ли аргумент 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
проверяйте зеленые повороты. Верификация принимает что возвращаемое значение 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
проверяйте зеленые повороты. Верификация принимает что все поля структуры 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
проверка покраснела. Верификация принимает это только поле 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;