Можно запустить Polyspace® на коде, сгенерированном из модели Simulink® или подсистемы.
Polyspace Bug Finder™ проверяет код на ошибки или кодирующий нарушения правила (например, MISRA C®: 2 012 правил).
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, результаты состоят из ошибок, обнаруженных в сгенерированном коде. Если при запуске Программу автоматического доказательства Кода, результаты состоят из проверок, на которые наносят цветную маркировку можно следующим образом:
Зеленый (доказанный код): проверка не перестала работать для обеспеченных ограничений данных. Например, операция деления не вызывает ошибку Division by Zero.
Красный (проверенная ошибка): проверка всегда перестала работать для набора обеспеченных ограничений данных. Например, операция деления всегда вызывает ошибку Division by Zero.
Оранжевый (возможная ошибка): проверка указывает на бездоказательный код и может перестать работать для определенных значений обеспеченных ограничений данных. Например, операция деления иногда вызывает ошибку Division by Zero.
Серый (недостижимый код): проверка указывает на операцию кода, которая не может быть достигнута обеспеченные ограничения данных.
Рассмотрите каждый результат анализа подробно. Например, в ваших результатах Программы автоматического доказательства Кода:
На панели Results List выберите красную проверку Out of bounds array index.
На панели Source установите свой курсор на красную проверку, чтобы просмотреть дополнительную информацию. Например, подсказка на красном [ оператор утверждает размер массивов и возможные значения индекса массива. Панель Result Details также предоставляет эту информацию.
Ошибка происходит в рукописном файле C Command_strategy_file.c. Файлом C является в Блоке s-function Command_Strategy в Reduced Precision подсистема (в модели - ссылке relative threshold).
Для кода, сгенерированного из модели, можно проследить ошибку до модели. Эти разделы показывают, как проследить определенные результаты Программы автоматического доказательства Кода до модели.
На панели 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.
В диалоговом окне Configuration Parameters выберите подходящую опцию в списке Settings from. Например, выберите Project configuration and MISRA C 2012 AGC Checking.
Рекомендуется, чтобы вы запустили Bug Finder для проверки правил MISRA C:2012. На вкладке Polyspace выберите Bug Finder.
Нажмите Apply или OK и повторно выполните анализ.
Можно выровнять по ширине результаты путем добавления аннотаций в блоки. Во время анализа кода Polyspace Code Prover читает ваши аннотации и заполняет результат с вашим выравниванием. Если вы выравниваете по ширине результат, вы не должны рассматривать его снова.
На панели Results List, из выпадающего списка в левом верхнем углу, выбирают File.
В файле polyspace_controller_demo.c, в функциональном polyspace_controller_demo_step(), выберите нарушение правила 10.4 MISRA C:2012. Панель 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 предварительно заполняются с вашими аннотациями.