Можно экспортировать список глобальных переменных в коде к файлу разделенного текста вкладки или таблице MATLAB® (MATLAB). Текстовый файл или таблица содержат ту же информацию как панель Variable Access в пользовательском интерфейсе Polyspace®.
Используя текстовый файл, вы можете:
Сгенерируйте графики или статистику о глобальных переменных. Например, вы видите процент разделяемых глобальных переменных, которые не защищены от параллельного доступа.
Используйте информацию об области значений, чтобы создать внешние ограничения для глобальных переменных. Например, можно сообщить, что код свободен от определенных ошибок времени выполнения только для извлеченной области значений глобальных переменных.
Можно также использовать область значений, чтобы задать внешние ограничения на последующие верификации или верификацию других модулей. Смотрите Задают Внешние Ограничения.
Можно экспортировать результаты пользовательского интерфейса или командной строки.
Пользовательский интерфейс | Командная строка |
---|---|
| Используйте подходящие варианты с Доступные параметры:
|
Вместо текстового файла можно считать результаты анализа Polyspace в таблицу MATLAB. Смотрите polyspace.CodeProverResults.variableAccess
.
Текстовый файл или таблица содержат информацию о результате, доступную на панели Variable Access в пользовательском интерфейсе.
Например, предположите, что панель Variable Access показывает переменную SHR
с этой информацией.
Если вы экспортируете эту информацию в текстовый файл с разделителями табуляции и открываете файл в Excel®, вы видите ту же информацию. Часть информации показывают ниже.
Переменные | Тип данных | Доступ | Значения | #Reads | #Writes | Записанный задачей | Читайте задачей | Защита | Строка | Столбец | Файл | Функция | Расширение |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
SHR | int32 | Агрегат | 0 или 22 | 1 | 2 | server1 server2 | tregulate | Критический раздел | 30 | 11 | tasks1.c | c | |
SHR | Запись | 0 | 30 | 11 | tasks1.c | _init_globals () | c | ||||||
SHR | Запись | 22 | 81 | 8 | tasks1.c | Tserver () | c | ||||||
SHR | Чтение | 0 или 22 | 53 | 14 | tasks1.c | initregulate () | c |
См. также Переменный доступ.
Некоторые различия в представлении между панелью Variable Access и текстовым файлом (или таблица MATLAB) описаны ниже.
Столбец Access в текстовом файле указывает, показывает ли строка информацию о переменной (Aggregate) или информация об операциях на переменной (Write или Read).
Столбец Function в текстовом файле показывает функции, где переменная считана или записана (и на панели Variable Access).
Нет никаких строк, соответствующих к операциям чтения и операциям записи от задач (и на панели Variable Access). Эта информация доступна в Written by task и столбцах Read by task в текстовом файле (Tasks_Write
и Tasks_Read
столбцы в таблице MATLAB).
Цвета на панели Variable Access представлены через столбцы Unreachable и Protected:
Если к совместно используемой переменной получают доступ в нескольких задачах без общей защиты, это окрашено в оранжевый на панели Variable Access. В текстовом файле столбец Protected показывает Unprotected.
Если к совместно используемой переменной получают доступ в нескольких задачах, но с общей защитой, это окрашено в зеленый на панели Variable Access. В текстовом файле столбец Protected показывает Protected.
Если к совместно используемой переменной не получают доступ вообще, это окрашено в серый на панели Variable Access. В текстовом файле столбец Unreachable показывает Is unreachable.
Столбец Potential в текстовом файле показывает операции чтения или операции записи через указатели (или на панели Variable Access). Для операций через указатели столбец показывает Potential access.