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

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