-temporal-exclusions-file)Задайте функции точки входа, которые не могут выполниться одновременно
Задайте функции точки входа, которые не могут выполниться одновременно. Выполнение функций не может наложиться друг с другом.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Multitasking. Смотрите Зависимости для других опций, которые необходимо также включить.
Командная строка: Используйте опцию -temporal-exclusions-file. Смотрите информацию о командной строке.
Используйте эту опцию, чтобы реализовать временное исключение в многозадачном коде.
Верификация Программы автоматического доказательства Кода проверяет при определении определенных задач, когда временно исключительный защищает все совместно используемые переменные от параллельного доступа. При определении возможных значений тех совместно используемых переменных верификация составляет то, что временно исключительные задачи не прерывают друг друга. Смотрите Глобальные переменные.
Анализ Средства поиска Ошибки использует временную информацию об исключении, чтобы искать дефекты параллелизма, такие как гонка данных. Смотрите Дефекты Параллелизма (Polyspace Bug Finder).
Никакое значение по умолчанию
Щелкните
, чтобы добавить поле. В каждом поле введите разделенный пробелом список функций. Polyspace® полагает, что функции в списке не могут выполниться одновременно.
Введите имена функций вручную или выберите из списка.
Щелкните, чтобы добавить поле и ввести имена функций.
Щелкните
, чтобы перечислить функции в вашем коде. Выберите функции из списка.
Чтобы включить эту опцию в пользовательском интерфейсе десктопных решений, сначала выберите опцию Configure multitasking manually.
При рассмотрении возможных значений совместно используемых переменных верификация Программы автоматического доказательства Кода учитывает спецификации для временно исключительных задач.
Однако, если совместно используемая переменная является указателем или массивом, программное обеспечение использует спецификации только, чтобы определить, является ли переменная разделяемой защищенной глобальной переменной. Для ошибки времени выполнения, регистрируясь в Программе автоматического доказательства Кода, программное обеспечение не принимает ваши спецификации во внимание и полагает, что к переменной можно одновременно получить доступ.
Для параметра командной строки создайте временный файл исключений в следующем формате:
На каждой линии введите одну группу временно исключенных задач.
В линии задачи разделяются пробелами.
Чтобы ввести комментарии, начните с #. Для примера смотрите файл polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\temporal_exclusions.txtpolyspaceroot, C:\Program Files\Polyspace\R2019a.
Параметр: -temporal-exclusions-file |
| Никакое значение по умолчанию |
| Значение: Имя временного файла исключений |
Пример (Средство поиска Ошибки):
Polyspace Bug Finder - источники |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Средства поиска Ошибки):
сервер средства поиска ошибки полипробела - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |
-non-preemptable-tasks | -preemptable-interrupts | Critical section details (-critical-section-begin -critical-section-end) | Cyclic tasks (-cyclic-tasks) | Interrupts (-interrupts) | Tasks (-entry-points)