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

Исходный код построения

Проверьте файл макияжа. 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

Убедитесь, что построение завершается.

Создание файла параметров одного пространства для полного построения

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

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

Запустите средство поиска ошибок или средство проверки кода, используя ранее созданный файл параметров. Сохраните результаты анализа в results подпапка.

polyspace-bug-finder -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

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

Например, создайте исходный код для двоичного файла cmd1.o. Укажите цель makefile 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.

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

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

Этот подход работает только при использовании следующих компиляторов:

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

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

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

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

polyspace-bug-finder -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%.*}_results"
    logName="${fileName%.*}.log"
    polyspace-bug-finder -options-file "$filePath" -results-dir "${resultsDirName}" >> "${logName}"
done

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