Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ANN: cil-0.0.1

  • Subject: [Frama-c-discuss] ANN: cil-0.0.1
  • From: tomahawkins at gmail.com (Tom Hawkins)
  • Date: Sun, 16 May 2010 22:55:54 -0500
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