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

Например, если вы сопоставляете свой функциональный 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.

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

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) →__ps_lookup_table_clip (аргумент 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 инициализируется допустимыми значениями.