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
- Prev by Date: [Frama-c-discuss] question about a simple example and jessie
- Next by Date: [Frama-c-discuss] Small function on buffer doesn't verify
- Previous by thread: [Frama-c-discuss] Jessie plugin
- Next by thread: [Frama-c-discuss] Feedback on presenting Formal Methods
- Index(es):