Skip to content

Commit 9066f2c

Browse files
karkhazpaulbartell
andauthored
Upgrade proof tool submodules (#102)
* Upgrade proof tool submodules This commit advances Litani to release 1.10.0, and the starter kit to the tip-of-tree. This brings the following improvements: - Profiling - Litani measures the memory usage of the CBMC safety checking and coverage checking jobs - The dashboard includes box-and-whisker diagrams for memory use per proof - The dashboard includes a graph of how many parallel jobs are running over the whole run, making it easy to choose a CI machine with enough parallelism - It is now possible to designate particular proofs as "EXPENSIVE"; Litani runs expensive proofs serially, ensuring that they do not over-consume resources like RAM. - UI improvements - Each pipeline page includes a table of contents - Each pipeline page includes a dependency graph of the pipeline - Each job on the pipeline page has a hyperlink to that job - The terminal output is now less noisy * Symlink run-cbmc-proofs.py to starter kit The run script is now a symbolic link into the starter kit submodule, meaning that it will be updated whenever the starter kit is. This is done iso that E-SDK doesn't carry custom modifications to the run script unless necessary; previous commits have made the E-SDK proofs consistent with the generic starter kit conventions. Co-authored-by: Paul Bartell <[email protected]>
1 parent 53194dc commit 9066f2c

File tree

4 files changed

+4
-260
lines changed

4 files changed

+4
-260
lines changed

test/cbmc/.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ proofs/**/gotos
44
proofs/**/report
55
proofs/**/html
66
proofs/**/core_json.c
7+
proofs/output
78

89
# Emitted by CBMC Viewer
910
TAGS-*

test/cbmc/litani

Submodule litani updated 55 files

test/cbmc/proofs/run-cbmc-proofs.py

-258
This file was deleted.

test/cbmc/proofs/run-cbmc-proofs.py

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../aws-templates-for-cbmc-proofs/template-for-repository/proofs/run-cbmc-proofs.py

0 commit comments

Comments
 (0)