Accueil Explorer Aide
Connexion
kindring
/
libpeer
1
0
Fork 0
Fichiers Tickets 0 Pull Requests 0 Wiki
Aborescence: 67da75dea5
Branches Tags
libpeer
/
third_party
/
coreHTTP
/
test
/
cbmc
/
proofs
kindring 67da75dea5 初次提交 il y a 7 mois
..
HTTPClient_AddHeader 67da75dea5 初次提交 il y a 7 mois
HTTPClient_AddRangeHeader 67da75dea5 初次提交 il y a 7 mois
HTTPClient_InitializeRequestHeaders 67da75dea5 初次提交 il y a 7 mois
HTTPClient_ReadHeader 67da75dea5 初次提交 il y a 7 mois
HTTPClient_Send 67da75dea5 初次提交 il y a 7 mois
HTTPClient_strerror 67da75dea5 初次提交 il y a 7 mois
findHeaderFieldParserCallback 67da75dea5 初次提交 il y a 7 mois
findHeaderOnHeaderCompleteCallback 67da75dea5 初次提交 il y a 7 mois
findHeaderValueParserCallback 67da75dea5 初次提交 il y a 7 mois
httpParserOnBodyCallback 67da75dea5 初次提交 il y a 7 mois
httpParserOnHeaderFieldCallback 67da75dea5 初次提交 il y a 7 mois
httpParserOnHeaderValueCallback 67da75dea5 初次提交 il y a 7 mois
httpParserOnHeadersCompleteCallback 67da75dea5 初次提交 il y a 7 mois
httpParserOnMessageBeginCallback 67da75dea5 初次提交 il y a 7 mois
httpParserOnMessageCompleteCallback 67da75dea5 初次提交 il y a 7 mois
httpParserOnStatusCallback 67da75dea5 初次提交 il y a 7 mois
lib 67da75dea5 初次提交 il y a 7 mois
Makefile-project-defines 67da75dea5 初次提交 il y a 7 mois
Makefile-project-targets 67da75dea5 初次提交 il y a 7 mois
Makefile-project-testing 67da75dea5 初次提交 il y a 7 mois
Makefile-template-defines 67da75dea5 初次提交 il y a 7 mois
Makefile.common 67da75dea5 初次提交 il y a 7 mois
README.md 67da75dea5 初次提交 il y a 7 mois
run-cbmc-proofs.py 67da75dea5 初次提交 il y a 7 mois

README.md

CBMC proofs

This directory contains the CBMC proofs. Each proof is in its own directory.

This directory includes four Makefiles.

One Makefile describes the basic workflow for building and running proofs:

  • Makefile.common:
    • make: builds the goto binary, does the cbmc property checking and coverage checking, and builds the final report.
    • make goto: builds the goto binary
    • make result: does cbmc property checking
    • make coverage: does cbmc coverage checking
    • make report: builds the final report

Three included Makefiles describe project-specific settings and can override definitions in Makefile.common:

  • Makefile-project-defines: definitions like compiler flags required to build the goto binaries, and definitions to override definitions in Makefile.common.
  • Makefile-project-targets: other make targets needed for the project
  • Makefile-project-testing: other definitions and targets needed for unit testing or continuous integration.