Polyspace ® Code Prover™ - это инструмент звукового статического анализа, который доказывает отсутствие переполнения, деления на ноль, внеграничного доступа к массиву и некоторых других ошибок времени выполнения в исходном коде C и C++. Анализ проверки кода дает результаты, не требуя выполнения программы, инструментальных средств кода или тестовых примеров. Code Prover использует семантический анализ и абстрактную интерпретацию на основе формальных методов для определения потока управления и потока данных в коде. Средство проверки кода можно использовать для рукописного кода, сгенерированного кода или комбинации этих двух кодов. В результатах анализа каждая операция кодируется цветом, чтобы указать, свободна ли она от ошибок времени выполнения, доказана ли ее неудачность, недостижимость или недоказанность.
Программу Code Prover можно запустить для кода C/C + + из пользовательского интерфейса Polyspace в поддерживаемой среде разработки (IDE), такой как Eclipse™ или использование сценариев. См.:
Запуск Polyspace в интерфейсе пользователя
При первом использовании Polyspace может потребоваться начать работу с пользовательского интерфейса Polyspace. Можно получить справку от таких функций, как мастер настройки проекта, вспомогательная настройка и сводный журнал анализа.
Запуск Polyspace в командной строке Windows или Linux
После настройки проекта в интерфейсе пользователя Polyspace и выполнения нескольких пробных запусков можно экспортировать конфигурацию в сценарии, запускаемые автоматически или по запросу. Анализ Polyspace также можно выполнить непосредственно из командной строки операционной системы. Затем можно сохранить команды в пакетных файлах (Windows) или сценариях оболочки (Linux) для последующих запусков. При работе с продуктами Polyspace Server с помощью средств непрерывной интеграции, таких как Jenkins, можно повторно использовать сценарии из настольных продуктов Polyspace.
Запустить Polyspace в затмении
После ознакомления с запуском Polyspace из командной строки можно создать пункты меню в среде IDE, которые запускают сценарии и запускают анализ Polyspace одним щелчком мыши. В IDE на основе Eclipse и Eclipse можно установить подключаемый модуль Polyspace, который вообще не требует дополнительной установки. При запуске Polyspace из плагина Eclipse конфигурация анализа создается непосредственно из проекта Eclipse.
При установке MATLAB очень легко писать сценарии для выполнения анализа Polyspace. Вы получаете все преимущества создания сценариев в среде MATLAB, например, автоматическую справку по синтаксисам функций. После анализа можно создать собственную визуализацию результатов с помощью графики MATLAB и инструментов визуализации.
Чтобы выполнить действия, описанные в этом учебном пособии, скопируйте файлы |
Дважды щелкните значок polyspace исполняемый файл в polyspaceroot\polyspace\binpolyspacerootC:\Program Files\Polyspace\R2020a. См. также Папку установки.
При настройке ярлыка Polyspace на рабочем столе или в меню «Пуск» Windows ® дважды щелкните ярлык.
Для выполнения проверки необходимо создать новый проект Polyspace. Проект Polyspace указывает на источник и включает папки в файловой системе.
В левой части панели «Начальная страница» нажмите кнопку «Начать новый проект». Либо выберите «Файл» > «Новый проект».
После ввода имени проекта на следующих экранах:
Добавьте исходную папку.
В этом учебном пособии добавьте путь к папке, в которой был сохранен файл. example.c. Нажмите кнопку Далее.
Добавьте папку включения.
В этом учебном пособии добавьте путь к папке, в которой был сохранен файл. include.h. Эта папка может совпадать с предыдущей. Нажмите кнопку Готово (Finish).
После завершения добавления источника и добавления папок на панели «Диспетчер проектов» появится новый проект. Исходные папки копируются в первый модуль проекта. Чтобы добавить дополнительные папки позже, щелкните проект правой кнопкой мыши. При последующем добавлении папок их необходимо явно скопировать в модуль.
Можно изменить опции по умолчанию, связанные с анализом Polyspace.
Щелкните узел Конфигурация в модуле проекта. При необходимости измените параметры на панели Конфигурация (Configuration). Например, в узле Coding Rules & Code Metrics выберите Check MISRA C:2004.
Дополнительные сведения см. в подсказке по каждому параметру. Щелкните ссылку Дополнительная справка для контекстной справки по параметрам.
Чтобы начать проверку, нажмите кнопку Запустить программу проверки кода на верхней панели инструментов. Если кнопка указывает на поиск ошибок, щелкните стрелку рядом с кнопкой, чтобы переключиться на средство проверки кода.
Следите за ходом проверки в окне Вывод сводки (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.
Обратите внимание, что папка результатов очищается и повторно заполняется на каждом прогоне. Чтобы избежать случайного удаления файлов во время очистки, вместо использования существующей папки, содержащей другие файлы, укажите специальную папку для результатов Polyspace.
Verify module or library (-main-generator): Укажите, что main функция должна быть сгенерирована, если не найдена в исходных файлах
После проверки результаты сохраняются в файле. ps_results.pscp. Этот файл можно открыть в интерфейсе пользователя Polyspace. Например, введите следующее:
polyspace ps_results.pscp
Вместо указания разделенных запятыми источников непосредственно в командной строке можно перечислить источники в текстовом файле (по одному файлу на строку). Использовать опцию -sources-list-file для указания этого текстового файла.
См.:
При разработке кода в Eclipse или среде IDE на основе Eclipse можно запустить программу проверки кода непосредственно из среды IDE.
После установки плагина Eclipse можно запустить Polyspace непосредственно над файлами в проектах Eclipse.
На панели «Обозреватель проектов» в Eclipse выберите проект. Чтобы использовать средство проверки кода для анализа, выберите «Полиспейс» > «Средство проверки кода». Чтобы начать анализ, выберите Полиспейс (Polyspace) > Выполнить (Run) (Ctrl + R).
После анализа результаты автоматически открываются в Eclipse.
См. раздел Выполнение анализа пространства в проектах затмения.
Перед запуском Polyspace из MATLAB ® необходимо связать установки Polyspace и MATLAB. См. раздел Интеграция полиспейса с MATLAB и Simulink.
Для выполнения анализа используйте polyspace.Project объект. Объект имеет два свойства:
Configuration: Укажите параметры анализа, такие как источники, include, компилятор и папка результатов, используя это свойство.
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)
См.: