-temporal-exclusions-file
)Задайте функции точки входа, которые не могут выполняться одновременно
Эта опция недоступна для кода, сгенерированного из MATLAB® код или Simulink® модели.
Задайте функции точки входа, которые не могут выполняться одновременно. Выполнение функций не может перекрываться друг с другом.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция доступна на узле Multitasking. Смотрите Зависимости для других опций, которые вы также должны включить.
Командная строка и файл опций: Используйте опцию -temporal-exclusions-file
. См. «Информация о командной строке».
Используйте эту опцию, чтобы реализовать временное исключение в многозадачном коде.
A Кода Prover верификации проверяет, защищает ли установка временных исключений для некоторых задач все общие переменные от параллельного доступа. При определении возможных значений этих общих переменных верификация учитывает тот факт, что временные исключительные задачи не прерывают друг друга. См. «Глобальные переменные» (Polyspace Code Prover).
Анализ Bug Finder использует информацию о временном исключении для поиска дефектов параллелизма, таких как гонка данных. См. «Дефекты параллелизма».
По умолчанию нет
Щелкните, чтобы добавить поле. В каждом поле введите разделенный пробелом список функций. Polyspace® считает, что функции в списке не могут выполняться одновременно.
Введите имена функции вручную или выберите из списка.
Щелкните, чтобы добавить поле и ввести имена функции.
Щелкните, чтобы отобразить функции в коде. Выберите функции из списка.
Чтобы включить эту опцию в пользовательском интерфейсе продуктов для настольных ПК, сначала выберите опцию Configure multitasking manually
.
При рассмотрении возможных значений общих переменных верификация Code Prover учитывает ваши спецификации для временно эксклюзивных задач.
Однако, если общая переменная является указателем или массивом, программа использует спецификации только для того, чтобы определить, является ли переменная общей защищенной глобальной переменной. Для проверки ошибок времени выполнения в Code Prover, программное обеспечение не учитывает ваши спецификации и считает, что переменная может быть одновременно доступна.
Для опции командной строки создайте файл временных исключений в следующем формате:
В каждой линии введите одну группу временно исключенных задач.
В течение линии задачи разделяются пространства.
Чтобы ввести комментарии, начнем с #
. Для получения примера смотрите файл
. Здесь, polyspaceroot
\ polyspace\examples\cxx\Code _ Prover _ Example\sources\temporal _ exclusions.txt
является папкой установки Polyspace, например polyspaceroot
C:\Program Files\Polyspace\R2019a
.
Параметр:
-temporal-exclusions-file |
По умолчанию нет |
Значение: Имя файла временных исключений |
Пример (Bug Finder):
Polyspace Bug Finder -sources file_name |
Пример (Code Prover):
Polyspace Code Prover -sources file_name |
Пример (Bug Finder Server):
polyspace-bug-finder-server -sources file_name |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |