Bounded Model Checking C

Bounded model checking C

Contract

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.