Polyspace® Code Prover™ является инструментом звукового статического анализа, который доказывает отсутствие переполнения, деления на нули, доступа к массиву вне границ и некоторых других ошибок времени выполнения в исходном коде C и C++. Анализ Code Prover дает результаты, не требуя выполнения программы, отладки кода или тестов. Code Prover использует семантический анализ и абстрактную интерпретацию, основанную на формальных методах, для определения потока управления и потока данных в коде. Можно использовать Code Prover на рукописном коде, сгенерированном коде или комбинации из двух. В результатах анализа каждая операция кодируется по цвету, чтобы указать, свободна ли она от ошибок времени выполнения, доказала свою неудачу, недоступность или недоказанность.
Можно запустить Code Prover на C/C + + коде из пользовательского интерфейса Polyspace в поддерживаемой среде разработки (IDE), такой как Eclipse™ или использование скриптов. См.:
Запуск Polyspace в пользовательском интерфейсе
Если вы впервые используете Polyspace, вы можете начать с пользовательского интерфейса Polyspace. Вы можете получить помощь от таких функций, как мастер настройки проекта, вспомогательное строение и журнал сводного анализа.
Запуск Polyspace в командной строке Windows или Linux
После настройки проекта в пользовательском интерфейсе Polyspace и завершения нескольких пробных запусков можно экспортировать строение в скрипты, которые запускаются автоматически или по требованию. Можно также запустить анализ Polyspace непосредственно из командной строки в операционной системе. Затем можно сохранить команды в пакетных файлах (Windows) или оболочечных скриптах (Linux) для последующих запусков. Если при запуске Серверные продукты Polyspace с помощью инструментов непрерывного интегрирования, таких как Jenkins, можно переиспользовать скрипты из десктопных решений Polyspace.
Как только вы знакомы с запуском Polyspace из командной строки, можно создать в своей среде IDE элементы меню, которые запускают ваши скрипты и запускают анализ Polyspace в одно нажатие кнопки. В Eclipse и основанных на Eclipse IDE, можно установить плагин Polyspace, который не требует никакой дополнительной настройки вообще. Когда вы запускаете Polyspace из плагина Eclipse, строение анализа создаётся непосредственно из вашего проекта Eclipse.
Если у вас есть установка MATLAB, особенно легко написать скрипты, чтобы запустить анализ Polyspace. Вы получаете все преимущества скриптирования в среде MATLAB, например, автоматическую справку по синтаксисам функций. После анализа можно создать собственную визуализацию результатов с помощью графики MATLAB и инструментов визуализации.
Чтобы следовать шагам в этом руководстве, скопируйте файлы |
Дважды кликните polyspace исполняемый файл в polyspaceroot\ polyspace\binpolyspacerootC:\Program Files\Polyspace\R2020a. См. также Папка установки.
Если вы настраиваете ярлык Polyspace на рабочем столе или в Start меню Windows®дважды кликните ярлык.
Чтобы запустить верификацию, необходимо создать новый проект Polyspace. Проект Polyspace указывает, на исходный код и включать папки в вашей файловой системе.
В левой части панели Start Page нажмите Start a new project. Также выберите File > New Project.
После того, как вы задаете имя проекта, на следующих экранах:
Добавьте исходную папку.
В этом руководстве добавьте путь к папке, в которой вы сохраняли файл example.c. Нажмите Next.
Добавьте папку include.
В этом руководстве добавьте путь к папке, в которой вы сохраняли файл include.h. Эта папка может совпадать с предыдущей. Нажмите Finish.
После завершения добавления исходного кода и включения папок на панели Project Browser отображается новый проект. Исходные папки копируются в первый модуль проекта. Можно щелкнуть правой кнопкой мыши проект, чтобы добавить больше папок позже. Если вы добавляете папки позже, необходимо явным образом скопировать их в модуль.
Можно изменить опции по умолчанию, связанные с анализом Polyspace.
Щелкните узел Configuration в модуле проекта. На панели Configuration измените опции по мере необходимости. Для образца на узле Coding Rules & Code Metrics выберите Check MISRA C:2004.
Для получения дополнительной информации см. всплывающую подсказку по каждой опции. Щелкните ссылку More help для контекстно-зависимой справки по опциям.
Чтобы начать верификацию, щелкните Run Code Prover на верхней панели инструментов. Если кнопка указывает Bug Finder, щелкните стреле рядом с кнопкой, чтобы переключиться на Code Prover.
Следите за прогрессом верификации в окне Output Summary. После верификации результаты открываются автоматически.
См.:
Можно запустить Code Prover из Windows или Linux® командная строка с пакетом (.bat) файлы или интерпретатор (.sh) скрипты.
Используйте polyspace-code-prover команда для запуска верификации.
Чтобы сохранить полный путь к команде, добавьте путь polyspaceroot\ polyspace\binPath окружение в операционной системе. Здесь, polyspacerootC:\Program Files\Polyspace\R2020a.
Перейдите в папку, в которой вы сохраняли файлы (используя cd). Введите следующее:
polyspace-code-prover -sources example.c -I . -results-dir . -main-generator
. указывает текущую папку. Используются следующие опции:
-sources: Укажите разделенные запятыми исходные файлы.
-I: Укажите путь для включения папки. Используйте -I флаг при каждом добавлении отдельной папки включения.
-results-dir: Укажите путь к папке, в которой будут сохранены результаты Polyspace Code Prover.
Обратите внимание, что папка результатов очищается и повторно заполняется при каждом запуске. Чтобы избежать случайного удаления файлов во время очистки, вместо использования существующей папки, содержащей другие файлы, укажите выделенную папку для результатов Polyspace.
Verify module or library (-main-generator): Задайте, что main функция должна быть сгенерирована, если не найдена в исходных файлах
После верификации результаты сохраняются в файле ps_results.pscp. Открыть этот файл можно из пользовательского интерфейса Polyspace. Для образца введите следующее:
polyspace ps_results.pscp
Вместо указания разделенных запятыми источников непосредственно в командной строке можно перечислить источники в текстовом файле (по одному файлу на линию). Используйте опцию -sources-list-file чтобы задать этот текстовый файл.
См.:
Если вы разрабатываете код в Eclipse или основанной на Eclipse среде IDE, можно запустить Code Prover непосредственно из среды IDE.
После установки плагина Eclipse можно запустить Polyspace непосредственно на файлах в проектах Eclipse.
На панели Project Explorer в Eclipse выберите свой проект. Чтобы использовать Code Prover для анализа, выберите Polyspace > Code Prover. Чтобы начать анализ, выберите Polyspace > Run (Ctrl + R).
После анализа результаты автоматически открываются в Eclipse.
Смотрите Запуск анализа Polyspace на проектах Eclipse.
Прежде чем запускать Polyspace из MATLAB®необходимо связать установки Polyspace и MATLAB. См. «Интеграция Polyspace с MATLAB и Simulink».
Чтобы запустить анализ, используйте polyspace.Project объект. Объект имеет два свойства:
Configuration: Задайте опции анализа, такие как источники, включения, компилятор и папка результатов, используя это свойство.
Results: После анализа прочтите результаты анализа в таблицу MATLAB с помощью этого свойства.
Чтобы запустить анализ, используйте run метод данного объекта.
Чтобы запустить Polyspace для файла с примером example.c в polyspaceroot\ polyspace\examples\cxx\Code _ Prover _ Examples\sources
proj = polyspace.Project % Configure analysis proj.Configuration.Sources = {fullfile(polyspaceroot, 'polyspace', 'examples',... 'cxx', 'Code_Prover_Example', 'sources', 'example.c')}; proj.Configuration.EnvironmentSettings.IncludeFolders = {fullfile(polyspaceroot,... 'polyspace', 'examples', 'cxx', 'Code_Prover_Example', 'sources')} proj.Configuration.TargetCompiler.Compiler = 'gnu4.9'; proj.Configuration.ResultsDir = fullfile(pwd,'results'); proj.Configuration.CodeProverVerification.MainGenerator = true; % Run analysis cpStatus = proj.run('codeProver'); % Read results resObj = proj.Results; cpSummary = getSummary(resObj, 'runtime'); cpResults = getResults(resObj, 'readable');
После верификации результаты сохраняются в файле ps_results.pscp. Открыть этот файл можно из пользовательского интерфейса Polyspace. Для образца введите следующее:
resultsFile = fullfile(proj.Configuration.ResultsDir,'ps_results.pscp');
polyspaceCodeProver(resultsFile)
См.: