[CIL users] Some CIL questions

[Mark K. <M.K...@cs...>]

Hi there,

I am considering the use of CIL for our project (regarding automatic 
verification of c programs). I am mostly interested in the way in which 
CIL can handle large c programs and produce a much simpler 
representation in CIL that is semanticly equivalent, but with much 
simpler (and unambiguous) syntax. I have looked at CIL for a little 
while and I have some general questions:

- I quote from the documentation: `We plan to release a C-language 
interface to CIL so that you can write your analyses in C instead of 
Ocaml'. I would be very interested in such an interface. Is there any 
provisional version out there that I could have a look at? When do you 
expect this release?
I am not so much interested in being able to transform the AST in c, as 
I could always write this transformation in Ocaml should I need to. 
However, the most likely implementation language of our tool would be c, 
and should we use CIL, it would be very useful if there exists a binding 
such that we can extract the parsed and transformed AST in a simple fashion.

- It seems that "--save-temps" is the only way to retrieve the *.cil.c 
file. This also produces the object files. If I only want to execute the 
first phase of the compilation process (i.e. producing a CIL 
representation, possibly with some transformations) is this possible?

- I am new to Ocaml, but not to functional programming. Besides 
tutorials on ocaml, what do you recommend to read if I want to get 
started writing a module for CIL. For instance, do you have a dummy 
module (besides logwrites), that simply ouputs the AST node when 
visited, but doesn't do much else?

Thank you for any help!

Kind regards,

Mark Kattenbelt
University of Birmingham