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

Например, если вы сопоставляете свой функциональный 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++. Имена тех функций не следуют определенным соглашениям. Необходимо явным образом задать их.

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

my_sqrt → sqrt:

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

my_lookup_table (аргумент 2) →__ps_lookup_table_clip (аргумент 1):

Если вы используете отображение, проверка User assertion становится зеленой. Верификация принимает, что возвращаемым значением my_lookup_table является в области значений массива интерполяционной таблицы table.

my_meminit →__ps_meminit:

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

my_meminit →__ps_meminit:

Если вы используете отображение, проверка Non-initialized local variable покраснела. Верификация принимает, что только поле field1 структуры x инициализируется с допустимыми значениями.

Функция создания потока: createTask → pthread_create

Функция, которая начинает критический раздел: takeLock → pthread_mutex_lock

Функция, которая заканчивает критический раздел: releaseLock → pthread_mutex_unlock

Перед отображением:

Анализ не обнаруживает гонку данных на var2.

typedef void* (*FUNT) (void*);

extern int takeLock(int* t);
extern int releaseLock(int* t);
// First argument is the function, second the id
extern int createTask(FUNT,int*,int*,void*);

int t_id1,t_id2;
int lock;

int var1; 
int var2; 

void* task1(void* a) {
    takeLock(&lock);
    var1++;
    var2++;
    releaseLock(&lock);
    return 0;
}

void* task2(void* a) {
    takeLock(&lock);
    var1++;
    releaseLock(&lock);
    var2++;
    return 0;
}

void main() {
    createTask(task1,&t_id1,0,0);
    createTask(task2,&t_id2,0,0);
}

Отображение спецификации:

На основе номера и типа параметров функционального createTask, удобно сопоставить createTask с функцией создания потока pthread_create. Другие доступные альтернативы, createThread или OSTaskCreate, имеют различные типы аргумента.

Сопоставляя с pthread_create, переотображение аргумента требуется, потому что аргументы не соответствуют точно. Поток запускается, стандартная программа является третьим аргументом pthread_create, но первым аргументом createTask.

<function name="createTask" std="pthread_create" >
    <mapping std_arg="1" arg="2"></mapping>
    <mapping std_arg="3" arg="1"></mapping>
    <mapping std_arg="2" arg="3"></mapping>
    <mapping std_arg="4" arg="4"></mapping>
</function>
<function name="takeLock" std="pthread_mutex_lock" >
</function>
<function name="releaseLock" std="pthread_mutex_unlock" >
</function>

Для списка поддерживаемых функций, с которыми можно сопоставить, смотрите, что демонстрационное сопоставляет файл function-behavior-specifications-sample.xml в polyspaceroot\polyspace\verifier\cxx\. polyspaceroot является папкой установки Polyspace, такой как C:\Program Files\Polyspace\R2019a. См. также Автоматическое обнаружение Создания Потока и Критического Раздела в Polyspace.

После отображения:

Анализ обнаруживает гонку данных на var2.

typedef void* (*FUNT) (void*);

extern int takeLock(int* t);
extern int releaseLock(int* t);
// First argument is the function, second the id
extern int createTask(FUNT,int*,int*,void*);

int t_id1,t_id2;
int lock;

int var1; 
int var2; 

void* task1(void* a) {
    takeLock(&lock);
    var1++;
    var2++;
    releaseLock(&lock);
    return 0;
}

void* task2(void* a) {
    takeLock(&lock);
    var1++;
    releaseLock(&lock);
    var2++;
    return 0;
}

void main() {
    createTask(task1,&t_id1,0,0);
    createTask(task2,&t_id2,0,0);
}