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