bounded-model-checking-c

# Bounded model checking C ## Contract | Field | Bound contract | |---|---| | Trigger | A C or C++ function or module needs its memory safety, arithmetic, or user assertions checked exhaustively up to a bound (CBMC), its runtime errors bounded by abstract interpretation (Frama-C Eva), or its ACSL contracts proved deductively (Frama-C WP), or an existing run's trace or alarm must be read. | | Authority | Reversible local: writes harness `.c` files, ACSL annotations in the source under analysis, and the tools' output directories; rollback is reverting those files. No remote mutation. | | Side effect | Harness and annotated source on disk, CBMC GOTO binaries when `goto-cc` is used, WP proof-obligation files under `-wp-out`, and Frama-C session files when `-save` is used. | | Done | Every property in scope is reported safe by CBMC under a recorded unwind bound, or has no Eva alarm, or is `Valid` under WP with a named prover, or has a trace or alarm mapped to a code defect and a fix. | ## Inputs The C sources, the entry function, and the properties: absence of undefined behavior (out-of-bounds access, null or dangling dereference, overflow, division by zero), or functional contracts. Tool pins from the grounded set: CBMC cbmc-6.11.0 (`brew install cbmc` on macOS, `.deb` or `.msi` packages, or Docker `ghcr.io/diffblue/cbmc`) and Frama-C 33.0 "Arsenic" (`opam install frama-c`, or the Linux `.run` installer `frama-c-linux-x86-64-33.0-Arsenic.run`); WP needs Why3 and at least one ...