-
Notifications
You must be signed in to change notification settings - Fork 21
CBMC starter kit setup proof script
Rémi Delmas edited this page Aug 2, 2021
·
4 revisions
For each proof, run the script scripts/setup-proof.py
to create a directory containing all the files you need to write a proof for a functions. The script will ask you for
- The name of the function under test.
- The path to the source file defining the function under test.
- The path to the source root (which is
${SRCDIR}
). - The path to the proof root (which is
${CBMC_ROOT}/proofs
).
cd ${PROOF_ROOT}
python3 ../aws-templates-for-cbmc-proofs/scripts/setup-proof.py
What is the function name? device_read
What is the path to the source file defining the function? /usr/project/src/device.c
What is the path to the source root? /usr/project
What is the path to the 'proofs' directory (usually '.')? .
The script will use the function name FUNCTION you that you give to create a directory FUNCTION. Files in that directory include:
- FUNCTION_harness.c: This is a template for the proof harness for the function FUNCTION.
-
Makefile: This is a template for the Makefile to build and check your proof (using
../Makefile.common
described above).
That this point you should be able to cut-and-paste into these templates, type make report
, and being debugging your first proof!