Настройте существующий шаблон отчета программы автоматического доказательства кода

В этом примере вы изучаете, как настроить существующий шаблон отчета, чтобы удовлетворить вашим требованиям. Шаблон отчета задает содержимое и форматирование отчетов, сгенерированных от результатов анализа. Если существующий шаблон отчета не удовлетворяет вашим требованиям, можно изменить определенные аспекты шаблона.

Для получения дополнительной информации о существующих шаблонах смотрите Bug Finder and Code Prover report (-report-template).

Предпосылки

Прежде чем вы настроите шаблон отчета:

  • Смотрите, удовлетворяет ли существующий шаблон отчета ваши требования. Идентифицируйте шаблон, который представляет отчеты в формате близко к тому, в чем вы нуждаетесь. Можно адаптировать этот шаблон.

    Чтобы протестировать шаблон, сгенерируйте отчет от демонстрационных результатов верификации с помощью шаблона. Смотрите Генерируют Отчеты.

  • Убедитесь, что вам установили MATLAB® Report Generator™ в вашей системе.

В этом примере вы изменяете шаблон Developer, который доступен в Polyspace® Code Prover™.

Просмотрите компоненты шаблона

Шаблон отчета может быть поврежден на компоненты в MATLAB Report Generator. Каждый компонент представляет часть информации, которая включена в отчет, сгенерированный с помощью шаблона. Например, Title Page компонента представляет информацию в титульном листе отчета.

В этом примере вы просматриваете компоненты шаблона Developer.

  1. Добавьте пути к специфичным для Polyspace компонентам отчета, указав на подпапки вашей папки установки Polyspace. В командной строке MATLAB введите:

    addpath(fullfile(polyspaceroot, 'toolbox', 'polyspace', 'psrptgen', 'psrptgen'));
    addpath(fullfile(polyspaceroot, 'toolbox', 'polyspace', 'psrptgen', 'templates'));

    Здесь, polyspaceroot папка установки Polyspace, например, C:\Program Files\Polyspace\R2019a. Если вы интегрируете MATLAB и Polyspace, можно использовать polyspaceroot функция в MATLAB, чтобы найти местоположение папки установки. Смотрите Интегрируют Polyspace с MATLAB и Simulink.

  2. Откройте интерфейс Report Explorer Генератора отчетов Simulink®. В командной строке MATLAB введите:

    report

  3. Откройте шаблон Developer в интерфейсе Report Explorer.

    Шаблон Developer находится в polyspaceroot/toolbox/polyspace/psrptgen/templates где polyspaceroot папка установки Polyspace.

Ваш шаблон открывается в Report Explorer. На левой панели вы видите компоненты шаблона. Можно кликнуть по каждому компоненту и просмотреть свойства компонентов на правой панели.

Некоторые компоненты шаблона Developer и их цели описаны ниже.

КомпонентЦель
Title Page

Вставляет титульный лист в начале отчета

Chapter/Subsection

Фрагменты групп отчета в разделы с заголовками

Code Verification Summary

Вставляет сводную таблицу результатов анализа Polyspace

Logical If

Выполняет дочерние компоненты, только если условию удовлетворяют

Run-time Checks Summary Ordered by File

Вставляет таблицу с проверками Polyspace Code Prover, сгруппированными файлом

Чтобы изучить, как шаблон работает, сравните компоненты в шаблоне с отчетом, сгенерированным с помощью шаблона.

Для получения дополнительной информации обо всех компонентах см. документацию MATLAB Report Generator. Для получения информации о специфичных для Polyspace компонентах смотрите, Генерируют Отчеты.

Примечание

Некоторые свойства компонентов установлены с помощью внутренних выражений. Несмотря на то, что можно просмотреть выражения, не изменяйте их. Например, условия, заданные в компонентах Logical If в шаблоне Developer, заданы с помощью внутренних выражений.

Измените компоненты шаблона

В интерфейсе Report Explorer вы можете:

  • Измените свойства существующих компонентов вашего шаблона.

  • Добавьте новые компоненты в свой шаблон или удалите существующие компоненты.

