Immutable. This exact content is served forever at /api/v1/blob/0b94f334cd0d90df.
--- name: bounded-model-checking-c description: 'Use when C or C++ code needs memory-safety or undefined-behavior guarantees proved with CBMC, or ACSL contracts checked with Frama-C Eva or WP. Not for choosing the proof policy: use proof-driven.' --- # 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 prover on `PATH`, and Alt-Ergo is the documented first choice. Optional: per-loop unwind bounds, the target data model (`--LP64`, `--ILP32`), and an Eva precision level. ## Procedure 1. Pick the analysis. CBMC answers "is there any input within the bound that reaches a failing check" and produces a concrete trace, so it is the default for a function with a small loop bound. Eva answers "which operations may be unsafe for any input" over the whole program without a bound, at the price of alarms that may be false. WP answers "does this function meet its ACSL contract" and needs the contract written first. Done when: one analysis is named with the reason. 2. Write a CBMC harness. In a new file, declare unconstrained inputs with the `nondet_` prefix convention (`int nondet_int();`, `_Bool nondet_bool();`), which CBMC treats as a fresh value on every call. Write a `harness` function that builds the inputs, restricts them with `__CPROVER_assume(cond)`, calls the function under test, and states the property with `__CPROVER_assert(cond, "description")` or plain `assert`. Since CBMC 6.0 the standard checks (bounds, pointer, division by zero, shift, signed overflow, unwinding assertions) are on by default; add `--unsigned-overflow-check`, `--conversion-check`, or `--memory-leak-check` when those classes matter, and `--no-standard-checks` only with a written reason. Done when: `cbmc harness.c src.c --function harness --show-properties` lists the checks the run will decide. 3. Run CBMC and read the result. `cbmc harness.c src.c --function harness --unwind 10 --trace`. `--unwind N` bounds every loop; `--unwindset L:B` bounds one loop by the id shown by `--show-loops`. A run ends with `VERIFICATION SUCCESSFUL` (exit 0), `VERIFICATION FAILED` (exit 10), or `VERIFICATION INCONCLUSIVE` (exit 5); exit 1, 2, and 6 are usage, parse, and internal errors. On failure, each violated property is listed with its id and description, and `--trace` prints the counterexample as numbered states with every assignment from the entry to the failing line. Read the assignments to the harness inputs first: they are the concrete input that breaks the property. A failed unwinding assertion means the bound is too small, not that the code is wrong; raise the bound and rerun. Use `--property id` to rerun one property and `--json-ui` when a script reads the result. Done when: every property passes, or the trace's concrete inputs are recorded with the source line they break. 4. Reduce the CBMC problem when it does not finish. Use `--slice-formula` to drop assignments that cannot reach the property, `--depth N` to cap the path length, and `--object-bits n` when the run reports too many objects. For a multi-file program, compile with `goto-cc -c src.c -o src.goto` and link the GOTO binaries once, then run `cbmc program.goto --function harness ...` for each property. Swap the backend with `--z3` or `--cvc5` when the default SAT solver stalls. Done when: the run finishes at a recorded bound, or the smallest harness that reproduces the stall is saved. 5. Run Eva. `frama-c -eva -main entry src.c`. Each alarm prints as `[eva:alarm] file.c:LINE: Warning: <description>.` followed by the ACSL assertion Eva could not prove, for example `assert \valid(p);`. The summary at the end counts alarms and the proportion of statements reached. Raise `-eva-precision N` (0 to 11) to trade time for fewer false alarms; `-eva-slevel N` allows N separate states per program point, which removes alarms caused by merging branches. Insert `Frama_C_show_each(expr)` in the source to print Eva's value set at that point when an alarm is not obvious. Classify each remaining alarm as a true defect (a concrete input reaches it, which a CBMC harness on that function can confirm) or a precision loss. Done when: every alarm is classified, and true defects carry a fix. 6. Write ACSL and run WP. Above the function, write `requires` for preconditions (`\valid(a+(0..n-1))` for array access), `assigns` for the exact write set, and `ensures` for the postcondition using `\result` and `\old(x)`. Above each loop, write `loop invariant`, `loop assigns`, and `loop variant`; WP cannot prove a loop without them. Run `frama-c -wp -wp-rte -wp-prover alt-ergo,z3 -wp-timeout 10 src.c -then -report`. `-wp-rte` adds the runtime-error guards to the obligations; `-wp-prover` lists provers in order (`-wp-list-provers` shows what is installed); `-wp-timeout` is seconds per goal (default 2). The report prints each property with its status, `[ Valid]` when proved, with the prover that closed it, and ends with a success percentage line. Done when: every property is `Valid`, or each unproved goal is named with the missing invariant or lemma. 7. Read a WP failure. `-wp-print` pretty-prints the unproved goal; the hypothesis list shows what the prover knew, and the goal shows what it could not derive. A goal that is true but unproved usually lacks a loop invariant strong enough to imply it, or an `assigns` clause too wide to preserve a fact; a goal that is false is a contract or code defect. Enable `-wp-counter-examples` to have WP ask the prover for a model of the failing goal. Done when: the goal is classified and the invariant, lemma, or code fix is applied and the goal is `Valid`. 8. Record the result. For CBMC, write the unwind bound, the checks enabled, and the data model beside each property. For Eva, write the precision and slevel with the alarm count. For WP, list the prover and timeout per property and every unproved goal or trusted annotation left in the session. Done when: every property line carries its bound or prover. ## Failure and recovery On a CBMC parse error (exit 2), check include paths and the data model flags; CBMC uses its own front end and needs the same `-I` paths and macro definitions as the build. On a run whose trace shows a `nondet_` value the harness never constrained, tighten `__CPROVER_assume` and rerun; a counterexample from an impossible input is a harness defect. On an Eva run that reports many alarms in library code, add `-main` on a narrower entry or raise precision before reading them; do not silence alarms with annotations you cannot prove. On a WP goal that times out, try a second prover through `-wp-prover` and raise `-wp-timeout` once with a written reason; then split the goal with an ACSL `assert` between the steps the prover cannot join. On Frama-C exit 1, the command line or source is invalid; on exit 4, 5, or 6, it is an internal error, so save the session with `-save` and report it with the minimal input. When a property cannot be discharged at any useful bound, report the bound reached, the tools tried, and the obligation left open; do not narrow the property. ## Output Harness and annotated source on disk; per property, the tool, version, bound or precision or prover, and verdict; for each failure, the concrete trace (CBMC), the classified alarm (Eva), or the unproved goal with its missing invariant (WP), and the fix applied; the list of every remaining assumed or unproved obligation.