Exponenta Banner

Temporally exclusive tasks (-temporal-exclusions-file)

Задайте функции точки входа, которые не могут выполниться одновременно

Описание

Эта опция не доступна для кода, сгенерированного из MATLAB® код или Simulink® модели.

Задайте функции точки входа, которые не могут выполниться одновременно. Выполнение функций не может перекрыться друг с другом.

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

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

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

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

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

Верификация Code Prover проверки при определении определенных задач как временно исключительный защищает все совместно используемые переменные от параллельного доступа. При определении возможных значений тех совместно используемых переменных верификация составляет то, что временно исключительные задачи не прерывают друг друга. Смотрите Глобальные переменные.

Анализ Bug Finder использует временную информацию об исключении, чтобы искать дефекты параллелизма, такие как гонка данных. Смотрите Дефекты Параллелизма.

Настройки

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

Щелкните, чтобы добавить поле. В каждом поле введите разделенный пробелом список функций. Polyspace® полагает, что функции в списке не могут выполниться одновременно.

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

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

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

Зависимости

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

Советы

При рассмотрении возможных значений совместно используемых переменных верификация Code Prover учитывает технические требования для временно исключительных задач.

Однако, если совместно используемая переменная является указателем или массивом, программное обеспечение использует технические требования только, чтобы определить, является ли переменная разделяемой защищенной глобальной переменной. Для ошибки времени выполнения, регистрируясь в Code Prover, программное обеспечение не принимает ваши технические требования во внимание и полагает, что к переменной можно одновременно получить доступ.

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

Для параметра командной строки создайте временный файл исключений в следующем формате:

  • На каждой линии введите одну группу временно исключенных задач.

  • В линии задачи разделяются пробелами.

Чтобы ввести комментарии, начните с #. Для примера смотрите файл polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\temporal_exclusions.txt. Здесь, polyspaceroot папка установки Polyspace, например, C:\Program Files\Polyspace\R2019a.

Параметр: -temporal-exclusions-file
Никакое значение по умолчанию
Значение: Имя временного файла исключений
Пример (Bug Finder): Polyspace Bug Finder - источники file_name - временный файл исключений "C:\exclusions_file.txt"
Пример (Code Prover): Polyspace Code Prover - источники file_name - временный файл исключений "C:\exclusions_file.txt"
Пример (Сервер Bug Finder): сервер средства поиска ошибки полипробела - источники file_name - временный файл исключений "C:\exclusions_file.txt"
Пример (Сервер Code Prover): сервер программы автоматического доказательства полипробела кода - источники file_name - временный файл исключений "C:\exclusions_file.txt"

Смотрите также

| | | | |

Темы

Документация Polyspace Code Prover

Поддержка