Abstract interpretation provides advanced techniques to infer numerical invariants on programs. There is an abundant literature about numerical abstract domains that operate on scalar variables. This work deals with lifting these techniques to a realistic C memory model. We present an abstract memory functor that takes as argument any standard numerical abstract domain, and builds a memory abstract domain that finely tracks properties about memory contents, taking into account union types, pointer arithmetic and type casts. This functor is implemented and verified inside the Coq proof assistant with respect to the CompCert compiler memory model. Using the Coq extraction mechanism, it is fully executable and used by the Verasco C static analyzer..
This work was accepted to ICFP 2016. A draft of the paper can be found here.
The development has been made with Coq 8.4 and OCaml 4.01. The sources are available here.
Note: the sources contain a modified version of CompCert 1.11 ported to Coq 8.4 with the CFG intermediate language (apply the patch `compcert-1.11-cfg.diff` from this directory). It also depends on the Containers library from contribs.
This also extracts an OCaml program and compile it. This last compilation expects he `cc` directory to contain the sources of CompCert.