Можно запустить Polyspace ® для кода, созданного в модели или подсистеме Simulink ®.
Polyspace Bug Finder™ проверяет код на наличие ошибок или нарушений правил кодирования (например, правил MISRA C ®: 2012).
Polyspace Code Prover™ тщательно проверяет код на наличие ошибок во время выполнения.
Если для создания кода используется Embedded Coder ®, в этом учебном пособии показано, как запустить Polyspace для кода, созданного на основе простой модели Simulink. Полный рабочий процесс см. в разделе Выполнение анализа полиспейса для кода, созданного с помощью встроенного кодера.
Перед запуском Polyspace из Simulink необходимо связать установки Polyspace и MATLAB ®. См. раздел Интеграция полиспейса с MATLAB и Simulink.
Чтобы открыть модель, используемую в этом примере, в окне команд MATLAB выполните следующее:
openExample('polyspace_code_prover/OpenModelForCodeGenerationAndPolyspaceAnalysisExample')Открытие модели polyspace_controller_demo для настройки генерации кода и анализа Polyspace.
Чтобы запустить анализ Polyspace кода, созданного из модели, выполните следующие действия.
На вкладке «Приложения» выберите «Верификатор кода Polyspace».
На вкладке Полиспейс (Polyspace) найдите поле Анализ (Analyze) и в раскрывающемся меню выберите Код, созданный как верхняя модель (Code Generated as Top model).
Щелкните в любом месте полотна. В поле Analyze Code from отображается имя модели. Выберите Выполнить анализ (Run Analysis).
При нажатии кнопки Выполнить анализ (Run Analysis) Полиспейс проверяет созданный код. Если созданный код отсутствует, Polyspace сначала генерирует код с помощью встроенного кодера, а затем начинает анализ.
Эквивалентный код 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.
При запуске средства поиска ошибок результаты состоят из ошибок, обнаруженных в сгенерированном коде. При запуске программы Code Prover результаты состоят из проверок, которые кодируются следующим образом:
Зеленый (проверенный код): Проверка ограничений данных не завершается неуспешно. Например, операция деления не вызывает ошибки деления на нуль.
Красный (проверенная ошибка): Проверка набора ограничений данных всегда завершается неуспешно. Например, операция деления всегда вызывает ошибку деления на ноль.
Оранжевый (возможная ошибка): проверка указывает на неподтвержденный код и может привести к сбою для определенных значений ограничений данных. Например, операция деления иногда вызывает ошибку деления на ноль.
Серый (недоступный код): проверка указывает на операцию кода, которая не может быть достигнута для предоставленных ограничений данных.
Просмотрите каждый результат анализа подробно. Например, в результатах проверки кода:
На панели Список результатов (Results List) выберите красную проверку индекса массива Вне границ (Out of bounds).
На панели «Источник» установите курсор на красную галочку для просмотра дополнительной информации. Например, подсказка на красном [ оператор указывает размер массива и возможные значения индекса массива. Эта информация также отображается на панели Сведения о результате (Result Details).
Ошибка возникает в рукописном файле C Command_strategy_file.c. Файл C находится внутри S-функционального блока Command_Strategy в Reduced Precision подсистема (в ссылке модели relative threshold).
Для кода, созданного из модели, можно отследить ошибку в модели. В этих разделах показано, как отслеживать определенные результаты проверки кода в модели.
На панели «Список результатов» выберите оранжевую ошибку индекса массива Out of bounds, которая возникает в файле. polyspace_controller_demo.c.
На панели «Источник» щелкните ссылку, 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 можно избежать несколькими способами. Один из способов - ограничить входную переменную index использование блока Насыщения перед диаграммой потока состояний.
На панели «Список результатов» выберите оранжевую ошибку переполнения, показанную ниже. Ошибка появляется в файле polyspace_controller_demo.c.
На панели «Источник» просмотрите ошибку. Чтобы отследить ошибку в модели, щелкните ссылку 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 подсистема внутри блока усиления, следующего за блоком суммы.
Можно избежать переполнения несколькими способами. Одним из способов является ограничение значения сигнала in_battery_info который подается в блок Суммы. Для ограничения сигнала:
Дважды щелкните блок «Ввод» Battery info который обеспечивает входной сигнал in_battery_info к модели.
На вкладке Signal Attributes (Атрибуты сигнала) измените максимальное значение сигнала.
Ошибки в этой модели возникают из-за одной из следующих причин:
Ошибочное масштабирование, неизвестные калибровки и непроверенные диапазоны данных, выходящие из подсистемы в арифметический блок.
Манипулирование массивом при моделировании на основе событий Stateflow и функции рукописной таблицы поиска.
Насыщения, приводящие к непредвиденному потоку данных внутри созданного кода.
Неисправное программирование Stateflow.
После определения первопричины ошибки можно соответствующим образом изменить модель, чтобы устранить проблему.
Чтобы проверить нарушения правил кодирования, перед началом анализа кода:
На вкладке «Полиспейс» выберите «Параметры».
В диалоговом окне Параметры конфигурации (Configuration Parameters) выберите соответствующую опцию в списке Настройки из (Settings from). Например, выберите Project configuration and MISRA C 2012 AGC Checking.
Рекомендуется запустить средство поиска ошибок для проверки правил C:2012 MISRA. На вкладке «Полиспейс» выберите «Поиск ошибок».
Щелкните Применить (Apply) или ОК (OK) и повторно запустите анализ.
Результаты можно выровнять, добавив аннотации к блокам. Во время анализа кода программа Polyspace Code Prover считывает аннотации и заполняет результат выравниванием. Как только вы оправдываете результат, вам не придется пересматривать его снова.
На панели Список результатов (Results List) в раскрывающемся списке в левом верхнем углу выберите Файл (File).
В файле polyspace_controller_demo.c, в функции polyspace_controller_demo_step()выберите нарушение MISRA C:2012 правило 10.4. На панели «Источник» показано, что операция добавления нарушает правило.
На панели «Источник» щелкните ссылку, 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.
Чтобы аннотировать этот блок и обосновать нарушение правила, выполните следующие действия.
Выберите блок. На вкладке «Полиспейс» выберите «Добавить аннотацию».
Выбрать MISRA-C-2012 в поле Тип аннотации (Annotation type) и введите сведения о нарушении правила. Установите для действия Статус (Status) значение Нет запланированного (No planned), а для действия Серьезность (Severity) значение Отменить (Unset).
Нажмите кнопку Apply (Применить) или OK. Под блоком появляются слова Polyspace annotation, указывающие на то, что блок содержит аннотацию кода.
Выполните регенерацию кода и повторно запустите анализ. Столбцы Серьезность (Severity) и Статус (Status) на панели Список результатов (Results List) заполняются аннотациями.