From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 2A7C0BCAB for ; Tue, 31 May 2005 03:30:32 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j4V1UVlX025020 for ; Tue, 31 May 2005 03:30:31 +0200 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id DAA08044 for ; Tue, 31 May 2005 03:30:31 +0200 (MET DST) Received: from junkmail.cs.umd.edu (junkmail.cs.umd.edu [128.8.128.69]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j4V1UThl002208 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Tue, 31 May 2005 03:30:31 +0200 Received: from toblerone.cs.umd.edu (toblerone.cs.umd.edu [128.8.129.39]) by junkmail.cs.umd.edu (8.12.10/8.12.5) with ESMTP id j4V1UPTs001351 for ; Mon, 30 May 2005 21:30:27 -0400 (EDT) Received: from localhost (localhost [127.0.0.1]) by toblerone.cs.umd.edu (8.12.10/8.12.5) with ESMTP id j4V1UOnu016551 for ; Mon, 30 May 2005 21:30:24 -0400 (EDT) Date: Mon, 30 May 2005 21:30:24 -0400 (EDT) From: Michael Furr To: Subject: SAFFIRE: type checking the OCaml/C FFI Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Miltered: at concorde with ID 429BBE37.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 429BBE35.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; ocaml:01 ffi:01 ocaml:01 inference:01 heap:01 camlparam:01 grammar:01 variants:01 pldi:01 cheers:01 -mike:01 polymorphic:01 integer:01 interfaces:01 functions:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: 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