From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.3 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id C6903BBAF for ; Mon, 26 May 2008 18:27:49 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlAAACuCOkiBaB4io2dsb2JhbACSOgEBAQEBCAUIBxGZPA X-IronPort-AV: E=Sophos;i="4.27,543,1204498800"; d="scan'208";a="26621035" Received: from mx1.polytechnique.org ([129.104.30.34]) by mail4-smtp-sop.national.inria.fr with ESMTP; 26 May 2008 18:27:47 +0200 Received: from is005115 (is005115.intra.cea.fr [132.166.135.75]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by ssl.polytechnique.org (Postfix) with ESMTP id 47A2533170; Mon, 26 May 2008 18:27:46 +0200 (CEST) Date: Mon, 26 May 2008 18:25:53 +0200 From: Virgile Prevosto To: Caml list , coq-club@pauillac.inria.fr, why-discuss@lists.gforge.inria.fr, frama-c-discuss@lists.gforge.inria.fr, espass-admin-members@lists.gforge.enseeiht.fr, Focal Subject: Introducing Frama-C Message-ID: <20080526182553.5d275e0f@is005115> X-Mailer: Claws Mail 3.3.1 (GTK+ 2.12.9; i486-pc-linux-gnu) Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-AV-Checked: ClamAV using ClamSMTP at djali.polytechnique.org (Mon May 26 18:27:46 2008 +0200 (CEST)) X-Org-Mail: virgile.prevosto.1996@polytechnique.org X-Spam: no; 0.00; ocaml:01 cuoq:01 analyzers:98 analyzers:98 plug-in:98 plug-in:98 cea:01 binary:02 variables:02 static:03 library:03 forthcoming:05 intermediate:05 computing:05 variation:06 Greetings. The Frama-C development team is proud to announce the availability of Frama-C, the framework for the development of collaborating static analyzers for the C language. Many analyzers are provided in the distribution, including a value analysis plug-in that provides variation domains for the variables of the program, and Jessie, a plug-in for computing Hoare style weakest preconditions. Frama-C is Open Source software. It is written in Ocaml and relies on the CIL (C Intermediate Language) library. Additional information, source code and documentation for Frama-C are available now at http://frama-c.cea.fr/. Binary distributions for various popular environments will be forthcoming. For the Frama-C development team, -- Pascal Cuoq and Virgile Prevosto