diff --git a/COMPILING b/COMPILING index a9681890bd..13b8339abd 100644 --- a/COMPILING +++ b/COMPILING @@ -203,3 +203,20 @@ To work with Eclipse, do the following: 6) Select Project -> Build All +CODE COVERAGE +------------- + +Code coverage metrics are provided using gcov and lcov. Ensure that you +have installed lcov from http://ltp.sourceforge.net/coverage/lcov.php +note for ubuntu lcov is available in the standard apt-get repos. + +To get coverage metrics run the following script from the regression +directory: + + get_coverage.sh + +This will: + 1) Rebuild CBMC with gcov enabled + 2) Run all the regression tests + 3) Collate the coverage metrics + 4) Provide an HTML report of the current coverage diff --git a/regression/get_coverage.sh b/regression/get_coverage.sh new file mode 100755 index 0000000000..e4907835e2 --- /dev/null +++ b/regression/get_coverage.sh @@ -0,0 +1,55 @@ +#!/bin/bash + +# Get a unique number to prevent collision of output files +outputDir=`mktemp -d ./coverage_XXXXX` +if [ $? -ne 0 ]; then + printf "ERROR: Could not create output directoy" + exit 1 +fi + +# Check that the previous command succeded, if not exit. +commandStatus() +{ + if [ $? -ne 0 ]; then + printf "[ERROR]\n" + echo "ERROR: See $outputDir/cbmc_coverage.out for more information" + exit 1 + fi + printf "[OK]\n" +} + +# Check that lcov has been installed +printf "INFO: Checking lcov is installed " +lcov -version > $outputDir/cbmc_coverage.out 2>&1 +commandStatus + +# Remove any previous build that may not have coverage in it. +printf "INFO: Cleaning CBMC build " +make clean -C ../src >> $outputDir/cbmc_coverage.out 2>&1 +commandStatus + +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 >> $outputDir/cbmc_coverage.out 2>&1 +commandStatus + +printf "INFO: Running Regression tests " +# Run regression tests which will collect the coverage metrics and put them in the src files +make >> $outputDir/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 $outputDir/cbmcCoverage.info >> $outputDir/cbmc_coverage.out 2>&1 +commandStatus + +printf "INFO: Removing unwanted metrics (for external libaries) " +# Remove the metrics for files that aren't CBMC's source code +lcov --remove $outputDir/cbmcCoverage.info '/usr/*' --output-file $outputDir/cbmcCoverage.info >> $outputDir/cbmc_coverage.out 2>&1 +commandStatus + +printf "INFO: Creating coverage report " +# Generate the HTML coverage report +genhtml $outputDir/cbmcCoverage.info --output-directory $outputDir/cbmcCoverage >> $outputDir/cbmc_coverage.out 2>&1 +commandStatus +echo "INFO: Coverage report is availabe in $outputDir/cbmcCoverage"