diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/cmake')
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake | 14 | ||||
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/cmake/compute-property.cmake | 14 | ||||
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake | 14 |
3 files changed, 42 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() 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() 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() |