exponenta event banner

polyspaceConfigure

Создание проекта Polyspace из системы сборки в командной строке MATLAB

Описание

пример

polyspaceConfigure buildCommand отслеживает систему сборки и создает проект Polyspace ® с информацией, собранной из системы сборки. Анализ проекта Polyspace можно выполнить только в интерфейсе пользователя настольных продуктов Polyspace.

пример

polyspaceConfigure -option value buildCommand отслеживает вашу систему сборки и использует -option value для изменения операции по умолчанию polyspaceConfigure. Укажите модификаторы перед buildCommand, в противном случае они рассматриваются как опции в самой команде build.

Примечание

Перед запуском Polyspace из MATLAB ® необходимо связать установки Polyspace и MATLAB. См. раздел Интеграция полиспейса с MATLAB и Simulink.

Примеры

свернуть все

В этом примере показано, как создать проект Polyspace при использовании команды make targetName buildOptions для создания исходного кода. В примере создается проект Polyspace, который можно открыть только в интерфейсе пользователя настольных продуктов Polyspace.

Создайте проект Polyspace, указав уникальное имя проекта. Используйте -B или -W makefileName вариант с make чтобы все предварительные цели в makefile были переделаны.

polyspaceConfigure  -prog myProject ...
          make -B targetName buildOptions

Откройте проект «Полиспейс» в Диспетчере проектов.

polyspaceBugFinder('myProject.psprj')

В этом примере показано, как создавать различные проекты Polyspace из одной и той же трассы системы сборки. Можно указать исходные файлы для каждого проекта. В примере создается проект Polyspace, который можно открыть только в интерфейсе пользователя настольных продуктов Polyspace.

Трассировка системы построения без создания проекта Polyspace путем указания параметра -no-project. Чтобы убедиться, что все предварительные цели в вашем makefile переделаны, используйте соответствующие make параметр команды построения, например, -B.

polyspaceConfigure -no-project make -B;

polyspace-configure сохраняет информацию кэша и трассировку построения в местоположениях по умолчанию в текущей папке. Чтобы сохранить информацию кэша и трассировку построения в другом расположении, укажите параметры -cache-path и -build-trace.

Создайте проекты Polyspace, используя информацию трассировки построения из предыдущего шага. Укажите имя проекта и используйте -include-sources или -exclude-sources выбор файлов для включения в каждый проект.

polyspaceConfigure -no-build -prog myProject ...
-include-sources "glob_pattern";

glob_pattern - шаблон «глобус», соответствующий папкам или файлам, фильтруемым в проекте или из него. Чтобы гарантировать, что оболочка не разворачивает шаблоны глобуса, которые вы передаете polysapce-configure, заключите их в двойные кавычки. Дополнительные сведения о поддерживаемом синтаксисе для шаблонов glob см. в разделе Синтаксис выбора исходных файлов для настройки polyspace.

Если указаны параметры -build-trace и -cache-path на предыдущем шаге укажите их еще раз.

Удалите файл трассировки и папку кэша.

rmdir('polyspace_configure_cache', 's');
delete polyspace_configure_built_trace;
 
Если использовались параметры -build-trace и -cache-pathиспользуйте пути и имена файлов из этих параметров.

В этом примере показано, как выполнять анализ Polyspace при использовании команды построения, такой как make targetName buildOptions для создания исходного кода. В этом примере используется polyspaceConfigure для отслеживания системы сборки, но не для создания проекта Polyspace. Вместо этого создается файл параметров, который можно использовать для выполнения анализа Polyspace из командной строки.

Создание файла параметров Polyspace, определяющего -output-options-file команда. Используйте -B или -W makefileName вариант с make чтобы все предварительные цели в makefile были переделаны.

polyspaceConfigure -output-options-file ... 
         myOptions make -B targetName buildOptions

Используйте созданный файл параметров для выполнения анализа Polyspace в командной строке:

polyspaceBugFinder -options-file myOptions

Входные аргументы

свернуть все

Команда Build указана точно так же, как используется для построения исходного кода.

Пример: make -B, make -W makefileName

Основные параметры

ВыборАргументОписание
-progНазвание проекта

Имя проекта, отображаемое в интерфейсе пользователя Polyspace. Значение по умолчанию: polyspace.

Если параметр не используется -output-project, -prog аргумент также задает имя проекта.

Пример: -prog myProject создает проект с именем myProject в интерфейсе пользователя. Если параметр не используется -output-project, имя проекта также myProject.psrprj.

