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 9AA517EE4B; Tue, 15 Oct 2013 15:02:54 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of david.mentre@gmail.com) identity=pra; client-ip=209.85.215.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="david.mentre@gmail.com"; x-sender="david.mentre@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of david.mentre@gmail.com designates 209.85.215.48 as permitted sender) identity=mailfrom; client-ip=209.85.215.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="david.mentre@gmail.com"; x-sender="david.mentre@gmail.com"; 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@mail-la0-f48.google.com) identity=helo; client-ip=209.85.215.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="david.mentre@gmail.com"; x-sender="postmaster@mail-la0-f48.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgkDACQ8XVLRVdcwlGdsb2JhbABagz9SgynAEggWDgEBAQEHCwsJEiqCJgEFIx0BMgYBAwwBBQULDwImAgIfAxIBBQEcBhOHdAMPDJ59jAKDXYRFJw2JZQEFDIEdkRKBOwOOUIk0gS+OaBgpgWOBLYFAOg X-IPAS-Result: AgkDACQ8XVLRVdcwlGdsb2JhbABagz9SgynAEggWDgEBAQEHCwsJEiqCJgEFIx0BMgYBAwwBBQULDwImAgIfAxIBBQEcBhOHdAMPDJ59jAKDXYRFJw2JZQEFDIEdkRKBOwOOUIk0gS+OaBgpgWOBLYFAOg X-IronPort-AV: E=Sophos;i="4.93,498,1378850400"; d="scan'208";a="30431301" Received: from mail-la0-f48.google.com ([209.85.215.48]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 15 Oct 2013 15:02:54 +0200 Received: by mail-la0-f48.google.com with SMTP id er20so6675962lab.7 for ; Tue, 15 Oct 2013 06:02:53 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc:content-type; bh=22HhmbywepdTPqp3+hh4IllcRdL+x6hooViqOx9oCrM=; b=oDFcP2Pz/19JRQXDQDTSjm1YLSPiVPVio3Wq0lhRIhEsd6kiqM/4JNTkixzQMqlE5u /j57KBjSj+Bz29ATqfG1yj3DDwoQfVGJpFF8anbM7NzfjFNZpOK0i8dhNYEHnOKYUule 6v9w96tv7ihzKAuqWdwscQkrF22gTI289nEWUbmB7yp8zwZj1hB+ZWOS0ZsdHJbGHkNp GDCvALHJslylXTK9DLcz2GwFFiSL8IJyMrGMwUvGEKQvm632pE827m8hQb9oUq49X2b1 u2SdlUgTUr6gbevDMOC8PCYPOPXKyWpQNiMV2TTCFiNmAF8sMGXEplh5zdNEGymxdi3R NaSA== X-Received: by 10.112.146.200 with SMTP id te8mr6670479lbb.32.1381842173298; Tue, 15 Oct 2013 06:02:53 -0700 (PDT) MIME-Version: 1.0 Sender: david.mentre@gmail.com Received: by 10.112.45.108 with HTTP; Tue, 15 Oct 2013 06:02:23 -0700 (PDT) In-Reply-To: References: <20131015124116.GA7090@kerneis.info> From: David MENTRE Date: Tue, 15 Oct 2013 15:02:23 +0200 X-Google-Sender-Auth: Oqs0wCGaiobmO54CcLKRIy7vL4k Message-ID: To: Xavier Rival Cc: Gabriel Kerneis , caml users , ocaml-jobs@inria.fr Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml Hello, 2013/10/15 Xavier Rival : > 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. In that case, why don't you extend CIL to fix its deficiencies? It would help other projects using CIL like Frama-C. In the same way, why do you implement your own C parsing infrastructure and do not build a Frama-C plug-in for your analysis? Frama-C has already a user base (industrial and academic), if you can improve it it would help a lot. And it would allow to combine your analysis with other Frama-C plug-ins. Last but not least, you say "We plan to release source code of the analyzer along the course of the project." Which kind of licence do you plan to use?[1] Sincerely yours, david [1] I am maintaining this directory: http://gulliver.eu.org/free_software_for_formal_verification