Mark Tuttle
Mark Tuttle
I've installed kani on Apple M1 running MacOS 11.6.5 with ``` git clone https://github.com/model-checking/kani.git kani cd kani && git submodule update --init PATH=$HOME/.cargo/bin:$PATH && cd kani && \ ./scripts/setup/macos-10.15/install_deps.sh &&...
The proof readme files copied into cbmc/proofs and cbmc/proofs/PROOFDIR are giving old instructions for how to install cbmc and run the proofs.
Reported by Oliver Lavery: Any DEFINES and INCLUDES in the proof Makefile get overwritten by Makefile-project-defines. Makefile.common is included at the end of the proof Makefile, and Makefile-project-defines does a...
We need the ability to test changes against a large subset of the proofs using the starter kit. The tooling branch of the fork https://github.com/markrtuttle/aws-viewer-for-cbmc contains preliminary work on this,...
The functions [link_text_to_file](https://github.com/awslabs/aws-viewer-for-cbmc/blob/aff75c57673da2dd092f98f9491a37a7f07250e7/cbmc_viewer/markup_link.py#L44) and [link_text_to_line](https://github.com/awslabs/aws-viewer-for-cbmc/blob/aff75c57673da2dd092f98f9491a37a7f07250e7/cbmc_viewer/markup_link.py#L54) should take an option "escape=True" argument and invoke html.escape on the text strings when escape is true. The invocation of html.escape in [format_srcloc](https://github.com/awslabs/aws-viewer-for-cbmc/blob/60c47b13b64265112d3b4b2fe2498049be524fcb/cbmc_viewer/markup_trace.py#L152) should be...
Replace os.path with pathlib.Path for readability and portability across operating systems.
Currently, when the `--property` flag is omitted, the errors are reported as "other errors" without line numbers or traces. All that is missing is the property description from the `--property`...
- Create a "proof assumptions" section in report that lists all expected stubs and expected undefined functions. The definition of expected comes from the cbmc-viewer.json proof configuration file. - Report...
We should restrict coverage to the reachable functions. Currently coverage checking reports coverage on all code, not just the statically reachable code. Prior attempts to restrict to reachable functions were...