alwin.berger/FRET-FreeRTOS
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
FRET-FreeRTOS/FreeRTOS-Plus/Source/AWS/device-defender/test/cbmc/proofs/Defender_MatchTopic
History
Alwin Berger 20d74ab530 init
2021-11-30 14:51:24 +01:00
..
cbmc-proof.txt
init
2021-11-30 14:51:24 +01:00
cbmc-viewer.json
init
2021-11-30 14:51:24 +01:00
Defender_MatchTopic_harness.c
init
2021-11-30 14:51:24 +01:00
Makefile
init
2021-11-30 14:51:24 +01:00
README.md
init
2021-11-30 14:51:24 +01:00

README.md

Defender_MatchTopic proof

This directory contains a memory safety proof for Defender_MatchTopic.

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).