-interrupts)Задайте функции, которые представляют непередаваемые прерывания
Эта опция недоступна для кода, сгенерированного из MATLAB® код или Simulink® модели.
Задайте функции, которые представляют непередаваемые прерывания. Анализ принимает, что операции в теле функции:
Может выполняться любое количество раз.
Не может быть прервана нециклическими задачами, циклическими задачами или другими прерываниями. Нециклические задачи задаются опцией Tasks (-entry-points) а циклические задачи задаются опцией Cyclic tasks (-cyclic-tasks).
Чтобы смоделировать прерывание, которое может быть прервано другими прерываниями, задайте прерывание как предопределяемое. См. -preemptable-interrupts. Для примеров смотрите Задать предпусковые прерывания и незапускаемые задачи.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция доступна на узле Multitasking. Смотрите Зависимости для других опций, которые вы также должны включить.
Командная строка и файл опций: Используйте опцию -interrupts. См. «Информация о командной строке».
Используйте эту опцию, чтобы задать прерывания в многозадачном коде. Функции, которые вы задаете, должны иметь прототип:
void function_name(void);
Верификация Code Prover использует ваши спецификации, чтобы определить:
Является ли глобальная переменная общей.
См. «Глобальные переменные» (Polyspace Code Prover).
Может ли возникнуть ошибка времени выполнения.
Для образца, если операция var=INT_MAX; происходит в прерывании и var++ происходит в теле задачи, переполнение может произойти, если прерывание исключает перед операцией в задаче. Анализ обнаруживает возможное переполнение.
Анализ Bug Finder использует ваши спецификации для поиска дефектов параллелизма. Для Data race дефект, анализ устанавливает следующие отношения между прерываниями и другими задачами:
Гонка данных между двумя прерываниями:
Две операции в разных прерываниях не могут мешать друг другу (если одно из прерываний не может быть предварительно опорожнено). Даже если операции используют ту же общую переменную без защиты, гонка данных не может произойти.
Гонка данных между прерыванием и другой задачей:
Операция в прерывании не может мешать атомарной операции в любой другой задаче. Даже если операции используют ту же общую переменную без защиты, гонка данных не может произойти.
Операция в прерывании может мешать неатомной операции в любой другой задаче, если другая задача также не является непередаваемым прерыванием. Поэтому, если операции используют ту же общую переменную без защиты, может произойти гонка данных.
См. «Дефекты параллелизма».
По умолчанию нет
Введите имена функции или выберите из списка.
Щелкните
, чтобы добавить поле и ввести имя функции.
Щелкните
, чтобы отобразить функции в коде. Выберите функции из списка.
Чтобы включить эту опцию в пользовательском интерфейсе продуктов для настольных ПК, сначала выберите опцию Configure multitasking manually.
В Code Prover функции, представляющие прерывания, должны иметь форму
void functionName (void)
Если функция func принимает аргументы или возвращает значение, вы не можете использовать его непосредственно как прерывание. Как использовать func как прерывание, вызов func от обертки void- void и укажите оболочку как прерывание. Смотрите Настройку многозадачного анализа Polyspace вручную.
Если вы задаете функцию как прерывание, необходимо предоставить ее определение. В противном случае верификация Code Prover останавливается с сообщением об ошибке:
task func_name must be a userdef function without parameters
Анализ Bug Finder продолжается, но не рассматривает функцию как прерывание.
Если вы запускаете файл по верификации файла в Code Prover, ваши опции многозадачности игнорируются. См. Verify files independently (-unit-by-unit).
Polyspace® многозадачный анализ принимает, что прерывание не может прервать само себя.
Параметр: -interrupts |
| По умолчанию нет |
Значение: |
Пример (Bug Finder): Polyspace Bug Finder -sources |
Пример (Code Prover):
Polyspace Code Prover -sources file_name |
Пример (Bug Finder Server): polyspace-bug-finder-server -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |
-non-preemptable-tasks | -preemptable-interrupts | Cyclic tasks (-cyclic-tasks) | Tasks (-entry-points)