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
This commit adds some comments that explain how the run-cbmc-proofs.py
script diverges from similar scripts that we use for other projects. The
comments begin with "# PROJECT SPECIFIC".
This commit makes Litani run make with the EXTERNAL_SAT_SOLVER variable
set. The template Makefile uses the value of this variable to determine
which external SAT solver CBMC should call out to. We're using Kissat
because the default SAT solver takes too long on two of the proofs,
MQTT_SerializeConnect and MQTT_Connect.
