Анализ Polyspace ® можно выполнить для пользовательского кода C в блоке C Function (Simulink) из Simulink ®. Polyspace проверяет пользовательский код C на наличие ошибок и ошибок, сохраняя при этом конкретную информацию о модели, например спецификацию диапазона конструкции, характер и количество входных данных, указанных в модели Simulink.
Перед запуском Polyspace из Simulink необходимо связать установки Polyspace и MATLAB ®. См. раздел Интеграция полиспейса с MATLAB и Simulink.
Чтобы открыть модель, используемую в этом примере, в окне команд MATLAB выполните следующее:
openExample('polyspace_code_prover/CScriptDemoExample') open_system('psdemo_model_link_sl_cscript');
Модель содержит блок функции C, называемый Command Strategy внутри controller подсистема.
Command Strategy блок реализует таблицу поиска с использованием пользовательского кода C и выводит значение result на основе двух входных данных x и y.
Перейдите на вкладку «Приложения» и выберите «Проверка кода полиспейса», чтобы открыть вкладку «Полиспейс».
Выберите Поиск ошибок (Bug Finder) или Проверка кода (Code Prover) в раскрывающемся списке, расположенном в крайнем левом углу вкладки Полиспейс (Polyspace).
Чтобы выполнить анализ Polyspace для пользовательского кода C в блоке C Function, выберите Пользовательский код, используемый в модели (Custom Code Used in Model) из выпадающего списка в разделе Analyze (Анализ).
Чтобы запустить анализ Polyspace, нажмите кнопку Выполнить анализ (Run Analysis). В окне команд MATLAB отображается ход выполнения анализа.
После анализа откроется интерфейс пользователя Polyspace с результатами. Можно не открывать результаты автоматически после анализа, отменив выбор пункта Открыть результаты автоматически после проверки в разделе Настройки. Чтобы открыть результаты после завершения анализа, нажмите кнопку Результаты анализа (Analysis Results).
Чтобы просмотреть все результаты анализа Polyspace, щелкните Очистить активные фильтры (Clear active filters) в выпадающем списке Показать (Show) на панели Список результатов (Results List). При выполнении анализа проверки кода результаты для подсистемы контроллера содержат две проверки красного и оранжевого цвета.
Чтобы упорядочить результаты по семейству, щелкните
и выберите Семейство (Family).
Для переключения между функцией поиска ошибок и функцией проверки кода вернитесь в редактор Simulink из пользовательского интерфейса Polyspace. Выберите Поиск ошибок (Bug Finder) или Проверка кода (Code Prover) в раскрывающемся списке, расположенном в крайнем левом углу вкладки Полиспейс (Polyspace), и повторно запустите анализ.
Анализ Prover™ кода Polyspace для пользовательского кода этой модели можно выполнить в редакторе MATLAB или в окне команд, используя следующий код:
% Load the model 'psdemo_model_link_sl_cscript' load_system('psdemo_model_link_sl_cscript'); % Create a 'pslinkoptions' object mlopts = pslinkoptions('psdemo_model_link_sl_cscript'); % Specify whether to run 'CodeProver' or 'BugFinder' Analysis mlopts.VerificationMode = 'CodeProver'; % Specify custom code as analysis target and run the analysis pslinkrun('-slcc','psdemo_model_link_sl_cscript',mlopts);
Чтобы определить проблемы в пользовательском коде C, используйте информацию на панели Сведения о результате (Result Details) и на панели Источник (Source) интерфейса пользователя Polyspace. Если эти панели не отображаются, перейдите в меню «Окно» > «Показать/скрыть вид» и выберите отсутствующую панель. Дополнительные сведения о панелях см. в разделах Сведения о результатах и Источник.
Polyspace переносит код в блоке C Function в пользовательскую оболочку кода. Входы и выходы блока C Function объявляются как глобальные переменные. Пользовательский код C вызывается как функция.
/* Variables corresponding to inputs ..*/
// global In...
/* Variables corresponding to outputs*/
// global Out...
/* Wrapper functions for code in block */
// void ...(void){
//...
}
Глобальные переменные, соответствующие входам, начинаются с In, такие как In1_psdemo_model_link_sl_cscript_98_Command_strategy.
Глобальные переменные, соответствующие выходам, начинаются с Out, такие как Out1_psdemo_model_link_sl_cscript_98_Command_strategy.
void-void содержит пользовательский код C с переменными ввода и вывода, замененными глобальными переменными. При наличии нескольких функциональных блоков C код в каждом блоке переносится в отдельные функции.
Глобальные переменные отражают все свойства входа и выхода блока C Function, включая их диапазон данных, тип данных и размер. При наличии нескольких входных данных порядок глобальных переменных совпадает с порядком входных данных, определенных в блоке C Function. В этой таблице показаны входные и выходные переменные блока в данном примере и их соответствующие глобальные переменные на панели «Источник».
| Имя глобальной переменной в области источника | Объем | Имя переменной в функциональном блоке C |
|---|---|---|
In1_psdemo_model_link_sl_cscript_98_Command_strategy | Вход | x |
In2_psdemo_model_link_sl_cscript_98_Command_strategy | Вход | y |
Out1_psdemo_model_link_sl_cscript_98_Command_strategy | Продукция | result |
Определите проблемы в пользовательском коде, просмотрев упакованный код на панели «Источник». Используйте всплывающую подсказку на панели Источник (Source) и сведения на панели Сведения о результатах (Result Details), чтобы устранить проблемы. Этот рабочий процесс применяется к анализам проверки кода и поиска ошибок.
Красный флажок Незаконно деэрессецированный указатель выделяет операцию деэреференции после for цикл.
tmp = *p + 5;
*p находится за его пределами. Чтобы найти первопричину проверки, следуйте жизненному циклу указателя, приводящему к недопустимой деэреференции.
В начале жизненного цикла указатель *p указывает на первый элемент array который имеет 100 элементов.
Тогда p увеличивается на 100 раз, указывая *p в несуществующее расположение array[100].
Операция отмены ссылки в tmp = *p+5; становится незаконным, вызывая красный чек.
Красный индекс массива Check Out of Bounds выделяет операцию индексирования массива в if состояние.
if (another_array[return_val - i + 9] != 0)
another_array равно 2, в то время как значение индекса return_val-i+9 колеблется от 2 до 18. Чтобы найти основную причину проверки, отслеживайте значения переменных. return_val и i с помощью подсказки. При наведении курсора на любой экземпляр переменных на панели «Источник» отображается подсказка.
Значение i составляет 100.
Значение return_val колеблется от 93 до 109 из-за преобладающего состояния: if ((return_val > 92) && (return_val < 110)).
Значение индекса (return_val-i+9) вычисляется в диапазоне от 2 до 18.
Значения индекса выходят за пределы массива another_array, что вызвало красный чек.
Оранжевая проверка переполнения выделяет назначение return_val. На панели Сведения о результате (Result Details) указывается, что проверка связана с ограниченными входными значениями. Чтобы найти основную причину проверки, проверьте тип данных и соответствующий диапазон переменных с помощью всплывающей подсказки.
Входные значения x и y соответствуют этим соответствующим глобальным переменным
In1_psdemo_model_link_sl_cscript_98_Command_strategy
In2_psdemo_model_link_sl_cscript_98_Command_strategy
Первый вход x - несвязанное целое число без знака. Поскольку x является несвязанным, имеет полный диапазон целого числа без знака, который составляет от 0 до 65535.
Второй вход y - ограниченное беззнаковое целое число в диапазоне от 0 до 1023.
x-y назначается несвязанному целому числу со знаком return_val. Поскольку return_val является несвязанным, имеет полный диапазон от -32768 до 32767.
Диапазон x-y от 1023 до 65535, в то время как диапазон return_val от -32768 до 32767.
Некоторые возможные значения x-y не может вписываться в return_val, что вызвало оранжевый чек.
Дополнительные сведения о интерпретации результатов анализа проверки кода Polyspace см. в разделе Интерпретация результатов проверки кода в пользовательском интерфейсе Polyspace Desktop.
Измените пользовательский код C или модель, чтобы устранить проблемы. Можно исправить проверку Polyspace несколькими способами. Приведенные здесь примеры иллюстрируют общий рабочий процесс фиксации проверок Polyspace.
Эту проверку можно выполнить несколькими способами. Измените код C таким образом, чтобы не было доступа к несуществующему адресу памяти.
Вернитесь в редактор Simulink и дважды щелкните по блоку C Function, чтобы открыть пользовательский код.
Используйте оператор index на array для доступа к допустимому индексу массива. Вы можете получить доступ к индексам от 0 до 99, так как array имеет 100 элементов. Доступ к индексам за пределами этого диапазона приводит к ошибке во время выполнения в Simulink.
// access any index between 0 to 99 tmp = array[50] + 5;
p перед операцией обособления. Например, *p может указывать на 51-й элемент в array.// After the for loop, point p to a valid memory location p = &(array[50]); // ... tmp = *p + 5;
Эту проверку можно выполнить несколькими способами. Измените код таким образом, чтобы размер another_array[] остается больше или равно значению индекса return_val-i+9.
Вернитесь в редактор Simulink и дважды щелкните по блоку C Function, чтобы открыть пользовательский код.
Изменение преобладающего условия на return_val чтобы значение индекса return_val-i+9 всегда вычисляется как 0 или 1.
if ((return_val > 91) && (return_val < 92)) //...
another_array с размером 19.int another_array[19];
Эту проверку также можно выполнить несколькими способами. Измените код C или модель таким образом, чтобы диапазон правой стороны операции назначения оставался равным или большим диапазона левой стороны.
Вернуться к редактору Simulink.
Насыщение входных переменных x и y в модели, чтобы их разность могла поместиться в 16-битное целое число. Процедура устранения переполнения с помощью блоков насыщения описана в разделе Выполнение анализа полиспейсов для пользовательского кода в блоках вызывающих абонентов C и диаграммах статусов.
В качестве альтернативы увеличьте размер return_val в пользовательском коде C для размещения x-y.
Вернитесь в редактор Simulink и дважды щелкните по блоку C Function, чтобы открыть пользовательский код.
Объявить return_val как 32-разрядное целое число.
int32_T return_val;
Дополнительные сведения о адресации результатов Polyspace см. в разделе Адресация результатов Polyspace с помощью исправлений ошибок или обоснований.