Version française
Home     About     Download     Resources     Contact us    
Browse thread
SAFFIRE: type checking the OCaml/C FFI
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Michael Furr <furr@c...>
Subject: SAFFIRE: type checking the OCaml/C FFI

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