kindring 67da75dea5 初次提交 2 ヶ月 前
..
Makefile 67da75dea5 初次提交 2 ヶ月 前
README.md 67da75dea5 初次提交 2 ヶ月 前
cbmc-proof.txt 67da75dea5 初次提交 2 ヶ月 前
cbmc-viewer.json 67da75dea5 初次提交 2 ヶ月 前
findHeaderOnHeaderCompleteCallback_harness.c 67da75dea5 初次提交 2 ヶ月 前

README.md

findHeaderOnHeaderCompleteCallback proof

This directory contains a memory safety proof for findHeaderOnHeaderCompleteCallback.

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.