Чтобы сконфигурировать анализ Polyspace®, можно снова использовать параметры компиляции в команде сборки, такие как make. Во-первых, вы прослеживаете свою команду сборки с polyspace-configure (или polyspaceConfigure в MATLAB®) и создаете файл опций Polyspace. Вы позже задаете этот файл опций для последующего анализа Polyspace.
Если ваша команда сборки создает несколько двоичных файлов группами polyspace-configure по умолчанию исходные файлы для всех двоичных файлов в один файл опций Polyspace. Если двоичные файлы, которые используют те же исходные файлы или функции, скомпилированы с различными вариантами, вы теряете это различие в последующем анализе Polyspace. Присутствие той же функции многократно может вести, чтобы соединять ошибки во время анализа Polyspace и иногда к неправильным результатам.
Эта тема показывает, как создать отдельный файл опций Polyspace для каждого двоичного файла, созданного в вашем make-файле. Предположим, что make-файл создает четыре двоичных файла: два исполняемых файла (предназначаются для cmd1 и cmd2), и две разделяемых библиотеки (предназначаются для liba и libb). Можно создать отдельный файл опций Polyspace для каждого из этих двоичных файлов.
Чтобы попробовать этот пример, используйте файлы в |
Осмотрите make-файл. Make-файл создает четыре двоичных файла:
CC := gcc LD := ld LIBA_SOURCES := $(wildcard src/liba/*.c) LIBB_SOURCES := $(wildcard src/libb/*.c) CMD1_SOURCES := $(wildcard src/cmd1/*.c) CMD2_SOURCES := $(wildcard src/cmd2/*.c) LIBA_OBJ := $(notdir $(LIBA_SOURCES:.c=.o)) LIBB_OBJ := $(notdir $(LIBB_SOURCES:.c=.o)) CMD1_OBJ := $(notdir $(CMD1_SOURCES:.c=.o)) CMD2_OBJ := $(notdir $(CMD2_SOURCES:.c=.o)) LIBB_SOBJ := libb.so LIBA_SOBJ := liba.so all: cmd1 cmd2 cmd1: liba libb $(CC) -o $@ $(CMD1_SOURCES) $(LIBA_SOBJ) $(LIBB_SOBJ) cmd2: libb $(CC) -c $(CMD2_SOURCES) $(LD) -o $@ $(CMD2_OBJ) $(LIBB_SOBJ) liba: libb $(CC) -fPIC -c $(LIBA_SOURCES) $(CC) -shared -o $(LIBA_SOBJ) $(LIBA_OBJ) libb: $(CC) -fPIC -c $(LIBB_SOURCES) $(CC) -shared -o $(LIBB_SOBJ) $(LIBB_OBJ) .PHONY: clean clean: rm *.o |
Созданным двоичным файлам показали зависимости в этой фигуре. Например, создание объекта cmd1.o зависит от всех файлов .c в папке cmd1 и общих объектах liba.so и libb.so.
Создайте свой исходный код при помощи make-файла. Используйте флаг -B, чтобы гарантировать полную сборку.
make -B |
Убедитесь, что сборка выполнение до завершения.
Проследите команду сборки при помощи polyspace-configure. Используйте опцию -output-options-file, чтобы создать файл опций Polyspace psoptions из команды сборки.
polyspace-configure -output-options-file psoptions make -B |
Запустите Программу автоматического доказательства Средства поиска или Кода Ошибки при помощи ранее созданного файла опций: Сохраните результаты анализа в подпапке results.
polyspace-bug-finder -options-file psoptions -results-dir results |
Вы видите эту ошибку ссылки (предупреждение в Средстве поиска Ошибки):
Procedure 'main' multiply defined. |
Ошибка происходит, потому что файлы cmd1/cmd1_main.c и cmd2/cmd2_main.c оба имеют функцию main. Когда вы запускаете свою команду сборки, эти два файла используются в отдельных целях в make-файле. Однако polyspace-configure по умолчанию создает один файл опций для полной сборки. Файл опций Polyspace содержит оба исходных файла, приводящие к конфликтным определениям функции main.
Чтобы проверить причину ошибки, откройте файл опций Polyspace psoptions. Вы видите эти строки, которые включают файлы с конфликтными определениями функции main.
-sources src/cmd1/cmd1_main.c -sources src/cmd2/cmd2_main.c |
Чтобы избежать ошибки ссылки, создайте исходный код для определенного двоичного файла при трассировке команды сборки при помощи polyspace-configure.
Например, создайте свой исходный код для бинарного cmd1.o. Укажите, что make-файл предназначается для cmd1 для make, который создает этот двоичный файл.
polyspace-configure -output-options-file psoptions make -B cmd1 |
Запустите Программу автоматического доказательства Средства поиска или Кода Ошибки при помощи ранее созданного файла опций.
polyspace-bug-finder -options-file psoptions -results-dir results |
Ошибка ссылки не происходит, и анализ выполнение до завершения. Можно открыть файл опций Polyspace psoptions и видеть, что только исходные файлы в подпапке cmd1 и файлах, вовлеченных в создание общих объектов, включены с опцией -sources. Исходные файлы в подпапке cmd2, которые не вовлечены в создание бинарного cmd1.o, не включены в файл опций Polyspace.
Если вы прослеживаете создание общего объекта от библиотек, извлеченные исходные файлы не содержат функцию main. В последующем анализе Программы автоматического доказательства Кода вы видите ошибку из-за недостающего main.
Используйте опцию Polyspace Verify module or library (-main-generator), чтобы сгенерировать функцию main. Задайте опцию в файле опций, который был создан или непосредственно в командной строке. Смотрите Проверяют Приложение C Без основной Функции (Polyspace Code Prover).
На C++ используйте эти дополнительные опции для классов:
Создать файл опций для определенного двоичного файла создало в команде сборки, необходимо знать детали команды сборки. Если вы не знакомы с внутренними деталями команды сборки, можно создать отдельный файл опций Polyspace для каждого двоичного файла, созданного в команде сборки. Подход работает на двоичные файлы, которые являются исполняемыми файлами, разделяемыми (динамическими) библиотеками и статическими библиотеками.
Этот подход работает, только если вы используете эти компиляторы:
GNU C или GNU C++
Microsoft Visual C++
Проследите команду сборки при помощи polyspace-configure.To, создают отдельный файл опций для каждого двоичного файла, используют опцию -module с polyspace-configure.
polyspace-configure -module -output-options-path optionsFilesFolder make -B |
Команда создает файлы опций в папке optionsFilesFolder. В предыдущем примере команда создает четыре файла опций для этих четырех двоичных файлов:
cmd1.psopts
cmd2.psopts
liba_so.psopts
libb_so.psopts
Можно запустить Polyspace на реализации кода определенного двоичного файла при помощи соответствующего файла опций. Например, можно запуститься, Программа автоматического доказательства Кода на реализации кода двоичного файла, созданного из make-файла, предназначаются для cmd1 при помощи этой команды:
polyspace-bug-finder -options-file cmd1.psopts -results-dir results |
Для этого подхода вы не должны знать детали своей команды сборки. Однако, когда вы создаете отдельный файл опций для каждого двоичного файла таким образом, каждый файл опций содержит исходные файлы, непосредственно вовлеченные в двоичный файл а не через общие объекты. Например, файл опций cmd1.psopts в этом примере задает только исходные файлы в подпапке cmd1 а не исходные файлы, вовлеченные в создание общих объектов liba.so и libb.so. Последующий анализ при помощи этого файла опций не может, функции доступа от общих объектов и использования функционируют тупики вместо этого. В анализе Программы автоматического доказательства Кода, если вы видите слишком много оранжевых проверок из-за блокирования, используют подход, утвердил в разделе Create Options File for Specific Binary in Build Command.
Если вы прослеживаете создание общего объекта от библиотек, извлеченные исходные файлы не содержат функцию main. В последующем анализе Программы автоматического доказательства Кода вы видите ошибку из-за недостающего main.
Используйте опцию Polyspace Verify module or library (-main-generator), чтобы сгенерировать функцию main. Задайте опцию в файле опций, который был создан или непосредственно в командной строке. Смотрите Проверяют Приложение C Без основной Функции (Polyspace Code Prover).
На C++ используйте эти дополнительные опции для классов:
polyspace-bug-finder | polyspace-configure
