diff options
Diffstat (limited to 'exportclight/README')
-rw-r--r-- | exportclight/README | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/exportclight/README b/exportclight/README new file mode 100644 index 00000000..3fd8c0ae --- /dev/null +++ b/exportclight/README @@ -0,0 +1,34 @@ + 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 + |