/bounded-model-checking-c

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.'
disable-model-invocation: true

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-