Задачи (-entry-points)

Задайте функции, которые служат задачами к вашему многозадачному приложению

Описание

Задайте функции, которые служат задачами к вашему коду. Если функция не существует, верификация предупреждает вас и продолжает верификацию.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Multitasking. Смотрите Зависимости для других опций, которые необходимо также включить.

Командная строка: Используйте опцию -entry-points. Смотрите информацию о Командной строке.

Почему использование эта опция

Используйте эту опцию, когда ваш код будет предназначен для многозадачности.

Чтобы задать циклические задачи и прерывания, используйте опции Cyclic tasks (-cyclic-tasks) и Interrupts (-interrupts). Используйте эту опцию, чтобы задать другие задачи.

Анализ Программы автоматического доказательства Кода использует ваши спецификации, чтобы определить:

  • Совместно используется ли глобальная переменная.

    Смотрите глобальные переменные (Polyspace Code Prover).

  • Может ли ошибка времени выполнения произойти.

    Например, если операция var++ происходит в теле циклической задачи, и вы не накладываете ограничение на var, операция может переполниться. Анализ обнаруживает возможное переполнение.

Анализ Средства поиска Ошибки использует ваши спецификации, чтобы искать дефекты параллелизма. Для получения дополнительной информации смотрите Дефекты Параллелизма.

Настройки

Никакое значение по умолчанию

Введите имена функций или выберите из списка.

  • Щелкните, чтобы добавить поле и ввести имя функции.

  • Щелкните, чтобы перечислить функции в вашем коде. Выберите функции из списка.

Зависимости

Чтобы включить эту опцию в пользовательском интерфейсе десктопных решений, сначала выберите опцию Configure multitasking manually.

Советы

  • В Программе автоматического доказательства Кода функции, представляющие точки входа, должны иметь форму

    void functionName (void)

  • Если функциональный func берет аргументы, вы не можете использовать его непосредственно в качестве задачи. Использовать func в качестве задачи:

    1. Создайте новый функциональный newFunc. Объявление должно иметь форму void newFunc (void).

    2. Объявите аргументы к func как переменные volatile, локальные для newFunc. Вызовите func в newFunc.

    3. Задайте newFunc как задачу.

  • Если вы задаете функцию как задачу, необходимо предоставить ее определение. В противном случае верификация Программы автоматического доказательства Кода останавливается с сообщением об ошибке:

    task func_name must be a userdef function without parameters

    Анализ Средства поиска Ошибки продолжает, но не рассматривает функции как точку входа.

  • Если вы петляете верификацией файла в Программе автоматического доказательства Кода, ваши многозадачные опции проигнорированы. Смотрите Verify files independently (-unit-by-unit).

Информация о командной строке

Параметр: -entry-points
Никакое значение по умолчанию
Значение: function1[,function2[,...]]
Пример (средство поиска ошибки): polyspace-bug-finder -sources file_name -entry-points func_1,func_2
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -entry-points func_1,func_2
Пример (сервер средства поиска ошибки): polyspace-bug-finder-server -sources file_name -entry-points func_1,func_2
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -entry-points func_1,func_2