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