Запустите анализ Polyspace на пользовательском коде в блоке C Function

Можно запустить Polyspace® анализ пользовательского кода С в блоке C Function (Simulink) из Simulink®. Polyspace проверяет пользовательский код С на ошибки и ошибки при сохранении конкретной информации модели, такой как спецификация области значений проекта, характер и количество входов, заданных в модели Simulink.

Необходимые условия

Прежде чем запускать Polyspace из Simulink, необходимо связать Polyspace и MATLAB® установки. См. «Интеграция Polyspace с MATLAB и Simulink».

Чтобы открыть модель, используемую в этом примере, в Командном окне MATLAB, запустите:

openExample('polyspace_code_prover/CScriptDemoExample')
open_system('psdemo_model_link_sl_cscript');

Откройте модель для выполнения анализа Polyspace на пользовательском коде в блоке C Function

Модель содержит блок C Function, вызываемый Command Strategy внутри controller подсистема.

The Command Strategy блок реализует интерполяционную таблицу с использованием пользовательского кода С и выводит значение result на основе двух входов x и y.

Запуск анализа Polyspace

Запустите анализ Polyspace из редактора Simulink

Щелкните вкладку Apps и выберите Polyspace Code Verifier, чтобы открыть вкладку Polyspace.

  1. Выберите Bug Finder или Code Prover из выпадающего списка, расположенного в крайнем левом углу вкладки Polyspace.

  2. Чтобы запустить анализ Polyspace на пользовательском коде С в блоке C Function, выберите Custom Code Used in Model из выпадающего списка в разделе Analyze.

  3. Чтобы запустить анализ Polyspace, нажмите кнопку Run Analysis. В Командном Окне MATLAB отображается прогресс анализа.

  4. После анализа откроется пользовательский интерфейс Polyspace с результатами. Можно принять решение не открывать результаты автоматически после анализа, отменив выбор Open results automatically after verification в Settings. Чтобы открыть результаты после завершения анализа, нажмите кнопку Analysis Results.

  5. Чтобы просмотреть все результаты анализа Polyspace, щелкните Clear active filters из раскрывающегося списка Showing на панели Results List. Если вы запускаете анализ Code Prover, результаты для подсистемы контроллера содержат две красные проверки и оранжевую проверку.

  6. Чтобы организовать результаты по семейству, щелкнитеsquare drop down menu и выберите Family.

Чтобы переключиться между Bug Finder и Code Prover анализом, вернитесь в Редактор из пользовательского интерфейса Polyspace. Выберите Bug Finder или Code Prover из выпадающего списка, расположенного в крайнем левом углу вкладки Polyspace, и повторите анализ.

Запуск анализа Polyspace из MATLAB

Можно запустить анализ Polyspace Code Prover™ на пользовательском коде для этой модели из РЕДАКТОРА 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);

Идентифицируйте проблемы в коде С

Чтобы идентифицировать проблемы в пользовательском коде С, используйте информацию на панели Result Details и панели Source пользовательского интерфейса Polyspace. Если вы не видите эти панели, перейдите в Window > Show/Hide View и выберите отсутствующую панель. Для получения дополнительной информации о панелях см. «Сведения о результате» и «Источник».

Идентифицируйте входы и выходы блоков C Function в исходной панели

Polyspace переносит код в блок C Function в пользовательском оболочке кода. Входы и выходы блока C Function объявлены как глобальные переменные. Пользовательский код С вызывается как функция.

