Включите автоматическое обнаружение параллелизма для Программы автоматического доказательства Кода (-enable-concurrency-detection)

Автоматически обнаружьте определенные семейства функций многопоточности

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

Задайте, должен ли анализ автоматически обнаружить POSIX®, VxWorks®, Windows®, μC/OS II и другие функции многопоточности.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Multitasking. Смотрите Зависимости для других опций, которые необходимо включить или отключить.

Командная строка: Используйте опцию -enable-concurrency-detection. Смотрите информацию о Командной строке.

Почему использование эта опция

Если вы используете эту опцию, Polyspace® определяет вашу многозадачную модель от вашего использования функций многопоточности. В Средстве поиска Ошибки автоматическое обнаружение параллелизма включено по умолчанию. В Программе автоматического доказательства Кода необходимо явным образом включить автоматическое обнаружение параллелизма.

В некоторых случаях использование автоматического обнаружения параллелизма может замедлить анализ Программы автоматического доказательства Кода. В тех случаях можно принять решение не включить эту опцию и явным образом задать многозадачную модель. Смотрите Анализ Многозадачности Polyspace Конфигурирования Вручную.

Настройки

На

Если вы используете одну из поддерживаемых функций для многозадачности, анализ автоматически обнаруживает вашу многозадачную модель из вашего кода.

Для списка поддерживаемых многозадачных функций и ограничений в автоматическом обнаружении потоков, смотрите Автоматическое обнаружение Создания Потока и Критического Раздела в Polyspace.

От (значения по умолчанию)

Анализ не пытается обнаружить многозадачную модель из вашего кода.

Если вы хотите вручную сконфигурировать свою многозадачную модель, смотрите Анализ Многозадачности Polyspace Конфигурирования Вручную.

Зависимости

Если вы включаете эту опцию, ваш код должен содержать функцию main. Вы не можете использовать опции Программы автоматического доказательства Кода, чтобы сгенерировать main.

Информация о командной строке

Параметр: -enable-concurrency-detection
Значение по умолчанию: 'off'
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -enable-concurrency-detection
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -enable-concurrency-detection