From: Mark Kattenbelt <M.K<attenbelt@cs...> - 2007-01-10 10:45:00
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!
University of Birmingham
From: Benjamin Ylvisaker <benjaminy@fa...> - 2007-01-11 23:57:45
I am interested in using Cil to do a project that involves program
slicing (see http://www.cs.wisc.edu/wpis/html/ for info on slicing).
I thought that astslicer.ml might be a good place to start, but I am
having some trouble understanding exactly what that file does. Is
there any more information about this file available?