Постройте анализ Polyspace из модулей при помощи команды сборки

Чтобы сконфигурировать анализ Polyspace®, можно снова использовать параметры компиляции в команде сборки, такие как make. Во-первых, вы прослеживаете свою команду сборки с polyspace-configure (или polyspaceConfigure в MATLAB®) и создаете файл опций Polyspace. Вы позже задаете этот файл опций для последующего анализа Polyspace.

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

Эта тема показывает, как создать отдельный файл опций Polyspace для каждого двоичного файла, созданного в вашем make-файле. Предположим, что make-файл создает четыре двоичных файла: два исполняемых файла (предназначаются для cmd1 и cmd2), и две разделяемых библиотеки (предназначаются для liba и libb). Можно создать отдельный файл опций Polyspace для каждого из этих двоичных файлов.

Чтобы попробовать этот пример, используйте файлы в polyspaceroot\help\toolbox\codeprover\examples\multiple_modules. Здесь, polyspaceroot является папкой установки Polyspace, например, C:\Program Files\Polyspace\R2019a или C:\Program Files\Polyspace Server\R2019a.

Создайте исходный код

Осмотрите 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 для полной сборки

Проследите команду сборки при помощи polyspace-configure. Используйте опцию -output-options-file, чтобы создать файл опций Polyspace psoptions из команды сборки.

polyspace-configure -output-options-file psoptions make -B

Запустите Программу автоматического доказательства Средства поиска или Кода Ошибки при помощи ранее созданного файла опций: Сохраните результаты анализа в подпапке results.

polyspace-code-prover -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-code-prover -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 Без основной Функции.

На 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-code-prover -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 Без основной Функции.

На C++ используйте эти дополнительные опции для классов:

Смотрите также

|

Похожие темы