-authorИмя автора

Имя автора проекта.

Пример: -author jsmith

-output-projectПуть

Имя файла проекта и расположение для сохранения проекта. По умолчанию используется файл polyspace.psprj в текущей папке.

Пример: -output-project ../myProjects/project1 создает проект project1.psprj в папке с относительным путем ../myProjects/.

-output-options-fileИмя файла

Опция для создания файла опций анализа Polyspace. Используйте этот файл для анализа командной строки с помощью одной из следующих команд:

  • polyspace-bug-finder

  • polyspace-code-prover

  • polyspace-bug-finder-server

  • polyspace-code-prover-server

  • polyspace-bug-finder-access

-allow-build-errorНичего

Возможность создания проекта Polyspace даже при возникновении ошибки в процессе построения.

При возникновении ошибки в журнале трассировки построения отображается следующее сообщение:

polyspace-configure (polyspaceConfigure) 
   ERROR: build command 
   command_name fail [status=status_value]
command_name является именем команды построения, которое используется и status_value ненулевое состояние выхода или уровень ошибки, который указывает, какая ошибка произошла в процессе построения.

Этот параметр игнорируется при использовании -compilation-database.

-allow-overwriteНичего

Возможность перезаписи проекта с тем же именем, если он существует.

По умолчанию polyspace-configure (polyspaceConfigure) выдает ошибку, если проект с таким именем уже существует в папке вывода. Этот параметр используется для перезаписи проекта.

-no-console-output

-silent (по умолчанию)

-verbose

Ничего

Параметр для подавления или отображения дополнительных сообщений при выполнении polyspace-configure (polyspaceConfigure).

  • -no-console-output - Подавление всех выходов, включая ошибки и предупреждения.

  • -silent (по умолчанию) - отображение только ошибок и предупреждений.

  • -verbose - Показать все сообщения.

При указании нескольких из этих параметров применяется наиболее подробный вариант.

Эти опции игнорируются, если они используются в сочетании с -easy-debug.

-helpНичего

Опция для отображения полного списка polyspace-configure (polyspaceConfigure) команды

-debugНичего

Возможность хранения отладочной информации для использования в службе технической поддержки MathWorks ®.

Этот параметр заменен параметром -easy-debug.

-easy-debugПуть

Возможность хранения отладочной информации для использования в службе технической поддержки MathWorks.

После polyspace-configure (polyspaceConfigure) run, предоставленный путь содержит zipped-файл, заканчивающийся на pscfg-output.zip. Если при выполнении не удается создать полный файл проекта или параметров Polyspace, отправьте этот архивированный файл в службу технической поддержки MathWorks для дальнейшей отладки. Архивированный файл не содержит исходных файлов, отслеживаемых в сборке. См. также Ошибки при создании проекта из Build Systems.

Параметры создания нескольких модулей

Эти параметры несовместимы с -compilation-database.

ВыборАргументОписание
-moduleНичего

Возможность создания отдельного файла параметров для каждого двоичного файла, созданного в системе построения.

Можно создавать отдельные файлы параметров только для различных двоичных файлов. Невозможно создать несколько модулей в проекте Polyspace (для работы в пользовательском интерфейсе Polyspace).

Используйте этот параметр только для систем сборки, использующих компиляторы GNU ® и Visual C++ ®.

См. также раздел Модулирование анализа полиспейса с помощью команды построения.

-output-options-pathИмя пути

Расположение, в котором сохраняются созданные файлы опций. Используйте эту опцию вместе с опцией -module.

Файлы параметров называются по имени двоичных файлов, созданных в системе построения.

Дополнительные параметры

ВыборАргументОписание
-compilation-databaseПуть и имя файла

Местоположение и имя файла базы данных компиляции JSON (JSON CDB). Этот файл создается из системы построения, например, с помощью флага -DCMAKE_EXPORT_COMPILE_COMMANDS=1 с cmake. Файл содержит вызовы компилятора для всех единиц перевода в проектах. Дополнительные сведения см. в разделе База данных компиляции JSON. polyspace-configure использует содержимое этого файла для получения информации о системе сборки. Извлеченные пути компилятора в JSON CDB должны быть доступны из пути, по которому выполняется polyspace-configure.

При использовании этого параметра команда построения не указывается.

Системы сборки и компиляторы поддерживают создание JSON CDB:

  • CMake

  • Bazel

  • Лязг

  • Ниндзя

  • Qbs

  • WAF

