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