Документация

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

Смотрите 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

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

polyspace-code-prover -options-file psoptions -results-dir results

Вы видите эту ошибку ссылки (предупреждение в Bug Finder):

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

Запустите Bug Finder или Программу автоматического доказательства Кода при помощи ранее созданного файла опций.

polyspace-code-prover -options-file psoptions -results-dir results

Ошибка ссылки не происходит, и анализ выполнение до завершения. Можно открыть файл опций Polyspace psoptions и смотрите что только исходные файлы в cmd1 подпапка и файлы, вовлеченные в создание общих объектов, включены с -sources опция. Исходные файлы в cmd2 подпапка, которые не вовлечены в создание бинарного cmd1.o, не включены в файл опций Polyspace.

Создайте один файл опций на двоичный файл, созданный в команде сборки

Создать файл опций для определенного двоичного файла создало в команде сборки, необходимо знать детали команды сборки. Если вы не знакомы с внутренними деталями команды сборки, можно создать отдельный файл опций Polyspace для каждого двоичного файла, созданного в команде сборки. Подход работает на двоичные файлы, которые являются исполняемыми файлами, разделяемыми (динамическими) библиотеками и статическими библиотеками.

Этот подход работает, только если вы используете эти компиляторы:

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

polyspace-configure -module -output-options-path optionsFilesFolder make -B

Команда создает файлы опций в папке optionsFilesFolder. В предыдущем примере команда создает четыре файла опций для этих четырех двоичных файлов:

Можно запустить Polyspace на реализации кода определенного двоичного файла при помощи соответствующего файла опций. Например, можно запуститься, Программа автоматического доказательства Кода на реализации кода двоичного файла, созданного из make-файла, предназначаются для cmd1 при помощи этой команды:

polyspace-code-prover -options-file cmd1.psopts -results-dir results

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

#!/bin/bash
FILEPATHS=optionsFilesFolder/*.psopts
for filePath in $FILEPATHS
do
    echo "Running Polyspace on $filePath"
    fileName="${filePath##*/}"
    resultsDirName="${fileName%.*}"
    logName="{fileName%.*}.log"
    polyspace-code-prover -options-file "$filePath" -results-dir "${resultsDirName}" >> "${logName}"
done

Для этого подхода вы не должны знать детали своей команды сборки. Однако, когда вы создаете отдельный файл опций для каждого двоичного файла таким образом, каждый файл опций содержит исходные файлы, непосредственно вовлеченные в двоичный файл а не через общие объекты. Например, файл опций cmd1.psopts в этом примере задает только исходные файлы в cmd1 подпапка а не исходные файлы, вовлеченные в создание общих объектов liba.so и libb.so. Последующий анализ при помощи этого файла опций не может, функции доступа от общих объектов и использования функционируют тупики вместо этого. В анализе Программы автоматического доказательства Кода, если вы видите слишком много оранжевых проверок из-за блокирования, используют подход, утвердил в разделе Create Options File for Specific Binary in Build Command.