[Haskell-cafe] ANN: cil-0.0.1

[Tom Hawkins]

CIL [1] is an OCaml library that parses and compiles C down to a
simplified subset to ease different forms of static analysis.  Frama-C
[2] augments CIL with a property specification language (ACSL), which
can capture design contracts for C functions.  Frama-C's Jessie plugin
uses the Why [3] software verification platform, which itself uses
several different SMT solvers and proof assistances to verify ACSL
function contracts -- a very cool platform, I encourage anyone
interested in the verification of C programs to check it out.

This Hackage library [4] is an interface to the Frama-C environment.
Specifically, it provides equivalent CIL and ACSL data types, allowing
CIL and ACSL based analyzers to be written in Haskell.

The library installs a Frama-C/OCaml plugin, which dumps the CIL
database into Haskell.  Internally, both the OCaml and Haskell sides
of the interface are generated by a script (GenCIL.hs) that parses the
contents of the CIL type definitions (cil_types.mli).

Currently it only works for the most basic C programs.  A bug in
either the generated OCaml plugin or Frama-C causes issues [5].

-Tom


[1] http://cil.sourceforge.net/
[2] http://frama-c.com/
[3] http://why.lri.fr/
[4] http://hackage.haskell.org/package/cil
[5] http://bts.frama-c.com/view.php?id=481