Этот параметр несовместим с -no-project и с опциями для создания нескольких модулей.

Параметры управления кэшем, -allow-build-error, и -no-build игнорируются при использовании этого параметра.

-compiler-configПуть и имя файла

Расположение и имя файла конфигурации компилятора.

Файл должен иметь определенный формат. Для получения инструкций см. существующие файлы конфигурации в разделе polyspaceroot\polyspace\configure\compiler_configuration\. Сведения о содержимом файла см. в разделе Компилятор, не поддерживаемый для создания проектов из Build Systems.

Пример: -compiler-configuration myCompiler.xml

-no-projectНичего

Возможность трассировки системы сборки без создания проекта Polyspace и сохранения информации трассировки сборки.

Используйте этот параметр, чтобы сохранить информацию трассировки построения для более позднего запуска polyspace-configure (polyspaceConfigure) с -no-build вариант.

Этот параметр несовместим с -compilation-database.

-no-buildНичего

Возможность создания проекта Polyspace с использованием ранее сохраненной информации трассировки построения.

Чтобы использовать этот параметр, необходимо сохранить данные трассировки построения из более раннего запуска polyspace-configure (polyspaceConfigure) с -no-project вариант.

При использовании этого параметра не требуется указывать buildCommand аргумент.

Этот параметр игнорируется при использовании -compilation-database.

-no-sourcesНичего

Параметр для создания файла параметров Polyspace, не содержащего спецификации исходного файла.

Используйте этот параметр, если предполагается указать исходные файлы другими способами. Например, эту опцию можно использовать в следующих случаях:

  • Запуск Polyspace для кода, специфичного для AUTOSAR.

    Вы хотите создать файл параметров, который отслеживает вашу команду build для параметров компилятора:

    -output-options-file options.txt -no-sources
    Позже этот файл опций добавляется при извлечении имен исходных файлов из спецификаций ARXML и выполнении последующего анализа программы проверки кода с помощью polyspace-autosar(Доказательство кода Polyspace)
    -extra-options-file options.txt

    См. также раздел Запуск Polyspace по коду AUTOSAR с помощью команды построения (средство проверки кода Polyspace).

  • Запуск Polyspace в Eclipse™.

    Исходные файлы уже указаны в проекте Eclipse. При выполнении анализа Polyspace необходимо указать файл опций, содержащий только опции компиляции.

-extra-project-optionsОпции для последующего анализа Polyspace. Например, "-stubbed-pointers-are-unsafe".

Опции, используемые для последующего анализа Polyspace.

После создания проекта Polyspace можно изменить некоторые параметры по умолчанию в проекте. Кроме того, эти параметры можно передать при трассировке команды построения. Флаг -extra-project-options позволяет передавать дополнительные параметры.

Укажите несколько параметров в списке, разделенном пробелами, например "-allow-negative-operand-in-shift -stubbed-pointers-are-unsafe".

Предположим, что необходимо задать опцию -stubbed-pointers-are-unsafe для каждого созданного проекта Polyspace. Вместо открытия каждого проекта и установки параметра можно использовать этот флаг при создании проекта Polyspace:

-extra-project-options "-stubbed-pointers-are-unsafe"

Список доступных опций см. в разделе:

Если создается файл параметров вместо проекта Polyspace из команды build, не используйте этот флаг.

-tmp-pathПутьРасположение папки, в которой хранятся временные файлы.
-build-traceПуть и имя файла

Расположение и имя файла, в котором хранится информация о построении. Значение по умолчанию: ./polyspace_configure_build_trace.log.

Пример: -build-trace ../build_info/trace.log

-include-sources

-exclude-sources

Шаблон Glob

Параметр для указания исходных файлов polyspace-configure (polyspaceConfigure) включает в созданный проект или исключает из него. Можно объединить оба варианта.

Исходный файл включается, если путь к файлу соответствует шаблону gob, переданному -include-sources.

Исходный файл исключается, если путь к файлу соответствует шаблону glob, переданному -exclude-sources.

-print-included-sources

-print-excluded-sources

Ничего

Параметр для печати списка исходных файлов, polyspace-configure (polyspaceConfigure) включает в созданный проект или исключает из него. Можно объединить оба варианта. В выходных данных отображается полный путь к каждому файлу в отдельной строке.

Используйте этот параметр для устранения неполадок, связанных с переданными шаблонами glob -include-sources или -exclude-sources. Можно просмотреть, какие файлы соответствуют шаблону, переданному -include-sources или -exclude-sources.

