diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-22 15:54:09 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-22 16:06:44 +0200 |
commit | b8ebdff476c716ec521d9771bf79b5ed1fd6b778 (patch) | |
tree | 27ce2483f286e13b8fb6b1d629e6df537b6b6d4b /export/README.md | |
parent | dffc9885e54f9c68af23ec79023dfe8516a4cc32 (diff) | |
download | compcert-b8ebdff476c716ec521d9771bf79b5ed1fd6b778.tar.gz compcert-b8ebdff476c716ec521d9771bf79b5ed1fd6b778.zip |
Update export/README.md
Diffstat (limited to 'export/README.md')
-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). |