Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml

[Julia Lawall <julia.lawall@lip6.fr>]

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