Skip to content

CBMC starter kit harness

Mark Tuttle edited this page Oct 29, 2020 · 2 revisions

Each proof directory contains a proof harness. For the function FUNCTION, the directory cbmc/proofs/FUNCTION contains a file FUNCTION_harness.c. The script setup-proof.py installs a blank template for this file, and the proof writer fills it in.