feat(tools/cbmc): add script to check CBMC results
This commit adds a python script that compares the CBMC results to the
baseline summaries that are committed in the source tree. If there is a
significant difference, the script returns an error.
A call to the script is added to the CheckCBMC.cmake file. If the script
returns error, the script output is printed on the console, however the
build is not interrupted with an error.
Change-Id: I50e7b9a570c1d30e03def630c6541d63536bd1c1
Signed-off-by: Mate Toth-Pal <mate.toth-pal@arm.com>
diff --git a/tools/cbmc/CheckCBMC.cmake b/tools/cbmc/CheckCBMC.cmake
index 251f541..4eecfdb 100644
--- a/tools/cbmc/CheckCBMC.cmake
+++ b/tools/cbmc/CheckCBMC.cmake
@@ -8,6 +8,13 @@
find_program(RMM_CBMC_PATH "cbmc"
DOC "Path to cbmc.")
+find_package(Python3 REQUIRED)
+find_program(CHECK_CBMC_SUMMARY_EXECUTABLE "compare_summary.py"
+ PATHS ${CMAKE_SOURCE_DIR}
+ PATH_SUFFIXES tools/cbmc
+ DOC "Path to compare_summary.py"
+ )
+
#
# Configure and execute CBMC
#
@@ -193,3 +200,21 @@
endforeach()
message(STATUS "Result in ${RMM_TESTBENCH_RESULT_DIR}")
+
+execute_process(
+ WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
+ COMMAND ${CHECK_CBMC_SUMMARY_EXECUTABLE}
+ ${CMAKE_SOURCE_DIR}/tools/cbmc/testbenches_results/BASELINE.${CBMC_RESULT_FILE_SUFFIX}
+ ${RMM_TESTBENCH_RESULT_DIR}/${SUMMARY_FILE}
+ OUTPUT_VARIABLE CHECK_SUMMARY_OUTPUT
+ ERROR_VARIABLE CHECK_SUMMARY_ERROR
+ RESULT_VARIABLE CHECK_SUMMARY_RC
+ OUTPUT_STRIP_TRAILING_WHITESPACE
+ )
+
+if (NOT ${CHECK_SUMMARY_RC} EQUAL "0")
+ message(WARNING
+ "cbmc-${CBMC_RESULT_FILE_SUFFIX}: FAILED\n${CHECK_SUMMARY_ERROR}")
+else()
+ message(STATUS "cbmc-${CBMC_RESULT_FILE_SUFFIX}: PASSED")
+endif()