-enable-concurrency-detection)Автоматически обнаружьте определенные семейства функций многопоточности
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Эта опция не доступна для кода, сгенерированного из кода MATLAB® или моделей Simulink®.
Задайте, должен ли анализ автоматически обнаружить POSIX®, VxWorks®, Windows®, μC/OS II и другие функции многопоточности.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Multitasking. Смотрите Зависимости (Polyspace Code Prover) для других опций, которые необходимо включить или отключить.
Командная строка: Используйте опцию -enable-concurrency-detection. Смотрите информацию о командной строке.
Если вы используете эту опцию, Polyspace® определяет вашу многозадачную модель из вашего использования функций многопоточности. В Средстве поиска Ошибки автоматическое обнаружение параллелизма включено по умолчанию. В Программе автоматического доказательства Кода необходимо явным образом включить автоматическое обнаружение параллелизма.
В некоторых случаях использование автоматического обнаружения параллелизма может замедлить анализ Программы автоматического доказательства Кода. В тех случаях можно принять решение не включить эту опцию и явным образом задать многозадачную модель. Смотрите Анализ Многозадачности Polyspace Конфигурирования Вручную.
OnЕсли вы используете одну из поддерживаемых функций для многозадачности, анализ автоматически обнаруживает вашу многозадачную модель из вашего кода.
Для списка поддерживаемых многозадачных функций и ограничений в автоматическом обнаружении потоков, смотрите Автоматическое обнаружение Создания Потока и Критического Раздела в Polyspace.
От (значения по умолчанию)Анализ не пытается обнаружить многозадачную модель из вашего кода.
Если вы хотите вручную сконфигурировать свою многозадачную модель, смотрите Анализ Многозадачности Polyspace Конфигурирования Вручную.
Если вы включаете эту опцию, ваш код должен содержать main функция. Вы не можете использовать опции Программы автоматического доказательства Кода, чтобы сгенерировать main.
Параметр: -enable-concurrency-detection |
| Значение по умолчанию: Off |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |