diff --git a/regression/get_coverage.sh b/regression/get_coverage.sh index 3f2a8e424f3..9ca3561714a 100755 --- a/regression/get_coverage.sh +++ b/regression/get_coverage.sh @@ -9,6 +9,7 @@ if [ $? -ne 0 ]; then printf "ERROR: Could not create output directoy" exit 1 fi +output_dir_abs=`cd $output_dir > /dev/null ; pwd` # Check that the previous command succeded, if not exit. command_status() @@ -49,18 +50,21 @@ lcov -version > $output_dir/cbmc_coverage.out 2>&1 command_status # Remove any previous build that may not have coverage in it. -printf "INFO: Cleaning CBMC build " -make clean -C ../src >> $output_dir/cbmc_coverage.out 2>&1 +printf "INFO: setting up vpath build " +cd ../src +../scripts/vpath-setup.sh coverage-build >> $output_dir_abs/cbmc_coverage.out 2>&1 command_status +cd ../regression printf "INFO: Building CBMC with Code Coverage enabled " # Run the usual make target with --coverage to add gcov instrumentation -make CXXFLAGS="--coverage" LINKFLAGS="--coverage" -C ../src >> $output_dir/cbmc_coverage.out 2>&1 +make CXXFLAGS="--coverage" LINKFLAGS="--coverage" -C ../src/coverage-build/src \ + >> $output_dir/cbmc_coverage.out 2>&1 command_status printf "INFO: Running Regression tests " # Run regression tests which will collect the coverage metrics and put them in the src files -make >> $output_dir/cbmc_coverage.out 2>&1 +make -C ../src/coverage-build/regression >> $output_dir/cbmc_coverage.out 2>&1 printf "[DONE]\n" printf "INFO: Gathering coverage metrics " diff --git a/scripts/vpath-setup.sh b/scripts/vpath-setup.sh new file mode 100755 index 00000000000..611b0056652 --- /dev/null +++ b/scripts/vpath-setup.sh @@ -0,0 +1,76 @@ +#!/bin/bash + +set -e + +if [ $# -ne 1 ] +then + echo "Target directory required" 1>&2 + exit 1 +fi + +if ! make -s generated_files +then + echo "Failed to run 'make generated_files'" 1>&2 + exit 1 +fi + +DEST=$1 + +gen_makefile() +{ + local d=$1 + local m=$2 + + mkdir -p $DEST/src/$d + cat > $DEST/src/$d/$m <> $DEST/src/$d/$m +} + +makefiles=$(find . -name Makefile | grep -v $DEST) + +for m in $makefiles +do + dir=$(dirname $m) + gen_makefile $dir Makefile +done + +gen_makefile big-int makefile + +cp common config.inc $DEST/src/ + +# tweak include paths in config.inc +perl -p -i -e 's/(= \.\.\/\.\.\/)/$1..\/..\//' $DEST/src/config.inc +echo "INCLUDES += -I$PWD" >> $DEST/src/config.inc + +# tweak targets that aren't compatible with vpaths +perl -p -i -e "s{(library/\\*.c)}{$PWD/ansi-c/\$1}" $DEST/src/ansi-c/Makefile +perl -p -i -e 's/^(cprover_library.inc:)/%$1/' $DEST/src/ansi-c/Makefile +perl -p -i -e 's/^(cprover_library.cpp:)/#$1/' $DEST/src/ansi-c/Makefile + +perl -p -i -e 's/^(irep_ids.cpp:)/#$1/' $DEST/src/util/Makefile + +# create sub-directories +mkdir -p $DEST/src/ansi-c/library $DEST/src/ansi-c/literals +mkdir -p $DEST/src/goto-instrument/{accelerate,wmm} +mkdir -p $DEST/src/solvers/{cvc,flattening,floatbv,miniBDD,prop,qbf,refinement,sat,smt1,smt2} + +# copy generated files for coverage reports +for f in \ + ansi-c/ansi_c_lex.yy.cpp ansi-c/scanner.l ansi-c/ansi_c_y.tab.cpp \ + assembler/scanner.l assembler/assembler_lex.yy.cpp \ + jsil/jsil_lex.yy.cpp jsil/scanner.l jsil/jsil_y.tab.cpp \ + json/parser.y json/json_lex.yy.cpp json/json_y.tab.cpp \ + xmllang/scanner.l xmllang/xml_lex.yy.cpp xmllang/xml_y.tab.cpp xmllang/parser.y +do + cp $f $DEST/src/$(dirname $f)/ +done + +cp -aL ../regression $DEST/ diff --git a/src/solvers/Makefile b/src/solvers/Makefile index b806aa47886..95ea7650274 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -120,7 +120,7 @@ SRC = $(CHAFF_SRC) $(BOOLEFORCE_SRC) $(MINISAT_SRC) $(MINISAT2_SRC) \ refinement/refine_arrays.cpp \ miniBDD/miniBDD.cpp -INCLUDES= -I .. \ +INCLUDES += -I .. \ $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \ $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \ $(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE) diff --git a/src/util/Makefile b/src/util/Makefile index f98b6588df8..237236f5230 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -37,11 +37,11 @@ all: util$(LIBEXT) ############################################################################### -irep_ids.h: irep_ids_convert$(EXEEXT) irep_ids.txt - ./irep_ids_convert$(EXEEXT) header < irep_ids.txt > $@ +irep_ids.h: irep_ids.txt irep_ids_convert$(EXEEXT) + ./irep_ids_convert$(EXEEXT) header < $< > $@ -irep_ids.inc: irep_ids_convert$(EXEEXT) irep_ids.txt - ./irep_ids_convert$(EXEEXT) table < irep_ids.txt > $@ +irep_ids.inc: irep_ids.txt irep_ids_convert$(EXEEXT) + ./irep_ids_convert$(EXEEXT) table < $< > $@ irep_ids.cpp: irep_ids.inc irep_ids.h