Run VeriFast proofs together with CBMC proofs

This commit changes the run-cbmc-proofs.py script so that it also adds
Litani jobs for each of the VeriFast proofs. The result of the VeriFast
proofs is presented on the Litani dashboard alongside the existing CBMC
proofs.

FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py

@@ -157,7 +157,7 @@ def run_build(litani, jobs):
 
 
 def get_litani_path(proof_root):
-    return proof_root.parent.parent / "litani" / "litani"
+    return "litani"
 
 
 def add_proof_jobs(proof_directory, proof_root, litani):
@@ -305,9 +305,53 @@ def main():
             "Failed to configure the following proofs:\n%s", "\n".join(
                 [str(f) for f in counter["fail"]]))
 
+    add_verifast_proofs(litani, proof_root.parent.parent / "VeriFast")
+
     if not args.no_standalone:
         run_build(litani, args.parallel_jobs)
 
 
+def add_verifast_proofs(litani, verifast_root):
+    with open(verifast_root / "proof-configuration") as handle:
+        for line in handle:
+            line = line.strip()
+            if line.startswith("#") or not line:
+                continue
+
+            parts = line.split()
+            coverage, proof_name, flags = parts[0], parts[1], ""
+            if len(parts) > 2:
+                flags = " ".join(parts[2:])
+            fyle = verifast_root / proof_name
+
+            out_file = verifast_root / "out" / f"{proof_name}.stdout"
+            cmd = f"verifast -I include -c {flags} {fyle.resolve()}"
+
+            run_cmd([
+                str(litani), "add-job",
+                "--command", cmd,
+                "--outputs", str(out_file),
+                "--stdout-file", str(out_file),
+                "--pipeline-name", f"VeriFast/{proof_name}",
+                "--ci-stage", "test",
+                "--cwd", str(verifast_root),
+                "--tags", "tool:verifast",
+                "--description", f"{proof_name}: running VeriFast",
+            ], check=True)
+
+            run_cmd([
+                str(litani), "add-job",
+                "--command", f"grep '{coverage} statements verified' < {out_file}",
+                "--inputs", str(out_file),
+                "--phony-outputs", f"{proof_name}_coverage_result",
+                "--pipeline-name", f"VeriFast/{proof_name}",
+                "--ci-stage", "report",
+                "--cwd", str(verifast_root),
+                "--tags", "tool:verifast",
+                "--description", f"{proof_name}: checking VeriFast coverage",
+            ], check=True)
+
+
+
 if __name__ == "__main__":
     main()

FreeRTOS/Test/VeriFast/proof-configuration

@@ -0,0 +1,28 @@
+# Expected Coverage
+# --- Proof Filename
+# --------------------------------------- Verifast Flags
+
+314   list/listLIST_IS_EMPTY.c
+440   list/uxListRemove.c
+329   list/vListInitialise.c
+316   list/vListInitialiseItem.c
+308   queue/prvCopyDataFromQueue.c
+289   queue/prvIsQueueEmpty.c
+289   queue/prvIsQueueFull.c
+290   queue/prvLockQueue.c
+304   queue/prvUnlockQueue.c
+292   queue/uxQueueMessagesWaiting.c
+290   queue/uxQueueSpacesAvailable.c
+287   queue/vQueueDelete.c
+335   queue/xQueueGenericSend.c
+287   queue/xQueueIsQueueEmptyFromISR.c
+287   queue/xQueueIsQueueFullFromISR.c
+335   queue/xQueuePeek.c
+300   queue/xQueuePeekFromISR.c
+337   queue/xQueueReceive.c
+314   queue/xQueueReceiveFromISR.c        -disable_overflow_check
+317   queue/xQueueGenericSendFromISR.c    -disable_overflow_check
+456   list/vListInsert.c                  -disable_overflow_check
+410   list/vListInsertEnd.c               -disable_overflow_check
+315   queue/create.c                      -disable_overflow_check
+336   queue/prvCopyDataToQueue.c          -disable_overflow_check