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

[Xavier Rival <Xavier.Rival@ens.fr>]

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.