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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 518127EE4B; Tue, 15 Oct 2013 14:48:51 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of Xavier.Rival@ens.fr) identity=pra; client-ip=129.199.96.40; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="Xavier.Rival@ens.fr"; x-sender="Xavier.Rival@ens.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of Xavier.Rival@ens.fr designates 129.199.96.40 as permitted sender) identity=mailfrom; client-ip=129.199.96.40; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="Xavier.Rival@ens.fr"; x-sender="Xavier.Rival@ens.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@nef2.ens.fr) identity=helo; client-ip=129.199.96.40; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="Xavier.Rival@ens.fr"; x-sender="postmaster@nef2.ens.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AugBAGE4XVKBx2AonGdsb2JhbABaxjKBIhYOAQEBAQEICwkJFCiCJQEBBAE4AhkmBQsLGC5XBogTBr1Wj0oHhCUDq2yBQA X-IPAS-Result: AugBAGE4XVKBx2AonGdsb2JhbABaxjKBIhYOAQEBAQEICwkJFCiCJQEBBAE4AhkmBQsLGC5XBogTBr1Wj0oHhCUDq2yBQA X-IronPort-AV: E=Sophos;i="4.93,498,1378850400"; d="scan'208";a="30429004" Received: from nef2.ens.fr ([129.199.96.40]) by mail3-smtp-sop.national.inria.fr with ESMTP; 15 Oct 2013 14:48:50 +0200 Received: from di.ens.fr (di.ens.fr [129.199.99.1]) by nef2.ens.fr (8.13.6/1.01.28121999) with ESMTP id r9FCmoZf072366 ; Tue, 15 Oct 2013 14:48:50 +0200 (CEST) X-Envelope-To: ocaml-jobs@inria.fr Received: from ssh-di.ens.fr (ssh.di.ens.fr [129.199.99.31]) by di.ens.fr (8.13.6/jb-1.1) id r9FCmnoi027493 ; Tue, 15 Oct 2013 14:48:49 +0200 Received: from localhost (rival@localhost) by ssh-di.ens.fr (8.14.4/jb-1.1) id r9FCmnJP004096 ; Tue, 15 Oct 2013 14:48:49 +0200 X-Authentication-Warning: ssh-di.ens.fr: rival owned process doing -bs Date: Tue, 15 Oct 2013 14:48:49 +0200 (CEST) From: Xavier Rival X-X-Sender: rival@ssh-di.ens.fr To: Gabriel Kerneis cc: caml-list@inria.fr, ocaml-jobs@inria.fr In-Reply-To: <20131015124116.GA7090@kerneis.info> 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; format=flowed X-Virus-Scanned: by amavisd-milter (http://amavis.org/) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-3.1.4 (nef2.ens.fr [129.199.96.32]); Tue, 15 Oct 2013 14:48:50 +0200 (CEST) X-Validation-by: xavier.rival@ens.fr Subject: Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml 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. Best Regards, Xavier.