From b8ebdff476c716ec521d9771bf79b5ed1fd6b778 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 22 Sep 2021 15:54:09 +0200 Subject: Update export/README.md --- export/README.md | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'export') 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 search for include files - -D define preprocessor macro - -U undefine preprocessor macro - -Wp, pass options to C preprocessor - -f 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). -- cgit