Update CBMC proofs for llhttp #127
Conversation
| @@ -67,7 +66,7 @@ UNWINDSET += strncmp.0:5 | |||
|
|
|||
There was a problem hiding this comment.
Lines 58-61 should be reevaluated given these warnings: https://d39z7xfr4hj3jh.cloudfront.net/final/f6b58be4-d13f-4665-9be6-c5c08cfb8476/artifacts/HTTPClient_Send/report/html/index.html
There was a problem hiding this comment.
These are all present in the main branch: https://d39z7xfr4hj3jh.cloudfront.net/final/4b7c2384-c743-404b-8e74-9eb0ab5e3b0a/artifacts/HTTPClient_Send/report/html/index.html. They're not a result of these changes. I planned to follow up in the CBMC chat, but I don't think it should block this PR going into dev.
There was a problem hiding this comment.
Followed up with CBMC and there's an open issue for this: model-checking/cbmc-starter-kit#88
| @@ -26,17 +26,17 @@ | |||
| */ | |||
There was a problem hiding this comment.
The makefile for this case needs a loop unwindset updated: https://d39z7xfr4hj3jh.cloudfront.net/final/f6b58be4-d13f-4665-9be6-c5c08cfb8476/artifacts/findHeaderFieldParserCallback/report/html/index.html
There was a problem hiding this comment.
I tested removing that unwindset and the test fails, so it is doing something despite what the warning indicates. I'll ask in the cbmc group.
* Replace http-parser with llhttp (#126) * Add llhttp submodule * Replace http-parser with llhttp in source * Fix CI checks * Fix unit tests 100% coverage * Rename functions * Disable strict mode * Remove http-parser submodule * Update CBMC proofs for llhttp (#127) * Update CBMC proofs * Update execute mocks * Rename stub file * Return error fields from stubs * Remove unused variable (#128) * Remove unused variable * Void unused status code * Address review comments Signed-off-by: Gaurav Aggarwal <[email protected]> Co-authored-by: Muneeb Ahmed <[email protected]>
Description:
Updates the CBMC proofs to compile after the parser was changed from http-parser to llhttp. All tests pass, but some proofs may not have 100% coverage for some functions, which are covered by different proofs. The
HTTPClient_SendandHTTPClient_ReadHeaderproofs are the ones affected by thehttp-parser->llhttpchange, and both have coverage equal or better than that of themainbranch.