diff options
Diffstat (limited to 'export/README.md')
| -rw-r--r-- | export/README.md | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/export/README.md b/export/README.md new file mode 100644 index 00000000..9b5d5b35 --- /dev/null +++ b/export/README.md @@ -0,0 +1,33 @@ +# The clightgen tool + +## Overview + +`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 + +Configure CompCert with `./configure -clightgen`. + +Build CompCert as usual. + +The `clightgen` tool will be installed in the same directory as the +`ccomp` compiler. + +## Usage +``` + clightgen [options] <C source files> +``` +For each source file `src.c`, its Clight abstract syntax is generated +in `src.v`. + +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). |