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

[David MENTRE <dmentre@linux-france.org>]

Hello,

2013/10/15 Xavier Rival <Xavier.Rival@ens.fr>:
> 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