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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
