1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
#!/bin/bash
# By default remove temporary files after the run
keep_files=false
# Get a unique number to prevent collision of output files
output_dir=`mktemp -d ./coverage_XXXXX`
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()
{
if [ $? -ne 0 ]; then
printf "[ERROR]\n"
echo "ERROR: See $output_dir/cbmc_coverage.out for more information"
exit 1
fi
printf "[OK]\n"
}
# Print usage
print_usage()
{
echo "Usage: $0 [-k]"
echo " -k Keep all raw coverage files"
}
#Check the options that the user provided
while getopts ":k" opt
do
case $opt in
k)
keep_files=true
;;
\?)
echo "ERROR: Invalid option: -$opt"
print_usage
exit 1
;;
esac
done
# Check that lcov has been installed
printf "INFO: Checking lcov is installed "
lcov -version > $output_dir/cbmc_coverage.out 2>&1
command_status
# Remove any previous build that may not have coverage in it.
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/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 -C ../src/coverage-build/regression >> $output_dir/cbmc_coverage.out 2>&1
printf "[DONE]\n"
printf "INFO: Gathering coverage metrics "
# Gather all of the coverage metrics into a single file
lcov --capture --directory ../src --output-file $output_dir/cbmc_coverage.info >> $output_dir/cbmc_coverage.out 2>&1
command_status
printf "INFO: Removing unwanted metrics (for external libaries) "
# Remove the metrics for files that aren't CBMC's source code
lcov --remove $output_dir/cbmc_coverage.info '/usr/*' --output-file $output_dir/cbmc_coverage.info >> $output_dir/cbmc_coverage.out 2>&1
command_status
printf "INFO: Creating coverage report "
# Generate the HTML coverage report
genhtml $output_dir/cbmc_coverage.info --output-directory $output_dir/cbmc_coverage >> $output_dir/cbmc_coverage.out 2>&1
command_status
echo "INFO: Coverage report is availabe in $output_dir/cbmc_coverage"
if [ $keep_files == false ]; then
# Remove the temporary coverage files
printf "INFO: Removing temporary coverage files (1 of 2) "
find ../ -name "*.gcda" -delete >> $output_dir/cbmc_coverage.out 2>&1
command_status
printf "INFO: Removing temporary coverage files (2 of 2) "
find ../ -name "*.gcno" -delete >> $output_dir/cbmc_coverage.out 2>&1
command_status
fi
|
