Можно запустить Polyspace® на коде, сгенерированном из Simulink® модель или подсистема.
Polyspace Bug Finder™ проверяет код на наличие ошибок или нарушений правил кодирования (для образца, MISRA C®: правила 2012 года).
Polyspace Code Prover™ полностью проверяет код на ошибки времени выполнения.
Если вы используете Embedded Coder® для генерации кода в этом руководстве показано, как запустить Polyspace на коде, сгенерированном из простой модели Simulink. Полный рабочий процесс см. в разделе Запуск анализа Polyspace на коде, сгенерированном с помощью Embedded Coder.
Прежде чем запускать Polyspace из Simulink, необходимо связать Polyspace и MATLAB® установки. См. «Интеграция Polyspace с MATLAB и Simulink».
Чтобы открыть модель, используемую в этом примере, в Командном окне MATLAB, запустите:
openExample('polyspace_code_prover/OpenModelForCodeGenerationAndPolyspaceAnalysisExample')Откройте модель polyspace_controller_demo для настройки генерации кода и анализа Polyspace.
Чтобы начать анализ Polyspace кода, сгенерированного из модели:
На вкладке Apps выберите Polyspace Code Verifier.
На вкладке Polyspace найдите поле Analyze и выберите Code Generated as Top model из раскрывающегося меню.
Щелкните в любом месте на холсте. В Analyze Code from поле показано имя модели. Выберите Run Analysis.
Polyspace проверяет сгенерированный код, когда вы нажимаете Run Analysis. Если сгенерированный код не присутствует, Polyspace сначала генерирует код при помощи Embedded Coder, а затем начинает анализ.
Эквивалентный код MATLAB:
load_system('polyspace_controller_demo'); slbuild('polyspace_controller_demo'); mlopts = pslinkoptions('polyspace_controller_demo'); mlopts.ResultDir ='\result' mlopts.VerificationMode = 'CodeProver'; pslinkrun('polyspace_controller_demo', mlopts);
CodeProver с BugFinder. Для получения дополнительной информации о коде смотрите pslinkoptions и pslinkrun.После анализа результаты отображаются в пользовательском интерфейсе Polyspace.
Если запустить Bug Finder, результаты состоят из ошибок, обнаруженных в сгенерированном коде. Если вы запускаете Code Prover, результаты состоят из проверок, которые закодированы следующим образом:
Зеленый (проверенный код): Проверка не проваливается для предоставленных ограничений данных. Для образца операция деления не вызывает Division by Zero ошибки.
Красный (проверенная ошибка): проверка всегда прекращается для набора предоставленных ограничений данных. Для образца операция деления всегда вызывает Division by Zero ошибку.
Оранжевый (возможная ошибка): проверка указывает на недоказанный код и может оказаться неудачной для определенных значений предоставленных ограничений данных. Для образца операция деления иногда вызывает Division by Zero ошибку.
Серый (недоступный код): Проверка указывает на операцию кода, которая не может быть достигнута для предоставленных ограничений данных.
Подробно проверьте результаты каждого анализа. Например, в результатах Code Prover:
На панели Results List выберите красный Out of bounds array index.
На панели Source поместите курсор на красный чек, чтобы просмотреть дополнительные сведения. Например, всплывающая подсказка на красном [ оператор утверждает размер массива и возможные значения индекса массива. Панель Result Details также содержит эти сведения.
Ошибка возникает в рукописном файле C Command_strategy_file.c. Файл C находится внутри блока s-function Command_Strategy в Reduced Precision подсистема (в модель-ссылку relative threshold).
Для кода, сгенерированного из модели, можно отследить ошибку обратно в модель. В этих разделах показано, как проследить определенные результаты Code Prover обратно в модель.
На панели Results List выберите оранжевую ошибку Out of bounds array index, которая происходит в файле polyspace_controller_demo.c.
На панели Source щелкните ссылку, S4:76 в комментариях над оранжевой ошибкой.
/* Transition: '<S4>:75' */ /* Transition: '<S4>:76' */ (*i)++; /* Outport: '<Root>/FaultTable' */ polyspace_controller_demo_Y.FaultTable[*i] = 10;
Вы видите, что ошибка возникает из-за перехода на диаграмме Stateflow synch_and_asynch_monitoring. Можно проследить ошибку до индекса входной переменной диаграммы Stateflow.
Избежать Out of bounds array index можно несколькими способами. Одним из способов является ограничение переменного входа index использование блока Saturation перед диаграммой Stateflow.
На панели Results List выберите оранжевую ошибку Overflow, показанную ниже. Ошибка появится в файле polyspace_controller_demo.c.
На панели Source проверьте ошибку. Чтобы проследить ошибку назад в модель, щелкните ссылку, S1/Gain в комментариях над оранжевой ошибкой.
/* Gain: '<S1>/Gain' incorporates: * Inport: '<Root>/Battery Info' * Inport: '<Root>/Rotation' * Sum: '<S1>/Sum1' */ Gain = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >> 10);
Fault Management подсистема внутри блока Gain, следующего за блоком Sum.
Избежать Overflow можно несколькими способами. Одним из способов является ограничение значения сигнала in_battery_info который подается на блок Sum. Для ограничения сигнала:
Дважды кликните блок Inport Battery info который обеспечивает входной сигнал in_battery_info в модель.
На вкладке Signal Attributes измените Maximum значение сигнала.
Ошибки в этой модели происходят из-за одного из следующих:
Дефектное масштабирование, неизвестные калибровки и непроверенные области значений данных, выходящие из подсистемы в арифметический блок.
Манипуляции с массивами в функциях на основе событий Stateflow и рукописной интерполяционной таблицы.
Насыщенность, приводящая к неожиданному потоку данных внутри сгенерированного кода.
Дефектное программирование Stateflow.
Если вы идентифицируете первопричину ошибки, можно соответствующим образом изменить модель, чтобы исправить проблему.
Чтобы проверить на нарушения правил кодирования, перед началом анализа кода:
На вкладке Polyspace выберите Settings.
В диалоговом окне Параметры конфигурации выберите подходящую опцию в списке Settings from. Для образца выберите Project configuration and MISRA C 2012 AGC Checking.
Рекомендуется запустить Bug Finder для проверки правил C:2012 MISRA. На вкладке Polyspace выберите Bug Finder.
Щелкните Apply или OK и повторите анализ.
Можно выровнять результаты путем добавления аннотаций к блокам. Во время анализа кода Polyspace Code Prover считывает ваши аннотации и заполняет результат вашим обоснованием. Как только вы обосновываете результат, вы не должны пересматривать его снова.
На панели Results List в раскрывающемся списке в верхнем левом углу выберите File.
В файл polyspace_controller_demo.c, в функциональной polyspace_controller_demo_step(), выберите нарушение MISRA C:2012 правила 10.4. На панели Source показано, что операция сложения нарушает правило.
На панели Source щелкните ссылку, S1/Sum1 в комментариях над операцией сложения.
/* Gain: '<S1>/Gain' incorporates: * Inport: '<Root>/Battery Info' * Inport: '<Root>/Rotation' * Sum: '<S1>/Sum1' */ Gain = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >> 10);
Вы видите, что нарушение правил происходит в блоке Sum.
Чтобы аннотировать этот блок и обосновать нарушение правил:
Выберите блок. На вкладке Polyspace выберите Add Annotation.
Выберите MISRA-C-2012 для Annotation type и ввода информации о нарушении правил. Установите Status на No action planned, а Severity на Unset.
Щелкните Apply или OK. Слова Polyspace annotation появляются под блоком, что указывает на то, что блок содержит аннотацию кода.
Перегенерируйте код и перезапустите анализ. Severity и Status столбцы на панели Results List заполняются аннотациями.