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