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