The clightgen tool
                        ------------------

OVERVIEW

"clightgen" is an experimental tool that transforms C source files
into Clight abstract syntax, pretty-printed in Coq format in .v files.
These generated .v files can be loaded in a Coq session for
interactive verification, typically.


HOW TO BUILD

Change to the top-level CompCert directory and issue

          make clightgen


USAGE

        clightgen [options] <C source files>

For each source file "src.c", its Clight abstract syntax is generated
in "src.v".

The options recognized are a subset of those of the CompCert compiler ccomp
(see http://compcert.inria.fr/man/manual003.html for full documentation):

   -I<dir>     search <dir> for include files
   -D<symbol>  define preprocessor macro
   -U<symbol>  undefine preprocessor macro
   -Wp,<opts>  pass options to C preprocessor
   -f<feature> activate emulation of the given C feature