Verified Value Analysis for CompCert
A companion web page

Verified Value Analysis for CompCert is built on top of the C CompCert verified compiler. The value analysis operates on the CFG intermediate representation and outputs a correct interval of possible values for each program variable, at each program point.

Page last updated on: 2013-03-29


This work has been accepted at the 20th Static Analysis Symposium (SAS 2013). You can access it here.

Coq Development

Download the last stable version of the Coq development: [value-analysis.tgz]
(tested with OCaml 4.00 and Coq 8.3pl5)

Download a virtual machine image of the development: []
This VirtualBox VM contains a Debian Linux with precompiled binaries of our development (and the contents of the .tgz archive).
Note: after decompression it requires around 1.5 GB of disk space.
On some machines we experienced some issues with VirtualBox that were resolved by re-adding/re-running the machine. Should you experience any issues, please contact us to help resolve it.

Installation instructions

Note: You need OCaml (3.12 or 4.00) and Coq 8.3 (up to 8.3pl5, but not 8.4) installed on your machine.
The provided archive is already bundled with CompCert 1.11.
  1. Download and extract the archive (tar xvf value-analysis.tgz).
  2. Inside the value-analysis directory, run make proof to Coq-prove the analysis and the CompCert C compiler (this can take several minutes; adding flag -j<N> for parallel processing can speed it up, but will require more memory).
  3. Run make extraction cfgcomp to extract and compile the Coq code. This will produce a binary executable cfgcomp that accepts some extra command-line options specific to the value analysis.
  4. Go to the annotated-benchs directory and run ./ <file.c> to analyze a single file, or ./ to run the analysis on all files. In both cases, each analyzed source produces a <file>.value.cfg file containing the program's CFG representation annotated with the result of the analysis.
    Note: to run, Python must be installed on the machine.

Afterwards, you can run cfgcomp <file> on a specific C program to analyze it.

Additional information

Browsable version of the Coq development

The documentation gives a commented listing of the underlying Coq specifications and proofs. Proof scripts are folded by default, but can be viewed by clicking on "Proof".

CFG Language

Value analysis

Utilities and common code

CompCert original files