From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 8D0497EE4C; Tue, 15 Oct 2013 14:52:23 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.93,498,1378850400"; d="scan'208";a="37121643" Received: from vaio-julia.rsr.lip6.fr ([132.227.76.33]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 15 Oct 2013 14:52:22 +0200 Date: Tue, 15 Oct 2013 14:52:19 +0200 (CEST) From: Julia Lawall X-X-Sender: jll@hadrien To: Xavier Rival cc: Gabriel Kerneis , caml-list@inria.fr, ocaml-jobs@inria.fr In-Reply-To: Message-ID: References: <20131015124116.GA7090@kerneis.info> User-Agent: Alpine 2.02 (DEB 1266 2009-07-14) MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Validation-by: julia.lawall@lip6.fr Subject: Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml On Tue, 15 Oct 2013, Xavier Rival wrote: > On Tue, 15 Oct 2013, Gabriel Kerneis wrote: > > > On Tue, Oct 15, 2013 at 02:31:17PM +0200, Xavier Rival wrote: > > > The task that will be undertaken consists in developping front-end > > > components for the MemCAD static analyzer, including a C front-end, > > > syntax tree simplification, and possibly pre-analyses to be used in > > > the MemCAD tool (the goal of this tool is to infer program > > > invariants for codes manipulating complex memory data-structures). > > > The components that shall be designed as part of this effort have > > > the potential to be used by other research groups in the static > > > analysis area. > > > > Out of curiosity, why don't CIL or Frama-C suit your needs? > > I have used CIL in another project in the past. My experience is that it is a > great front-end for program transformation. It is less adapted to static > analysis though, as it does a lot of syntactic transformations, causing part > of the structure of the code to be lost. For instance, it transforms loops > into a while(1) form, with break statements. This design choice does not help > static analyzers, and may require recalculating information that was lost in > the early phases. I would have thought that all of those would be the same things that make it not good for program transformation. At least not if you want to look at the transformed code. It could be OK for something like weaving aspects, where you just want to execute the code, and want to advise the parts that are not broken by the simplifications. I have the impression that Frama-C does similar reorganizations. julia