Этот пример описывает, как открыть результаты Polyspace® Code Prover™ для AUTOSAR-специфичного кода и интерпретировать результаты, которые подсвечивают нарушение ограничений данных в ARXML.
Программа автоматического доказательства кода проверяет реализацию кода компонентов программного обеспечения AUTOSAR для несоответствия со спецификациями в ARXML. Например, если аргумент функции RTE имеет значение вне ограниченной области значений, заданной в ARXML, анализ отмечает возможную проблему.
Чтобы выполнить шаги в этом примере, запустите Polyspace на демонстрационных файлах в |
Если при запуске анализ в пользовательском интерфейсе Polyspace, можно открыть каждый результат непосредственно. Дважды кликните результат, который вы хотите открыть.
Если при запуске анализ при помощи скриптов после анализа, можно открыть результаты несколькими способами.
Откройте файл psar_project.xhtml от вашей папки проекта в веб-браузере. Вы видите обзор результатов для всех компонентов программного обеспечения и перешли к результатам для каждого компонента программного обеспечения. Для получения дополнительной информации смотрите, См. Обзор Результатов для всех Компонентов программного обеспечения.
Откройте файл psar_project.psprj от вашей папки проекта в пользовательском интерфейсе Polyspace. Откройте каждый результат на панели Project Browser.
Перейдите к папкам, содержащим отдельные файлы результатов. Откройте файл результата (с дополнительным .pscp) в пользовательском интерфейсе Polyspace.
Файлы результатов хранятся в подпапке AUTOSAR папки проекта. Путь к каждому результату следует за полностью определенным именем внутреннего поведения компонента программного обеспечения. Например, для полностью определенного имени pkg.component.bhv, результаты хранятся в AUTOSAR\pkg\component\bhv\verification (итоговую подпапку называют CP_Result, если вы запускаете верификацию в пользовательском интерфейсе Polyspace).
Прежде, чем открыть определенный набор результатов, вы можете хотеть видеть обзор результатов для всех компонентов программного обеспечения. Выполнить одно из следующих действий:
Откройте файл psar_project.xhtml в вашей папке проекта.
Загрузите файлы результата на Метрики Polyspace. Чтобы начаться, смотрите, Генерируют Метрики качества Кода.
Используйте первый метод для более легкого понимания результатов.
В файле psar_project.xhtml кликните
по значку на верхнем левом углу. На левой панели нажмите Behaviors. Вы видите список всех компонентов программного обеспечения, внутренние поведения которых извлечены.
Можно отфильтровать этот список, чтобы отобразить только компоненты программного обеспечения, которыми вы интересуетесь. Чтобы видеть определенные компоненты программного обеспечения, в поле поиска, вводят полностью определенное имя компонента программного обеспечения, которым вы интересуетесь.
Можно также ввести регулярные выражения, чтобы видеть несколько компонентов. Например, чтобы видеть все компоненты, полностью определенные имена которых начинаются с pkg.tst002.swc001, введите выражение:
^pkg.tst002.swc001.*
Нажмите Search. Список на праве отображает только компоненты программного обеспечения, для которых вы запросили.
Можно также отфильтровать компоненты на основе других критериев:
Успешность или неуспешность верификации
Чтобы видеть только компоненты программного обеспечения, которые завершили верификацию, кликните и затем очистите фильтр error status.
Присутствие или отсутствие определенных видов результатов, например, красных проверок
Чтобы видеть только компоненты программного обеспечения, которые имеют красные проверки, щелкните, все на строке, содержащей red, фильтрует кроме самого фильтра red.
Для каждого компонента программного обеспечения вы видите эту информацию в файле psar_project.xhtml в вашей папке проекта (см. предыдущую фигуру).
Состояние этого компонента программного обеспечения относительно анализа. Таким образом, была ли спецификация компонента программного обеспечения проанализирована, ее исходный код, извлеченный, и затем анализировала с Программой автоматического доказательства Кода.
Чтобы убедиться, что анализ Программы автоматического доказательства Кода был завершен под разделом Verification of extracted implementation code, ищут этот оператор:
State after last command execution: updated.Функции обеспечиваются этим компонентом программного обеспечения, и функции Rte_ используются.
Чтобы видеть этот список, щелкните по ссылке:
See key autosar definition for this behaviorГрафическое представление runnables в компоненте программного обеспечения. Графическое представление показывает:
Функции точки входа, реализующие runnables и их вызываемых
Файлы, содержащие эти функции
Чтобы видеть это представление, в списке компонентов программного обеспечения на левой панели, нажатие кнопки
(график поведения) значок для компонента программного обеспечения, вы интересуетесь. Чтобы возвратиться от графика до текстового описания компонента программного обеспечения, щелкните
(страница поведения) значок.
В этом примере вы видите, что компонент программного обеспечения с внутренним поведением bhv001 имеет три runnables, реализованные через функции точки входа foo, init и step. Все три функции точки входа заданы в файле swc001.c.
Функциональный step вызывает функции, определяемые в других файлах, например, dep3.c. Можно кликнуть
по значку для step, чтобы видеть только файлы, вовлеченные в реализацию выполнимого step. Чтобы вернуться к полному графическому представлению компонента программного обеспечения, щелкните где угодно в пробеле в графике.
Обзор Программы автоматического доказательства Кода заканчивается со ссылками на файлы результата.
Ищите строки как эти строки:
Verification results are in summary: green check=84, orange check=2, red check=1
.pscp прежде, щелкание по ссылке может просто загрузить файл результата. Убедитесь, что файлы .pscp всегда открываются в пользовательском интерфейсе Polyspace (с исполняемым polyspaceroot\polyspace\binpolyspacerootРезультаты состоят из AUTOSAR-специфичных проверок на этапе выполнения, таких как Invalid result of AUTOSAR runnable implementation и общие проверки на этапе выполнения C/C++, такие как Division by zero.
На панели Results List выберите результат Invalid result of AUTOSAR runnable implementation или Invalid use of AUTOSAR runtime environment function. Исследуйте результат далее при помощи информации о различных панелях.
Используя информацию о панели Result Details, определите, нарушают ли возвращаемое значение или аргумент ограничения данных в ARXML или могут быть с пустым знаком. Ищите! значок, который указывает на определенную ошибку или? значок, который указывает на возможную ошибку.
Для возвращаемого значения и каждого аргумента, вы видите фактические возможные значения во время выполнения, и значения, позволенные по условию, вводят в спецификации ARXML. Сравните их и найдите значение, которое не позволено.
Invalid result of AUTOSAR runnable implementation результата определяет, может ли возвращаемое значение функции, реализующей выполнимое или выходные аргументы, нарушить ограничения данных. Invalid use of AUTOSAR runtime environment function результата определяет, нарушают ли входные параметры к функции Rte_ ограничения данных.
Иногда, вы можете хотеть видеть Тип Данных приложения, из которого происходит переменная Base Software Type. Щелкните по синей ссылке спецификации параметра и смотрите, что ARXML извлекает, который описывает эту информацию о типе данных возвращаемого значения или значении параметров:
Тип данных приложения, тип данных реализации и основной тип программного обеспечения
Ограничение данных, модуль и метод вычисления
Займитесь расследованиями, как переменная получает значения, которые нарушают ограничения данных. Чтобы проследить в вашем коде, на панели Source, щелкают правой кнопкой по переменной и ищут все ее экземпляры или перешли к ее определению. Для большего количества советов смотрите, Интерпретируют Результаты Polyspace Code Prover.
Решите, зафиксировать ли ваш код или ARXML, или выровнять по ширине результат через комментарии. Смотрите Результаты Polyspace Адреса Через Исправления ошибок или Комментарии.
Invalid result of AUTOSAR runnable implementation | Invalid use of AUTOSAR runtime environment function