<FUNCTION_NAME> proof
This directory contains a memory safety proof for <FUNCTION_NAME>.
To run the proof.
- Add
cbmc
,goto-cc
,goto-instrument
,goto-analyzer
, andcbmc-viewer
to your path. - Run
make
. - Open html/index.html in a web browser.
To use arpa
to simplify writing Makefiles.
- Run
make arpa
to generate a Makefile.arpa that contains relevant build information for the proof. - Use Makefile.arpa as the starting point for your proof Makefile by:
- Modifying Makefile.arpa (if required).
- Including Makefile.arpa into the existing proof Makefile (add
sinclude Makefile.arpa
at the bottom of the Makefile, right beforeinclude ../Makefile.common
).