/* 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.

  • The void-void функция содержит пользовательские Коды С с переменными входами и выходами, замененными глобальными переменными. Если у вас есть несколько блоков C Function, то код в каждом блоке заворачивается в отдельные функции.

Глобальные переменные отражают все свойства входа и выхода блока C Function, включая их область значений данных, тип данных и размер. Если у вас есть несколько входы, то порядок глобальных переменных совпадает с порядком входа, заданным в блоке C Function. В этой таблице показаны входные и выходные переменные блока в этом примере и соответствующие им глобальные переменные на панели Source.

Имя глобальной переменной в Source панелиВозможностиИмя переменной в блоке C Function
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. Чтобы устранить неполадки, используйте подсказку на панели Source и информацию на панели Result Details. Этот рабочий процесс применяется к Code Prover и Bug Finder анализам.

Незаконно удаленный указатель

Красный Illegally dereferenced pointer проверки подсвечивает операцию разыменования после for цикл.

tmp = *p + 5;
На панели Result Details указывается, что указатель *p находится вне его границ. Чтобы найти первопричину проверки, следуйте жизненному циклу указателя, ведущего к незаконному размену.

  1. В начале своего жизненного цикла указатель *p указывает на первый элемент array который имеет 100 элементов.

  2. Затем p увеличивается в 100 раз, указывая *p в несуществующее местоположение array[100].

  3. Операция разгрузки в tmp = *p+5; становится незаконным, вызывая красный чек.

Индекс За пределами массива

Красный Out of Bounds array index проверки подсвечивает операцию индексации массива в if состояние.

 if (another_array[return_val - i + 9] != 0)
На панели Result Details указывается, что размер another_array равен 2, в то время как значение индекса return_val-i+9 колеблется от 2 до 18. Чтобы найти первопричину проверки, отследите значения переменных return_val и i использование подсказки. При наведении указателя мыши на любой образец переменных на Source панели отображается всплывающая подсказка.

  1. Значение i равен 100.

  2. Значение return_val колеблется от 93 до 109 из-за преобладающего условия: if ((return_val > 92) && (return_val < 110)).

  3. Значение индекса (return_val-i+9) оценивается в области значений от 2 до 18.

  4. Значения индекса находятся вне границ для массива another_array, вызывающий красный чек.

Переполнение

Проверка Overflow оранжевого цвета подсвечивает присвоение 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 Code Prover, смотрите Результаты Interpret Code Prover в Пользовательском интерфейсе Рабочий Стол.

Исправление выявленных проблем

Измените пользовательский код С или модель, чтобы исправить проблемы. Можно исправить проверку Polyspace несколькими способами. Примеры здесь иллюстрируют общий рабочий процесс исправления проверок Polyspace.

Незаконно удаленный указатель

Эту проверку можно решить несколькими способами. Измените Код С так, чтобы не был получен доступ к отсутствующему адресу памяти.

  1. Вернитесь в Редактор Simulink и дважды кликните по блоку C Function, чтобы открыть пользовательский код.

  2. Используйте оператор индекса для array для доступа к допустимому индексу массива. Вы можете получить доступ к индексам от 0 до 99, потому что array имеет 100 элементов. Доступ к индексам за пределами этой области значений приводит к ошибке времени выполнения в Simulink.

    // access any index between 0 to 99
    tmp = array[50] + 5; 
    Кроме того, присвойте адрес действительного места памяти p перед операцией разгрузки. Для примера, *p может указать на 51st элемент в array.
    // After the for loop, point p to a valid memory location
    p = &(array[50]);
    // ...
    tmp = *p + 5;
    

Индекс За пределами массива

Эту проверку можно решить несколькими способами. Измените код так, чтобы размер another_array[] остается большим или равным значению индекса return_val-i+9.

  1. Вернитесь в Редактор Simulink и дважды кликните по блоку C Function, чтобы открыть пользовательский код.

  2. Измените преобладающее условие при return_val так, чтобы значение индекса return_val-i+9 всегда рассчитывает на 0 или 1.

    if ((return_val > 91) && (return_val < 92))
    //...
    
    Кроме того, объявите another_array с размером 19.
    int another_array[19];

Переполнение

Эту проверку можно также решить несколькими способами. Измените код С или модель так, чтобы область значений правой стороны операции назначения оставалась равным или большим, чем диапазон левой оси.

  1. Вернитесь в Редактор Simulink.

  2. Насыщайте входные переменные x и y в модели так, чтобы их различие могло вписаться в 16-битное целое число. Рабочий процесс для исправления Overflow при помощи блоков насыщения описан в Run Polyspace Analysis on Custom Code in C Caller Blocks and Диаграммы Stateflow.

В качестве альтернативы увеличьте размер return_val в пользовательском коде С для размещения x-y.

  1. Вернитесь в Редактор Simulink и дважды кликните по блоку C Function, чтобы открыть пользовательский код.

  2. Объявить return_val в виде 32-битного целого числа.

    int32_T return_val;

Для получения дополнительной информации об обращении к результатам Polyspace, смотрите Адрес Polyspace Результаты через исправления ошибок или Обоснования.

См. также

|

Похожие темы