diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake')
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake b/FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake new file mode 100644 index 000000000..819fa11bb --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake @@ -0,0 +1,14 @@ +execute_process( + COMMAND + cbmc --cover location --xml-ui + ${cbmc_flags} ${cbmc_verbosity} ${goto_binary} + OUTPUT_FILE ${out_file} + ERROR_FILE ${out_file} + RESULT_VARIABLE res +) + +if(NOT (${res} EQUAL 0 OR ${res} EQUAL 10)) + message(FATAL_ERROR + "Unexpected CBMC coverage return code '${res}' for proof ${proof_name}. Log written to ${out_file}." + ) +endif() |