-compiler-cache-pathПуть к папке

Укажите путь к папке, где polyspace-configure ищет или сохраняет файлы кэша компилятора. Если папка не существует, polyspace-configure создает его.

По умолчанию Polyspace ищет и хранит кэши компилятора в следующих папках:

  • Windows ®

    %appdata%\Mathworks\R20xxY\Polyspace

  • Linux ®

    ~/.matlab/R20xxY/Polyspace

  • Mac

    ~/Library/Application Support/MathWorks/MATLAB/R20xxY/Polyspace

R20xxY является версией выпуска продукта Polyspace, например R2020b.

-no-compiler-cacheНичего

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

По умолчанию при первом запуске polyspace-configure при определенной конфигурации компилятора Polyspace запрашивает у компилятора размер фундаментальных типов, определения макросов компилятора и другую информацию конфигурации компилятора, затем кэширует эту информацию. Polyspace повторно использует кэшированную информацию в последующих запусках polyspace-configure для сборок, использующих одну и ту же конфигурацию компилятора.

-reset-compiler-cache-entryНичегоИспользуйте этот параметр, чтобы запросить у компилятора текущую конфигурацию и обновить запись в файле кэша, соответствующую этой конфигурации. Другие записи конфигурации компилятора в кэше не обновляются.
-clear-compiler-cacheНичего

Этот параметр используется для удаления всех конфигураций компилятора, хранящихся в файле кэша.

Если также указана команда построения или -compilation-database, polyspace-configure вычисляет и кэширует конфигурационную информацию компилятора текущего запуска, за исключением тех случаев, когда указано -no-project или -no-compiler-cache.

-import-macro-definitions

none

from-whitelist

from-source-tokens

Используйте этот параметр для указания способа polyspace-configure запрашивает у компилятора определения макросов.

Можно указать:

  • none - Polyspace не запрашивает у компилятора определения макросов. Необходимо вручную предоставить определения макросов.

  • from-whitelist - Polyspace использует внутренний белый список для запроса в компиляторе определений макросов.

    При использовании параметра Polyspace по умолчанию использует белый список -compilation-database.

  • from-source-tokens (по умолчанию, за исключением использования -compilation-database ) - Polyspace использует каждый токен без ключевого слова в исходном коде для запроса в компиляторе определений макросов.

-options-for-sources-delimiterОдин символ

Укажите разделитель опций, который будет использоваться при связывании нескольких опций анализа с одним исходным файлом с помощью -options-for-sources вариант. Как правило, -options-for-sources в качестве разделителя используется точка с запятой.

См. также -options-for-sources.

Параметры управления кэшем

Эти параметры в первую очередь полезны для отладки. Используйте опции, если polyspace-configure (polyspaceConfigure) ошибка, и служба технической поддержки MathWorks просит вас использовать этот параметр и предоставить кэшированные файлы. Начиная с R2020a, опция -easy-debug предоставляет более простой способ предоставления отладочной информации. Обратитесь в службу технической поддержки по вопросам работы Polyspace.

Эти параметры игнорируются при использовании -compilation-database.

ВыборАргументОписание

-no-cache

-cache-sources (по умолчанию)

-cache-all-text

-cache-all-files

Ничего

Можно выполнить одно из следующих действий:

  • -no-cache: Не создавать кэш

  • -cache-sources: Кэшировать текстовые файлы, временно созданные во время построения, для последующего использования polyspace-configure (polyspaceConfigure).

  • -cache-all-text: Кэширование всех текстовых файлов, включая источники и заголовки.

  • -cache-all-files: Кэширование всех файлов, включая двоичные файлы.

Обычно временные файлы, созданные командой build, кэшируются для отладки проблем при трассировке команды.

-cache-pathПуть

Расположение папки, в которой хранится информация кэша.

При отслеживании построения Visual Studio (devenv.exe), если вы видите ошибку:

path is too long
попробуйте использовать более короткий путь для этого параметра, чтобы обойти ошибку.

Пример: -cache-path ../cache

-keep-cache

-no-keep-cache (по умолчанию)

Ничего

Возможность сохранения или очистки данных кэша после polyspace-configure (polyspaceConfigure) завершает выполнение.

Если polyspace-configure (polyspaceConfigure) не удалось, можно предоставить эту информацию кэша в службу технической поддержки для отладки.

Представлен в R2013b