diff options
-rw-r--r-- | export/README.md | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/export/README.md b/export/README.md index 85e0790b..9b5d5b35 100644 --- a/export/README.md +++ b/export/README.md @@ -1,19 +1,23 @@ # 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. +`clightgen` is an experimental tool that transforms C source files +into Clight abstract syntax or Csyntax abstract syntax, pretty-printed +in Coq format inside `.v` files. + +These generated `.v` files can be loaded in a Coq session for +interactive verification, for example using the +[VST](https://vst.cs.princeton.edu/) toolchain. ## How to build -Change to the top-level CompCert directory and issue -``` - make clightgen -``` +Configure CompCert with `./configure -clightgen`. + +Build CompCert as usual. + +The `clightgen` tool will be installed in the same directory as the +`ccomp` compiler. ## Usage ``` @@ -22,12 +26,8 @@ Change to the top-level CompCert directory and issue 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 [user's manual](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 -``` +Run `clightgen -help` for a list of options. + +Several options are shared with the `ccomp` compiler; +see [user's manual](http://compcert.inria.fr/man/manual003.html) +for full documentation). |