Запуск анализа Polyspace на пользовательском коде в блоках вызывающего абонента на C и диаграммах Stateflow

Можно проверить на ошибки и ошибки времени выполнения в пользовательском коде C/C + +, используемом в Simulink® модель. Polyspace® анализ проверяет функции, вызываемые из блоков C Caller и Stateflow® графики с входами от модели.

Необходимые условия

Прежде чем запускать Polyspace из Simulink, необходимо связать Polyspace и MATLAB® установки. См. «Интеграция Polyspace с MATLAB и Simulink».

Чтобы открыть модели, используемые в этом примере, смотрите этот пример в браузере MATLAB Help и нажмите кнопки Open Model.

Функция C/C + +, вызываемая один раз в модели

Этот пример использует функцию, вызываемую только один раз в модели из блока C Caller (Simulink). Анализ проверяет функцию с помощью входов в блок C Caller.

Откройте модель для выполнения анализа на пользовательском коде

Откройте модель mSlccBusDemo для анализа пользовательского кода с Polyspace. Модель содержит блок C Caller, который вызывает функцию counterbusFcn заданный в файл hCounterBus.c (заявлен в файле hCounterBus.h). Модель использует переменные, сохраненные в файле MAT dLctData.mat, который загружается в модель с помощью коллбэка.

Запуск анализа

Сконфигурируйте опции анализа и запустите Polyspace.

  1. На вкладке Apps выберите Polyspace Code Verifier, чтобы открыть вкладку Polyspace.

  2. Укажите тип анализа:

    • Выберите продукт для запуска, Bug Finder или Code Prover.

    • Укажите, что анализ должен выполняться на пользовательском коде в модели вместо сгенерированного кода.

      В Analyze Code from поле показано имя модели. Под полем вместо Code Generated as Top Model выберите Custom Code Used in Model.

  3. Выберите Run Analysis.

    Следите за прогрессом анализа в Командном Окне MATLAB. После анализа на вкладке Polyspace выберите Analysis Results. Результаты откроются в пользовательском интерфейсе Polyspace.

Можно также запустить тот же анализ из MATLAB следующим образом. Скрипт включает команды для загрузки модели и .mat файл, содержащий переменные, используемые в модели.

openExample('polyspace_code_prover/OpenModelForRunningAnalysisOnCustomCodeExample');
load_system('mSlccBusDemo');
load('dLctData.mat');

mlopts = pslinkoptions('mSlccBusDemo'); 
mlopts.VerificationMode = 'CodeProver'; 
pslinkrun('-slcc','mSlccBusDemo',mlopts);

Исправление проблем

Результаты анализа появляются на панели Results List в пользовательском интерфейсе Polyspace. Выберите каждый результат и см. дополнительные сведения на панели Result Details и соответствующий исходный код на панели Source.

Остальная часть этого руководства показывает, как исследовать и устранить проблемы, обнаруженные в анализе Code Prover. Аналогичные шаги могут быть выполнены для проблем, найденных с Bug Finder.

Если вы запускаете анализ Code Prover, результаты содержат оранжевую проверку Overflow.

Проверка подсвечивает операцию сложения в counterbusFcn функция, которая может переполниться:

limit = u1->inputsignal.input + u2;
Операнды поступают от входов к counterbusFcn, который, в свою очередь, поступает от этих входов в блок C Caller:

  • Сигнал шины COUNTERBUS, который объединяет сигналы input, upper_saturation_limit и lower_saturation_limit. Сигнал input неограниченно.

  • Обратная связь от самого C Caller через блок Delay.

Можно ограничить сигнал input несколькими способами. Например, можно ограничить переменную сигнала шины SIGNALBUS который исходит от input:

  1. В редакторе Simulink откройте браузер Model Explorer на вкладке Modeling.

  2. Базовые рабочие пространства содержат переменную SIGNALBUS. Выберите эту переменную и откройте редактор шины для редактирования этой переменной. Задайте минимальное и максимальное значение для переменной.

    Сохраните объект шины в MAT-файле. Можно перезаписать файл dLctData.mat или создать файл.

Можно также ограничить обратную связь от блока C Caller несколькими способами. Например, можно насыщать сигнал обратной связи:

  1. Добавьте блок Насыщения непосредственно перед входом сигнала обратной связи в блок C Caller.

  2. На вкладке Signal Attributes задайте минимальное и максимальное значение для выхода блока Насыщения.

    Обратите внимание, что установка нижнего и верхнего предела на вкладке Main блока Насыщения недостаточно для ограничения сигнала для анализа Polyspace. В анализе используются области значений проекта, заданные на вкладке Signal Attributes.

Перезапустите анализ. Сдача Overflow на хранение нового набора результатов выполняется зеленым цветом.

Функция C/C + + называется несколько раз в модели

Этот пример использует функцию, вызываемую из нескольких блоков C Caller в модели. Функция просто возвращает продукт двух аргументов.

