-interrupts)Задайте функции, которые представляют nonpreemptable прерывания
Задайте функции, которые представляют nonpreemptable прерывания. Анализ принимает что операции в теле функции:
Может выполнить любое число раз.
Не может быть прерван нециклическими задачами, циклическими задачами или другими прерываниями. Нециклические задачи заданы с опцией, Tasks (-entry-points) и циклические задачи заданы с опцией Cyclic tasks (-cyclic-tasks).
Чтобы смоделировать прерывание, которое может быть прервано другими прерываниями, задайте прерывание как выгружаемое. Смотрите -preemptable-interrupts. Для примеров смотрите, Задают Прерывания Preemptable и Задачи Nonpreemptable.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Multitasking. Смотрите Зависимости для других опций, которые необходимо также включить.
Командная строка: Используйте опцию -interrupts. Смотрите информацию о Командной строке.
Используйте эту опцию, чтобы задать прерывания в вашем многозадачном коде. Функции, которые вы задаете, должны иметь прототип:
void function_name(void);
Верификация Программы автоматического доказательства Кода использует ваши спецификации, чтобы определить:
Совместно используется ли глобальная переменная.
Смотрите глобальные переменные (Polyspace Code Prover).
Может ли ошибка времени выполнения произойти.
Например, если операция var=INT_MAX; происходит в прерывании, и var++ происходит в теле задачи, переполнение может произойти если прерывание excepts перед операцией в задаче. Анализ обнаруживает возможное переполнение.
Анализ Средства поиска Ошибки использует ваши спецификации, чтобы искать дефекты параллелизма. Для дефекта Data race анализ устанавливает следующие отношения между прерываниями и другими задачами:
Данные мчатся между двумя прерываниями:
Две операции в различных прерываниях не могут вмешаться друг в друга (если одно из прерываний не выгружаемо). Даже если операции используют ту же совместно используемую переменную без защиты, гонка данных не может произойти.
Данные мчатся между прерыванием и другой задачей:
Операция в прерывании не может вмешаться в атомарную операцию ни в какой другой задаче. Даже если операции используют ту же совместно используемую переменную без защиты, гонка данных не может произойти.
Операция в прерывании может вмешаться в неатомарную операцию в любой другой задаче, если другой задачей не является также nonpreemptable прерывание. Поэтому, если операции используют ту же совместно используемую переменную без защиты, гонка данных может произойти.
Смотрите дефекты параллелизма.
Никакое значение по умолчанию
Введите имена функций или выберите из списка.
Щелкните
, чтобы добавить поле и ввести имя функции.
Щелкните
, чтобы перечислить функции в вашем коде. Выберите функции из списка.
Чтобы включить эту опцию в пользовательском интерфейсе десктопных решений, сначала выберите опцию 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).
Параметр: -interrupts |
| Никакое значение по умолчанию |
Значение: |
Пример (средство поиска ошибки): |
Пример (программа автоматического доказательства кода):
|
Пример (сервер средства поиска ошибки): |
Пример (сервер программы автоматического доказательства кода):
|
-non-preemptable-tasks | -preemptable-interrupts | Cyclic tasks (-cyclic-tasks) | Tasks (-entry-points)