После генерации кода C/C++ из кода MATLAB® можно независимо проверять сгенерированный код на:
Ошибки или дефекты и кодирующий нарушения правила: Используйте Polyspace® Bug Finder™.
Ошибки времени выполнения: Используйте Polyspace Code Prover™.
Генерируете ли вы код в приложении MATLAB Coder™ или используете codegen, можно следовать за тем же рабочим процессом для проверки сгенерированного кода.
Этот пример использует пример MATLAB Coder averaging_filter в polyspaceroot\help\toolbox\codeprover\examples\matlab_coderpolyspacrootC:\Program Files\Polyspace\R2021a. Пример показывает анализ Программы автоматического доказательства Кода. Можно следовать за подобным рабочим процессом для Bug Finder.
Запускать этот пример:
У вас должна быть лицензия Embedded Coder®. Приложение MATLAB Coder не показывает варианты для рабочего Polyspace, если у вас нет лицензии Embedded Coder.
Необходимо быть знакомы с тем, как открыть и использовать приложение MATLAB Coder или codegen команда. В противном случае смотрите, что MATLAB Coder Начинает.
Необходимо соединить Polyspace и установки MATLAB. Смотрите Интегрируют Polyspace с MATLAB и Simulink.
В приложении MATLAB Coder сгенерируйте код из файла averaging_filter.m и анализируйте сгенерированный код.
Сгенерируйте код.
От функции точки входа в файле сгенерируйте автономный код C/C++ (статическая библиотека, динамически подключаемая библиотека или исполняемая программа) в приложении MATLAB Coder. Функция имеет вход того. Явным образом задайте тип данных для входа, например, 1 X 100 векторов из типа double, или обеспечьте файл для получения типов данных.
Анализируйте сгенерированный код.
После генерации кода, открытой панель Polyspace и, нажимают Run.
Если анализ завершается без ошибок, результаты Polyspace, открытые автоматически. Если вы закрываете результаты, можно вновь открыть их от итоговой страницы в приложении под разделом Generated Output. Результаты хранятся в подпапке results_averaging_filter в папке, содержащей файл MATLAB.
Написать сценарий предыдущего рабочего процесса, запуска:
% Generate code matlabFileName = fullfile(polyspaceroot, 'help',... 'toolbox','codeprover','examples','matlab_coder','averaging_filter.m'); codegenFolder = fullfile(pwd, 'codegenFolder'); codegen(matlabFileName, '-config:lib', '-c', '-args', ... {zeros(1,100,'double')}, '-d', codegenFolder); % Configure Polyspace analysis opts = pslinkoptions('ec'); opts.ResultDir = [tempdir 'results']; opts.OpenProjectManager = 1; % Run Polyspace [polyspaceFolder, resultsFolder] = pslinkrun('-codegenfolder', codegenFolder, opts);
После анализа панель Results List показывает список проверок на этапе выполнения. Для объяснения результирующих цветов смотрите Цвета Результата и Исходного кода Программы автоматического доказательства Кода (Polyspace Code Prover).
Рассмотрите результаты и определите, устранить ли проблемы.
Отфильтруйте результаты, которые вы не хотите рассматривать. Например, вы не можете хотеть видеть зеленые проверки.
См. обзор результатов на панели Dashboard. Кликните по оранжевому разделу круговой диаграммы, чтобы отфильтровать список результатов на панели Results List к одной оранжевой проверке. Кликните по этой оранжевой проверке Overflow и см. исходный код для операции, которая может переполниться.
Если результаты сгруппированы семейством, чтобы видеть, что плоский список, на панели Results List, от
выпадающего списка, выбирает None.
Найдите первопричину каждой ошибки времени выполнения.
На панели Source использование щелкает правой кнопкой по инструментам навигации и подсказкам, чтобы идентифицировать первопричину проверки. В этом случае вы видите что + операция переполняется, потому что Polyspace делает предположение о входном массиве к функции. Предположение - то, что элементы массива могут иметь любое значение, позволенное их double тип данных. Подсказка на линии buffer[0] = x[i] показывает принятую область значений.
С лицензией Embedded Coder можно легко проследить от сгенерированного кода C до оригинального кода MATLAB. Смотрите В интерактивном режиме Трассировку Между кодом MATLAB и Сгенерированным Кодом C/C++ (Embedded Coder).
Можно проверять сгенерированный код на определенную область значений входных параметров. Спецификация области значений помогает сузить предположение по умолчанию, что входные параметры являются полным диапазоном.
Указывать диапазон для входных параметров:
Откройте аналитическую настройку.
В пользовательском интерфейсе Polyspace переключитесь на проект Polyspace, созданный для анализа. Выберите Window> Reset Layout> Project Setup. На панели Project Browser кликните по настройке проекта.
Укажите диапазон проекта для входных параметров.
В панели Configuration, на узле Inputs & Stubbing, настраивает ваши ограничения. Нажмите Edit beside Constraint setup. Ограничьте область значений первого входа к [-100.. 100].
Можно перезаписать ограничительный шаблон по умолчанию или сохранить ограничения в другом месте. Для получения информации о столбцах в этом окне смотрите Внешние Ограничения для Анализа Polyspace.
Повторно выполните анализ из приложения Кодера (или в командной строке MATLAB) и смотрите результаты.
На панели Dashboard вы больше не видите предыдущее оранжевое переполнение.
