SAFFIRE: type checking the OCaml/C FFI

SAFFIRE: type checking the OCaml/C FFI

[Michael Furr]

Announcing,

     SAFFIRE: Static Analysis of Foreign Function InteRfacEs

Saffire is a static analysis program that detects bugs in programs that
use the OCaml/C foreign function interface. Saffire works by performing
type inference across both OCaml and C to make sure that values are used
consistently across the language boundary. For instance, if a OCaml passes
a record to a C function, that C function should not treat the data as an
integer. Saffire also tracks what C variables point into the OCaml heap
and ensure they are always registered with CAMLparam/local before any
allocation functions are called.

Saffire is currently only a proof of concept implementation and does not
handle every corner of the OCaml grammar.  For example, polymorphic
variants and objects are not supported.  For a detailed list of what is
and what is not currently supported, please see the website below.  For a
more complete discussion on how Saffire works, you may be interested in
reading our upcoming PLDI paper (also available from the site).

Saffire is implemented as a combination of camlp4 and a CIL module and is
freely available/redistributable.  The license is the same as CIL
(standard 3-clause BSD).

http://www.cs.umd.edu/~furr/saffire/

Cheers,
-Mike