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

Например, если вы сопоставили свою функцию cos32 к стандартной функции cos, верификация принимает, что cos32 возвращает значения в [-1,1].

В верификацию проверяются те же проблемы, что и при проверке стандартной функцией.

Например, если вы сопоставили свою функцию acos32 к стандартной функции acos, а Invalid use of standard library routine (Polyspace Code Prover) проверка определяет, является ли аргумент acos32 находится в [-1,1].

Стандартные функции библиотеки от math.h.

Функции управления памятью от string.h.

__ps_meminit: Функция, специфичная для Polyspace, которая инициализирует область памяти.

Иногда верификация не распознает функцию инициализации памяти и производит оранжевый Non-initialized local variable (Polyspace Code Prover) проверяйте переменную, которую вы инициализировали с помощью этой функции. Если вы знаете, что ваша функция инициализации памяти инициализирует переменную через ее адрес, сопоставьте вашу функцию с __ps_meminit. Чек становится зеленым.

__ps_lookup_table_clip: Функция, специфичная для Polyspace, которая возвращает значение в области значений входного массива.

Иногда верификация рассматривает полную область значений для возвращаемых значений функций, которые ищут значения в больших массивах (функции интерполяционной таблицы). Если вы знаете, что возврат значение функции интерполяционной таблицы должно находиться в области значений в его входе массиве, сопоставьте функцию с __ps_lookup_table_clip.

В коде, сгенерированном из моделей, верификация по умолчанию делает это предположение для функций интерполяционной таблицы. Чтобы идентифицировать, использует ли интерполяция в интерполяционной таблице, и нет экстраполяции, верификация использует имена функции. Используйте отображение только для рукописных функций, например, функций в блоке C/C + + S-Function (Simulink). Имена этих функций не соответствуют конкретным соглашениям. Они должны быть явно заданы.

NUMBER_SIGNIFICANT_CHARACTER_EXTERNAL_IDENTIFIER: Количество символов для сравнения с внешними идентификаторами. Внешние идентификаторы являются таковыми, объявленными с глобальными возможностями или классом памяти extern.

NUMBER_SIGNIFICANT_CHARACTER_INTERNAL_IDENTIFIER: Количество символов для сравнения с внутренними идентификаторами.

__ps_lookup_table_clip:

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

Например, предположим, что функция my_lookup_table имеет следующую декларацию:

double my_lookup_table(double u0, const real_T *table,
                                     const double *bp0);

<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);

__ps_meminit:

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

Например, предположим, что функция my_meminit имеет следующую декларацию:

     void my_meminit(enum InitKind k, void* dest, int is_aligned, unsigned int size);

<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));

memset: Переменное количество аргументов.

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

void* my_memset(void*, int, size_t, ...)

<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) становится зеленой. Верификация принимает, что возврат значение my_acos равен 0.

my_sqrt → sqrt:

Если вы используете отображение, Invalid use of standard library routine Проверка (Polyspace Code Prover) становится красной. В противном случае верификация не проверяет, является ли аргумент my_sqrt неотрицательная.

my_lookup_table (аргумент 2) →<reservedrangesplaceholder0> (аргумент 1):

Если вы используете отображение, User assertion Проверка (Polyspace Code Prover) становится зеленой. Верификация принимает, что возврат значение my_lookup_table находится в области значений массива интерполяционной таблицы table.

my_meminit → __ps_meminit:

Если вы используете отображение, Non-initialized local variable Проверка (Polyspace Code Prover) становится зеленой. Эта верификация принимает, что все поля структуры x инициализируются с допустимыми значениями.

my_meminit → __ps_meminit:

Если вы используете отображение, Non-initialized local variable Проверка (Polyspace Code Prover) становится красной. Эта верификация принимает, что только поле field1 структуры x инициализируется с допустимыми значениями.