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