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

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

Проверьте файл 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 для полной сборки

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

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

Запустите Bug Finder или Code Prover с помощью ранее созданного файла опций: Сохраните результаты анализа в 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 функция. Когда вы запускаете команду build, два файла используются в отдельных целях в make-файле. Однако polyspace-configure по умолчанию создает один файл опций для полной сборки. Файл опций Polyspace содержит оба исходных файла, что приводит к конфликтным определениям main функция.

Чтобы проверить причину ошибки, откройте файл опций Polyspace psoptions. Вы видите эти линии, которые включают файлы с конфликтующими определениями main функция.

-sources src/cmd1/cmd1_main.c
-sources src/cmd2/cmd2_main.c

Создайте файл опций для определенного двоичного файла в команде Build

Чтобы избежать ошибки ссылки, создайте исходный код для определенного двоичного кода при трассировке вашей команды сборки при помощи polyspace-configure.

Например, создайте свой исходный код для двоичного cmd1.o. Задайте конечный объект make-файла cmd1 для make, что создает эту двоичную единицу.

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

Запустите Bug Finder или Code Prover при помощи ранее созданного файла опций.

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

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

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

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

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

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

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

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

Запустить Polyspace о реализации кода определенного двоичного файла можно при помощи соответствующего файла опций. Например, можно запустить Code Prover для реализации кода двоичного файла, созданного из целевого файла 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

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