В этом примере вы добавляете компонент в шаблон Developer, который фильтрует Unreachable code проверки из отчета, сгенерированного с помощью шаблона.

  1. Откройте шаблон Developer в интерфейсе Report Explorer и сохраните его в другом месте с другим именем, например, Developer_without_UNR.

  2. Добавьте новый глобальный компонент, который фильтрует проверки Unreachable code из шаблона Developer_without_UNR. Компонент является глобальной переменной, потому что это применяется к полному отчету и не одной главе отчета.

    Выполнять это действие:

    1. Перетащите Report Customization (Filtering) компонента от средней панели и отбрасывания это выше компонента Title Page. Расположение компонента гарантирует, что фильтры применяются к полному отчету и не одной главе отчета.

    2. Выберите компонент Report Customization (Filtering). На правой панели можно установить свойства этого компонента. По умолчанию свойства установлены таким образом, что все результаты включены в отчет.

      Чтобы исключить проверки Unreachable code, под группой Advanced Filters, вводят ^(?!Unreachable code).* в поле Check types to include.

      Можно ввести регулярные выражения MATLAB в это поле. Генератор отчетов применяет регулярные выражения против имен результата Polyspace. Например:

      • Каре ^ указывает, что последующий шаблон должен быть в начале строки.

      • Символы (?! pattern) указывает, что последующий шаблон не должен появляться в строке.

      Вместе, регулярное выражение ^(?!Unreachable code).* указывает, что Polyspace заканчивается имена, начинающиеся с Unreachable code должен быть исключен из отчета. Смотрите Регулярные выражения Результаты Polyspace Code Prover и (MATLAB).

      Можно переключиться между активацией и деактивацией этого компонента. Щелкните правой кнопкой по компоненту и выберите Activate/Deactivate Component.

  3. Измените существующий специфичный для главы компонент так, чтобы он не заменял глобальный фильтр, который вы применили на предыдущем шаге. Если вы предотвращаете переопределение, специфичный для главы компонент следует техническим требованиям фильтрации в глобальном компоненте.

    Выполнять это действие:

    1. На левой панели выберите Run-time Checks Details Ordered by Color/File компонент. Этот компонент производит таблицы в отчете с деталями проверок на этапе выполнения, найденных в Polyspace Code Prover.

      Правая панель показывает свойства этого компонента.

    2. Очистите поле фильтра Override Global Report.

  4. В пользовательском интерфейсе Polyspace создайте отчет с помощью обоих шаблон Developer и Developer_without_UNR от результатов, содержащих проверки Unreachable code. Сравните два отчета.

    Например:

    1. Откройте Help> Examples> Code_Prover_Example.psprj.

      Демонстрационный результат содержит проверки Unreachable code.

    2. Создайте отчет PDF с помощью шаблона Developer.

      В отчете откройте Главу 5. Результаты Проверок на этапе выполнения Polyspace. Вы видите серые проверки Unreachable code. Закройте отчет.

    3. Создайте отчет PDF с помощью шаблона Developer_without_UNR. В окне Run Report используйте кнопку Browse, чтобы добавить шаблон Developer_without_UNR в существующий список шаблонов.

      В отчете откройте Главу 6. Результаты Проверок на этапе выполнения Polyspace. Вы не видите серые проверки Unreachable code.

      Примечание

      После того, как вы добавите, что шаблон к существующему списку шаблонов, прежде, чем сгенерировать отчет, убеждается, что выбрал недавно добавленный шаблон.

Дальнейшее исследование

Измените шаблон Developer, таким образом что файл initialisations.c исключен из отчета, сгенерированного с помощью шаблона. Сгенерируйте отчет от результатов Code_Prover_Example с помощью модифицированного шаблона и проверьте что файл initialisations.c исключен из отчета.

Подсказка: регулярным выражением, которое необходимо использовать, является ^(?!.*initialisations.c).*

Для большего количества примеров смотрите Демонстрационные Индивидуальные настройки шаблонов Отчета.

Смотрите также

| |

Похожие темы