feat(tools/cbmc): add option to test a single testbench
This feature becomes useful when working on a single testbench. There is
no need to wait for the other testbenches to finish analysis.
Change-Id: I277b37ef796c66c26c03c4b3ca2cd29c705cfc88
Signed-off-by: Mate Toth-Pal <mate.toth-pal@arm.com>
diff --git a/tools/cbmc/CheckCBMC.cmake b/tools/cbmc/CheckCBMC.cmake
index 1f9d030..e31e82f 100644
--- a/tools/cbmc/CheckCBMC.cmake
+++ b/tools/cbmc/CheckCBMC.cmake
@@ -132,7 +132,8 @@
message(FATAL_ERROR "Invalid RMM_CBMC_CONFIGURATION '${RMM_CBMC_CONFIGURATION}'")
endif()
-file(GLOB_RECURSE TESTBENCH_FILES "${TESTBENCH_DIR}/*.c")
+# Convert the space separated strings to a CMake list
+string(REPLACE " " ";" TESTBENCH_FILES "${TESTBENCH_FILES}")
#
# Create semi-colon separated list from white-space seperated ones.
@@ -273,10 +274,12 @@
endforeach()
message(STATUS "Result in ${RMM_TESTBENCH_RESULT_DIR}")
+list(TRANSFORM TESTBENCH_FILES REPLACE "${TESTBENCH_DIR}/" "" OUTPUT_VARIABLE TESTBENCH_FILENAMES)
execute_process(
WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
COMMAND ${CHECK_CBMC_SUMMARY_EXECUTABLE}
${CMAKE_SOURCE_DIR}/tools/cbmc/testbenches_results/BASELINE.${CBMC_RESULT_FILE_SUFFIX}
+ --testbench-files "${TESTBENCH_FILENAMES}"
${RMM_TESTBENCH_RESULT_DIR}/${SUMMARY_FILE}
OUTPUT_VARIABLE CHECK_SUMMARY_OUTPUT
ERROR_VARIABLE CHECK_SUMMARY_ERROR