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