From c5c41ef3af679c77657431da528b8e7c33423d32 Mon Sep 17 00:00:00 2001 From: ActoryOu Date: Fri, 22 Mar 2024 10:43:47 +0800 Subject: [PATCH] Update result section in README under CBMC folder. (#1196) * Update result section in README under CBMC folder * Code review suggestions Signed-off-by: Gaurav Aggarwal * Update proofs result path --------- Signed-off-by: Gaurav Aggarwal Co-authored-by: Gaurav Aggarwal Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com> --- FreeRTOS/Test/CBMC/README.md | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/FreeRTOS/Test/CBMC/README.md b/FreeRTOS/Test/CBMC/README.md index 8c0576f489..4b3e6de4a4 100644 --- a/FreeRTOS/Test/CBMC/README.md +++ b/FreeRTOS/Test/CBMC/README.md @@ -72,11 +72,19 @@ Each of the leaf directories under `proofs` is a proof of the memory safety of a single entry point in FreeRTOS. The scripts that you ran in the previous step will have left a Makefile in each of those directories. To run a proof, change into the directory for that proof and run `make`. -The proofs may take some time to run; they eventually write their output to -`cbmc.txt`, which should have the text `VERIFICATION SUCCESSFUL` at the end. +The proofs may take some time to run. -The make command will also generate a report in html and json format which makes -understanding the failures easier. +### Proof results + +The `make` command above generates a report in HTML and JSON format. Taking +[TaskCreate](./proofs/Task/TaskCreate) as an example: + +* HTML report is generated at `./proofs/Task/TaskCreate/html/html`. +* JSON report is generated at `./proofs/Task/TaskCreate/html/json`. + +You can open `./proofs/Task/TaskCreate/html/html/index.html` in any browser to view +the HTML report. You should see `None` under the `Errors` section in case of a +successful run. ### Proof directory structure