Пример запускает анализ Code Prover и показывает, как определить контекст вызова функции, начиная с результатов Code Prover. Как правило, при анализе Bug Finder не нужно различать различные контексты вызовов.

Откройте модель для анализа всего пользовательского кода

Откройте модель multiCCallerBlocks для выполнения анализа Polyspace.

openExample('polyspace_bf/OpenModelForAnalyzingAllCustomCodeExample');
open_system('multiCCallerBlocks');

Осмотрите модель

Модель содержит два блока C Caller, вызывающих одну и ту же функцию times_n. Входы в один блок C Caller поступают из двух блоков Inport, которые имеют неограниченный вход. Входы в другой блок C Caller поступают из блока Constant и блока Inport, вход которого ограничен блоком Насыщения.

Чтобы увидеть области значений проекта для блока C Caller, который имеет ограниченные входы:

  • Дважды кликните блок Константа или блок Насыщение.

  • На вкладке Signal Attributes обратите внимание на область значений проекта.

    Например, хотя блок Constant имеет постоянное значение, установленное в 3, диапазон проекта для проверки составляет 2,5-3,5.

    Проект области значений для блока Saturation - [-1,1].

Запуск анализа и анализ результатов

Выполните анализ как в предыдущем примере и откройте результаты.

На Results List панели отображается оранжевая проверка Overflow. Продукт в times_n переполнение функции.

#include "file.h"

double times_n(double x, double n) {
  return x * n;
}
Потому что times_n функция вызывается из двух контекстов, оранжевый цвет объединяет оба контекста и может указывать на две возможные ситуации:

  • Переполнение происходит в обоих контекстах вызова.

  • Переполнение, как доказано, не происходит в одном контексте (зеленая проверка) и может происходить в другом контексте (оранжевая проверка).

Чтобы определить, какой контекст вызова приводит к переполнению:

  1. Видеть всех вызывающих абонентов times_n.

    Выберите оранжевый цвет Overflow проверки. На панели Result Details щелкните. На Call Hierarchy панели показаны вызывающие абоненты times_n.

  2. На панели Call Hierarchy вы видите две функции оболочки как вызывающие. Каждая функция обертки представляет блок C Caller в модели.

    Выберите одну из функций-оболочек, чтобы открыть исходный код для customcode_wrappers.c.

  3. На панели Source проверьте код функций оболочки. Чтобы определить, какие входы приводят к переполнению, используйте всплывающие подсказки на подчеркнутых входах.

    Например, функция обертки для блока C Caller, который имеет ограниченные входы, выглядит аналогично этому коду:

    /* Go to model '<Root>/C Caller1' */
    /* Variables corresponding to inputs for block C Caller1 */
     real64_T _pslink_C_Caller1_In1;
     real64_T _pslink_C_Caller1_In2;
    /* Variables corresponding to outputs for block C Caller1 */
     real64_T _pslink_C_Caller1_Out1;
    /* Wrapper functions for code in block C Caller1 */
    void _pslink_step_C_Caller1(void) {
        /* See tooltips on function inputs for input ranges */
        _pslink_C_Caller1_Out1 = times_n(_pslink_C_Caller1_In1, _pslink_C_Caller1_In2);
    }
    Используйте подсказки к переменным, чтобы определить их области значений. Для образца всплывающая подсказка на переменной _pslink_C_Caller1_In1 показывает, что он находится в области значений [2,5, 3,5] и подсказка на _pslink_C_Caller1_In2 показывает, что он находится в области значений [-1,1]. Поэтому продукт двух входов не может переполниться. Переполнение должно происходить из другого контекста вызова. Вы можете увидеть всплывающие подсказки на входах к другому вызову и подтвердить, что переменные неограниченны.

    Чтобы найти блок C Caller, относящийся к функции обертки, на панели Source щелкните ссылку на имя синего блока над функцией обертки (в линии, начинающейся с Go to model). Блок C Caller подсвечивается в модели.

Включите контекстную чувствительность и повторный анализ

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

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

В этом примере, чтобы включить контекстную чувствительность для times_n функция:

  1. В модели на вкладке Polyspace выберите Settings > Project Settings.

    Кроме того, в пользовательском интерфейсе Polyspace выберите Project Browser. Откройте строение проекта, созданную для анализа.

  2. На узле Code Prover Verification > Precision выберите custom для Sensitivity context опций. В Procedure поле нажмитеplus button и введите times_n.

    См. также Sensitivity context (-context-sensitivity) (Polyspace Code Prover).

Перезапустите анализ из модели и снова откройте результаты. Выберите оранжевый цвет Overflow проверки.

На Result Details панели показаны контексты вызова отдельно. Можно увидеть, что переполнение происходит только для вызова с неограниченными входами (строка с оранжевым текстом) и не происходит для другого вызова (строка с зеленым текстом).

Щелкните строку с оранжевым текстом, чтобы непосредственно перейти к функции обертки, ведущей к оранжевой проверке. Из функции обертки можно перейти к блоку C Caller с неограниченными входами.

См. также

|

Похожие темы