diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake')
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake b/FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake new file mode 100644 index 000000000..8dc37b094 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake @@ -0,0 +1,14 @@ +execute_process( + COMMAND + cbmc --trace --unwinding-assertions + ${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 return code '${res}' for proof ${proof_name}. Log written to ${out_file}." + ) +endif() |