Чтобы настроить верификацию нескольких задач или потоков, которые выполняются одновременно, используйте опции многозадачности. Polyspace® интерпретирует определенные семейства многозадачных функций. Если вы не используете эти функции, необходимо явным образом указать, какие функции в коде указывают на точки входа, циклические задачи или прерывания. Необходимо также задать механизмы защиты для общих переменных.
Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection) | Автоматически обнаруживайте определенные семейства многопоточных функций |
External multitasking configuration | Включите настройку многозадачных строений из определений внешних файлов |
OIL files selection (-osek-multitasking) | Настройте строение многозадачности из определения файла OIL |
ARXML files selection (-autosar-multitasking) | Настройте строение многозадачности из определений файлов ARXML |
Configure multitasking manually | Допустим, что код предназначен для многозадачности |
Tasks (-entry-points) | Задайте функции, которые служат задачами для вашего многозадачного приложения |
Cyclic tasks (-cyclic-tasks) | Задайте функции, которые представляют циклические задачи |
Interrupts (-interrupts) | Задайте функции, которые представляют непередаваемые прерывания |
Critical section details (-critical-section-begin -critical-section-end) | Задайте функции, которые начинают и заканчивают критические сечения |
Temporally exclusive tasks (-temporal-exclusions-file) | Задайте функции точки входа, которые не могут выполняться одновременно |
Задайте опции анализа Polyspace
Задайте опции анализа Polyspace в пользовательском интерфейсе Polyspace, других IDE-s или скриптах.
Анализируйте многозадачные программы в Polyspace
Обнаружите гонки данных или взаимоблокировки или см. Комплексный анализ общего использования переменных.
Защиты для общих переменных в многозадачном коде
Защитите общие переменные с помощью критического раздела, временного исключения, приоритетов или отключения прерывания.
