CBMC starter kit writing proofs

We assume that you have run the script setup.py described in the starter kit installation instructions.

Writing a proof for a function begins with running the script setup-proof.py described in the starter kit installation instructions. If FUNCTION is the name of the function given to the setup script, then the script creates a directory names FUNCTION that contains two templates:

• Makefile
• FUNCTION_harness.c

Fill in these templates to write the proof.