diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-05 09:59:26 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-05 09:59:26 +0000 |
commit | 578cc2a54897e0c89425a56df7a173bebeee2382 (patch) | |
tree | 1ccb034fd4beebe618d4fad81abc5214677d8010 /exportclight/README | |
parent | ba8ad207029d3121d602a23aeeedd55b4dfd192a (diff) | |
download | compcert-kvx-578cc2a54897e0c89425a56df7a173bebeee2382.tar.gz compcert-kvx-578cc2a54897e0c89425a56df7a173bebeee2382.zip |
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
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 + |