Browse thread
SAFFIRE: type checking the OCaml/C FFI
- Michael Furr
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ 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 |
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