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