Учтите, что код предназначен для многозадачности
Эта опция недоступна для кода, сгенерированного в моделях MATLAB ® или Simulink ®.
Укажите, является ли ваш код многозадачным приложением. Этот параметр позволяет вручную настроить многозадачную структуру для Polyspace ®.
Пользовательский интерфейс (только для настольных ПК): в конфигурации проекта эта опция доступна на узле многозадачности.
Файл командной строки и параметров: См. Сведения о командной строке.
По умолчанию программа Bug Finder определяет модель многозадачности с помощью многопоточных функций. В программе Code Prover необходимо включить автоматическое обнаружение параллелизма с помощью опции Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection). Однако в некоторых случаях использование автоматического обнаружения параллелизма может замедлить анализ проверки кода.
В случаях, когда автоматическое обнаружение параллелизма не поддерживается, можно явно указать многозадачную модель с помощью этой опции. После выбора этого параметра можно явно указать функции точки входа, циклические задачи, прерывания и механизмы защиты для общих переменных, таких как сведения о критических разделах.
Проверка программы проверки кода использует ваши спецификации для определения:
Является ли глобальная переменная общей.
См. раздел Глобальные переменные (средство проверки кода Polyspace).
Может ли возникнуть ошибка времени выполнения.
Например, если операция var++ возникает в теле циклической задачи, и вы не накладываете ограничения на var, операция может переполниться. Анализ обнаруживает возможное переполнение.
Анализ Bug Finder использует ваши спецификации для поиска дефектов параллелизма. Дополнительные сведения см. в разделе Дефекты параллелизма.
НаКод предназначен для многозадачного приложения.
Необходимо явно указать многозадачную конфигурацию с помощью других параметров Polyspace. См. раздел Настройка многозадачного анализа в многозадачном пространстве вручную.
Выкл. (по умолчанию)Код не предназначен для многозадачного приложения.
Отключение этого параметра приводит к следующим дополнительным последствиям в программе Code Prover:
Если main существует, Code Prover проверяет только те функции, которые вызываются main.
Если main не существует, Polyspace проверяет заданные функции. Для проверки функций Polyspace генерирует main функции и вызывает функции из сгенерированных main в указанной последовательности. Дополнительные сведения см. в разделе Verify module or library (-main-generator).
При запуске файла путем проверки файла в программе Code Prover параметры многозадачности игнорируются. Посмотрите Verify files independently (-unit-by-unit).
Нет одного параметра командной строки для включения многозадачного анализа. С помощью любой из опций Tasks (-entry-points), Cyclic tasks (-cyclic-tasks) или Interrupts (-interrupts), вы включаете многозадачный анализ.