Configure multitasking manually

Полагайте, что код предназначается для многозадачности

Описание

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

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

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Multitasking.

Командная строка: Смотрите информацию о Командной строке.

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

По умолчанию Средство поиска Ошибки определяет вашу многозадачную модель из вашего использования функций многопоточности. В Программе автоматического доказательства Кода необходимо включить автоматическое обнаружение параллелизма с опцией Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection). Однако в некоторых случаях использование автоматического обнаружения параллелизма может замедлить анализ Программы автоматического доказательства Кода.

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

Верификация Программы автоматического доказательства Кода использует ваши спецификации, чтобы определить:

  • Совместно используется ли глобальная переменная.

    Смотрите глобальные переменные (Polyspace Code Prover).

  • Может ли ошибка времени выполнения произойти.

    Например, если операция var++ происходит в теле циклической задачи, и вы не накладываете ограничение на var, операция может переполниться. Анализ обнаруживает возможное переполнение.

Анализ Средства поиска Ошибки использует ваши спецификации, чтобы искать дефекты параллелизма. Для получения дополнительной информации смотрите Дефекты Параллелизма.

Настройки

На

Код предназначается для многозадачного приложения.

Необходимо явным образом задать многозадачную настройку с помощью других опций Polyspace. Смотрите Анализ Многозадачности 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), вы включаете многозадачный анализ.