2021-11-30 14:51:24 +01:00
..
2021-11-30 14:51:24 +01:00
2021-11-30 14:51:24 +01:00
2021-11-30 14:51:24 +01:00
2021-11-30 14:51:24 +01:00
2021-11-30 14:51:24 +01:00

<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, and cbmc-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:
    1. Modifying Makefile.arpa (if required).
    2. Including Makefile.arpa into the existing proof Makefile (add sinclude Makefile.arpa at the bottom of the Makefile, right before include ../Makefile.common).