Можно запустить Polyspace® на коде, сгенерированном из модели Simulink® или подсистемы.
Polyspace Bug Finder™ проверяет код на ошибки или кодирующий нарушения правила (например, MISRA C®: 2 012 правил).
Polyspace Code Prover™ исчерпывающе проверяет код на ошибки времени выполнения.
Если вы используете Embedded Coder® для генерации кода, этот пример показывает, как запустить Polyspace на сгенерированном коде из Simulink.
Прежде чем вы запустите Polyspace от Simulink, необходимо соединить Polyspace и установки MATLAB®. Смотрите Интегрируют Polyspace с MATLAB и Simulink.
Откройте модель в качестве примера.
modelName = 'psdemo_model_link_sl';
open_system(modelName)
Сгенерируйте код для подсистемы controller в вашей модели.
Щелкните правой кнопкой по подсистеме controller и выберите C/C++ Code> Build This Subsystem.
В диалоговом окне выберите Build.
Эквивалентный код MATLAB:
subsysPath = 'psdemo_model_link_sl/controller';
rtwbuild(subsysPath);Анализируйте код, сгенерированный для подсистемы controller.
Выберите продукт, Средство поиска Ошибки или Программу автоматического доказательства Кода, чтобы анализировать код.
Щелкните правой кнопкой по подсистеме controller и выберите Polyspace> Options. Для Product mode выберите Code Prover или Bug Finder.
Анализируйте сгенерированный код.
Щелкните правой кнопкой по подсистеме controller и выберите Polyspace> Verify Generated Code for> Selected Subsystem. Следуйте за прогрессом анализа в Окне Команды MATLAB.
Эквивалентный код MATLAB:
opts = polyspace.ModelLinkOptions('C'); mlopts = pslinkoptions(subsysPath); mlopts.VerificationMode = 'CodeProver'; mlopts.PrjConfigFile = generateProject(opts, 'polyspaceProject'); pslinkrun(subsysPath, mlopts);
CodeProver на BugFinder. Для получения дополнительной информации о коде смотрите polyspace.ModelLinkOptions, pslinkoptions и pslinkrun.После анализа результаты отображены в пользовательском интерфейсе Polyspace.
Если при запуске Средство поиска Ошибки, результаты состоят из ошибок, обнаруженных в сгенерированном коде. Если при запуске Программу автоматического доказательства Кода, результаты состоят из проверок, на которые наносят цветную маркировку можно следующим образом:
Зеленый (доказанный код): проверка не перестала работать для обеспеченных ограничений данных. Например, операция деления не вызывает ошибку 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 в подсистеме controller.
Для кода, сгенерированного из модели, можно проследить ошибку до модели. Эти разделы показывают, как проследить определенные результаты Программы автоматического доказательства Кода до модели.
На панели Results List выберите оранжевую ошибку Out of bounds array index, которая происходит в файле controller.c.
На панели Source щелкните по ссылке S5:76 в комментариях выше оранжевой ошибки.
/* Transition: '<S5>:75' */ /* Transition: '<S5>:76' */ (*i)++; /* Outport: '<Root>/FaultTable' */ controller_Y.FaultTable[*i] = 10;
Вы видите, что ошибка происходит из-за перехода в диаграмме Stateflow synch_and_asynch_monitoring. Можно проследить ошибку до индекса входной переменной диаграммы Stateflow.
Можно избежать Out of bounds array index несколькими способами. Один путь состоит в том, чтобы ограничить входную переменную index с помощью блока Saturation перед диаграммой Stateflow.
На панели Results List выберите оранжевую ошибку Overflow, показанную ниже. Ошибка появляется в файле controller.c.
На панели Source рассмотрите ошибку. Чтобы проследить ошибку до модели, щелкните по ссылке S2/Gain в комментариях выше оранжевой ошибки.
/* Gain: '<S2>/Gain' incorporates: * Inport: '<Root>/Battery Info' * Inport: '<Root>/Rotation' * Sum: '<S2>/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 подсистеме controller.
На вкладке Signal Attributes измените значение Maximum сигнала.
Ошибки в этой модели происходят из-за одного из следующего:
Дефектное масштабирование, неизвестные калибровки и непротестированные области значений данных, выходящие из подсистемы в арифметический блок.
Манипуляция с массивами в Stateflow основанное на событии моделирование и рукописные функции интерполяционной таблицы.
Продвижение насыщения к неожиданному потоку данных в сгенерированном коде.
Дефектное программирование Stateflow.
Если вы идентифицируете первопричину ошибки, можно изменить модель соответственно, чтобы устранить проблему.
Проверять на кодирование нарушений правила, прежде, чем запустить анализ кода:
Щелкните правой кнопкой по подсистеме controller и выберите Polyspace> Options.
В диалоговом окне Configuration Parameters выберите подходящий вариант в списке Settings from. Например, выберите Project configuration and MISRA C 2012 AGC Checking.
Рекомендуется, чтобы вы запустили Средство поиска Ошибки для проверки правил MISRA C:2012. Для Product mode выберите Bug Finder.
Нажмите Apply или OK и повторно выполните анализ.
Можно выровнять по ширине результаты путем добавления аннотаций в блоки. Во время анализа кода Polyspace Code Prover читает ваши аннотации и заполняет результат с вашим выравниванием. Если вы выравниваете по ширине результат, вы не должны рассматривать его снова.
На панели Results List, из выпадающего списка в левом верхнем углу, выбирают File.
В файле controller.c, в функциональном controller_step(), выбирают нарушение правила 10.4 MISRA C:2012. Панель Source показывает, что операция сложения нарушает правило.
На панели Source щелкните по ссылке S2/Sum1 в комментариях выше операции сложения.
/* Gain: '<S2>/Gain' incorporates: * Inport: '<Root>/Battery Info' * Inport: '<Root>/Rotation' * Sum: '<S2>/Sum1' */ Gain = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >> 10);
Вы видите, что нарушение правила происходит в блоке Sum.
Аннотировать этот блок и выровнять по ширине нарушение правила:
Щелкните правой кнопкой по блоку и выберите Polyspace> Annotate Selected Block> Edit.
Выберите MISRA-C-2012 for Annotation type и введите информацию о нарушении правила. Установите Status на No action planned и Severity к Unset.
Нажмите Apply или OK. Polyspace annotation слов появляется ниже блока, указывая, что блок содержит аннотацию кода.
Регенерируйте код и повторно выполните анализ. Severity и столбцы Status на панели Results List предварительно заполняются с вашими аннотациями.