Exponenta Banner

Запустите Polyspace Code Prover на коде C/C++

Polyspace® Code Prover™ является звуковым инструментом статического анализа, который доказывает отсутствие переполнения, разделитесь на нуль, за пределы доступ к массиву и определенные другие ошибки времени выполнения в исходном коде C++ и C. Анализ Программы автоматического доказательства Кода приводит к результатам, не требуя выполнения программы, отладки кода или тестов. Программа автоматического доказательства кода использует семантический анализ и абстрактную интерпретацию на основе формальных методов, чтобы определить поток управления и поток данных в коде. Можно использовать Программу автоматического доказательства Кода на рукописном коде, сгенерированном коде или комбинации двух. В результатах анализа на каждую операцию наносят цветную маркировку, чтобы указать, свободно ли это от ошибок времени выполнения, которые, как доказывают, перестали работать, недостижимый, или бездоказательный.

Можно запустить Программу автоматического доказательства Кода на коде C/C++ от пользовательского интерфейса Polyspace в поддерживаемой среде разработки (IDE), такой как скрипты использования или Eclipse™. См.:

Чтобы выполнить шаги в этом примере, скопируйте файлы example.c и include.h от polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources до другой папки. Здесь, polyspaceroot является папкой установки Polyspace, например, C:\Program Files\Polyspace\R2019a.

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

Открытый пользовательский интерфейс Polyspace

Дважды кликните исполняемый файл polyspace в polyspaceroot\polyspace\bin. Здесь, polyspaceroot является папкой установки Polyspace, например, C:\Program Files\Polyspace\R2019a.

Если вы настраиваете ярлык Polyspace на вашем рабочем столе или меню Start в Windows®, дважды кликаете ярлык.

Добавьте исходные файлы

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

Слева от панели Start Page нажмите Start a new project. Также выберите File> New Project.

После того, как вы обеспечиваете название проекта на следующих экранах:

  • Добавьте свою исходную папку.

    В этом примере добавьте путь к папке, в которой вы сохранили файл example.c. Нажмите Next.

  • Добавьте ваш включать папку.

    В этом примере добавьте путь к папке, в которой вы сохранили файл include.h. Эта папка может совпасть с предыдущей папкой. Нажмите Finish.

После того, как вы закончите добавлять свой источник и включать папки, вы видите новый проект на панели Project Browser. Ваши исходные папки копируются в первый модуль в проекте. Можно щелкнуть правой кнопкой по проекту добавить больше папок позже. Если вы добавляете папки позже, необходимо явным образом скопировать их в модуль.

Сконфигурируйте и запущенный Polyspace

Можно изменить опции по умолчанию, сопоставленные с анализом Polyspace.

Кликните по узлу Configuration в своем модуле проекта. На панели Configuration измените опции по мере необходимости. Например, на узле Coding Rules & Code Metrics, выберите Check MISRA C:2004.

Для получения дополнительной информации смотрите подсказку на каждой опции. Щелкните по ссылке More help для контекстно-зависимой справки на опциях.

Чтобы запустить верификацию, нажмите Run Code Prover на главной панели инструментов. Если кнопка указывает на Средство поиска Ошибки, кликните по стрелке около кнопки, чтобы переключиться на Программу автоматического доказательства Кода.

Следуйте за прогрессом верификации на окне Output Summary. После верификации результаты открываются автоматически.

Дополнительная информация

См.:

Запустите Polyspace на командной строке Linux или Windows

Можно запустить Программу автоматического доказательства Кода от Windows или командной строки Linux® с пакетом (.bat) файлы или интерпретатор (.sh) скрипты.

Используйте команду polyspace-code-prover, чтобы запустить верификацию.

Чтобы сохранить ввод полного пути в команду, добавьте путь polyspaceroot\polyspace\bin в переменную окружения Path на вашей операционной системе. Здесь, polyspaceroot является папкой установки Polyspace, например, C:\Program Files\Polyspace\R2019a.

Перейдите к папке, где вы сохранили файлы (использующий cd). Введите следующее:

polyspace-code-prover -sources example.c -I . -results-dir . -main-generator
Здесь, . указывает на текущую папку. Используемые опции:

  • -sources: Задайте разделенные от запятой исходные файлы.

  • i: Задайте путь, чтобы включать папку. Используйте флаг -I каждый раз, когда вы хотите добавить, что отдельное включает папку.

  • -results-dir: Задайте путь, где результаты Polyspace Code Prover будут сохранены.

  • Verify module or library (-main-generator): Укажите, что функция main должна быть сгенерирована если не найденный в исходных файлах

После верификации результаты сохранены в файле ps_results.pscp. Можно открыть этот файл от пользовательского интерфейса Polyspace. Например, введите следующее:

polyspace ps_results.pscp

Вместо того, чтобы задать разделенные от запятой источники непосредственно на командной строке, можно перечислить источники в текстовом файле (один файл на строку). Используйте опцию -sources-list-file, чтобы задать этот текстовый файл.

Дополнительная информация

См.:

Запустите Polyspace в Eclipse

Если вы разрабатываете код в Eclipse или основанном на Eclipse IDE, можно запустить Программу автоматического доказательства Кода непосредственно от IDE.

После установки плагина Eclipse можно запустить Polyspace непосредственно на файлах в проектах Eclipse.

В панели Project Explorer в Eclipse выберите свой проект. Чтобы использовать Программу автоматического доказательства Кода для анализа, выберите Polyspace> Code Prover. Чтобы запустить анализ, выберите Polyspace> Run (Ctrl + R).

После анализа результаты открываются автоматически в Eclipse.

Дополнительная информация

Смотрите запущенный анализ Polyspace в Eclipse.

Запустите Polyspace в MATLAB

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

Чтобы запустить анализ, используйте объект polyspace.Project. Объект имеет два свойства:

  • Configuration: Задайте аналитические опции, такие как источники, включает, компилятор и папка результатов с помощью этого свойства.

  • Results: После анализа считайте результаты анализа в таблицу MATLAB с помощью этого свойства.

Чтобы запустить анализ, используйте метод run этого объекта.

Чтобы запустить Polyspace на файле в качестве примера example.c в polyspaceroot\polyspace\examples\cxx\Code_Prover_Examples\sources, введите следующее в подсказке команды MATLAB.

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
cpSummary = proj.Results.getSummary('runtime');
cpResults = proj.Results.getResults('readable');

После верификации результаты сохранены в файле ps_results.pscp. Можно открыть этот файл от пользовательского интерфейса Polyspace. Например, введите следующее:

resultsFile = fullfile(proj.Configuration.ResultsDir,'ps_results.pscp');
polyspaceCodeProver(resultsFile)

Дополнительная информация

См.:

Похожие темы

Документация Polyspace Code Prover
Поддержка