Можно проверять на ошибки и ошибки времени выполнения в пользовательском коде C/C++, используемом в модели Simulink®. Анализ Polyspace® проверяет функции, вызванные от блоков Вызывающей стороны C и графиков Stateflow® с входными параметрами из модели.
Прежде чем вы запустите Polyspace от Simulink, необходимо соединить Polyspace и установки MATLAB®. Смотрите Интегрируют Polyspace с MATLAB и Simulink.
Чтобы открыть модели, используемые в этом примере, ищите этот пример в Браузере документации MATLAB и нажмите кнопки Open Model.
Этот пример использует функцию, вызванную только однажды в модели от блока C Caller (Simulink). Анализ проверяет входные параметры использования функции с блоком C Caller.
Откройте модель mSlccBusDemo для анализа пользовательского кода с Polyspace. Модель содержит блок C Caller, который вызывает функциональный counterbusFcn заданный в файле hCounterBus.c (объявленный в файле hCounterBus.h). Модель использует переменные, сохраненные в файле MAT dLctData.mat, который загружается в модели с помощью коллбэка.
Сконфигурируйте Polyspace запуска и опции анализа.
На вкладке Apps выберите Polyspace Code Verifier, чтобы открыть вкладку Polyspace.
Задайте тип анализа:
Выберите продукт, чтобы запуститься, Bug Finder или Code Prover.
Укажите, что анализ должен работать на пользовательском коде в модели вместо сгенерированного кода.
Поле Analyze Code from показывает имя модели. Ниже поля, вместо Code Generated as Top Model, выбирают Custom Code Used in Model.
Выберите 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.
Остальная часть этого примера показывает, как исследовать и устранить проблемы, найденные в анализе Программы автоматического доказательства Кода. Подобные шаги могут быть выполнены для проблем, найденных с Bug Finder.
Если при запуске анализ Программы автоматического доказательства Кода, результаты содержат оранжевую проверку 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:
В Редакторе Simulink откройте Model Explorer от вкладки Modeling.
Переменные базового рабочего пространства содержат переменную SIGNALBUS. Выберите эту переменную и откройте редактор шины, чтобы отредактировать эту переменную. Задайте минимальное и максимальное значение для переменной.
Сохраните объект шины в MAT-файле. Можно перезаписать файл dLctData.mat или создайте файл.
Можно также ограничить обратную связь от блока C Caller несколькими способами. Например, можно насыщать сигнал обратной связи:
Добавьте блок Saturation сразу, прежде чем сигнал обратной связи будет введен с блоком C Caller.
На вкладке Signal Attributes задайте минимальное и максимальное значение для блока Saturation выход.
Обратите внимание на то, что определение нижнего и верхнего предела вкладки Main блока Saturation не достаточно, чтобы ограничить сигнал для анализа Polyspace. Анализ использует диапазоны проекта, указанные на вкладке Signal Attributes.
Повторно выполните анализ. Регистрация Overflow нового набора результатов является зеленой.
Этот пример использует функцию, вызванную от нескольких блоков Вызывающей стороны C в модели. Функция просто возвращает продукт своих двух аргументов.
Пример запускает анализ Программы автоматического доказательства Кода и показывает, как определить контекст вызова функции, начинающий с результатов Программы автоматического доказательства Кода. Как правило, в анализе Bug Finder, вы не должны различать различные контексты вызова.
Откройте модель multiCCallerBlocks для рабочего анализа Polyspace.
openExample('polyspace_bf/OpenModelForAnalyzingAllCustomCodeExample'); open_system('multiCCallerBlocks');
Модель содержит два блока Вызывающей стороны C, вызывая тот же функциональный times_n. Входные параметры с одним блоком C Caller прибывают из двух блоков Inport, которые имеют неограниченный вход. Входные параметры с другим блоком C Caller прибывают из блока Constant и блока Inport, которому ограничил вход блок Saturation.
Видеть проект располагается для блока C Caller, который ограничил входные параметры:
Дважды кликните блок Constant или блок Saturation.
На вкладке 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 функция вызвана от двух контекстов, оранжевый цвет комбинирует оба контекста и может указать на две возможных ситуации:
Переполнение происходит в обоих контекстах вызова.
Переполнение, как доказывают, не происходит в одном контексте (зеленая проверка) и может произойти в другом контексте (оранжевая проверка).
Чтобы определить, какой контекст вызова приводит к переполнению:
Смотрите все вызывающие стороны times_n.
Выберите оранжевую проверку Overflow. На панели Result Details щелкнуть
. Панель Call Hierarchy показывает вызывающим сторонам times_n.
На панели Call Hierarchy вы рассматриваете две функции обертки как вызывающие стороны. Каждая функция обертки представляет блок C Caller в модели.
Выберите одну из функций обертки, чтобы открыть исходный код для customcode_wrappers.c.
На панели 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 функция:
В вашей модели, на вкладке Polyspace, выбирают Settings> Project Settings.
В качестве альтернативы в пользовательском интерфейсе Polyspace, выберите Project Browser. Откройте настройку проекта, созданного для анализа.
На Code Prover Verification> узел Precision, выберите custom для опции Sensitivity context. В поле Procedure кликните
и введите times_n.
См. также Sensitivity context (-context-sensitivity) (Polyspace Code Prover).
Повторно выполните анализ из модели и вновь откройте результаты. Выберите оранжевую проверку Overflow.
Панель Result Details показывает контексты вызова отдельно. Вы видите, что переполнение происходит только для вызова с неограниченными входными параметрами (строка с оранжевым текстом) и не происходит для другого вызова (строка с зеленым текстом).
Кликните по строке с оранжевым текстом, чтобы непосредственно перейти к функции обертки, ведущей к оранжевой проверке. От функции обертки можно перейти с блоком C Caller с неограниченными входными параметрами.
