English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

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: 2005-05-31 (01:30)
From: Michael Furr <furr@c...>
Subject: SAFFIRE: type checking the OCaml/C FFI


     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).