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