Put clighgen files in exportclight/

Short doc in exportclight/README



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2089 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 34 insertions, 0 deletions

diff --git a/exportclight/README b/exportclight/README
new file mode 100644
index 0000000..3fd8c0a
--- /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
+