diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-09-30 13:23:42 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-09-30 13:23:42 +0200 |
| commit | ef508dae3e880bdd30e9d57ca2a8b3e257b1203b (patch) | |
| tree | 0cb08c27aeef48ca154525378419f5b129793b2b /exportclight/README.md | |
| parent | dbada6c41e51a03848b14260576ba825c3102313 (diff) | |
| parent | 539b81a1a8823fb4aac64a9493bf0bafea2f2560 (diff) | |
| download | compcert-kvx-ef508dae3e880bdd30e9d57ca2a8b3e257b1203b.tar.gz compcert-kvx-ef508dae3e880bdd30e9d57ca2a8b3e257b1203b.zip | |
Merge branch 'towards_2.10' of ../towards_3.10 into kvx-work
Diffstat (limited to 'exportclight/README.md')
| -rw-r--r-- | exportclight/README.md | 33 |
1 files changed, 0 insertions, 33 deletions
diff --git a/exportclight/README.md b/exportclight/README.md deleted file mode 100644 index 85e0790b..00000000 --- a/exportclight/README.md +++ /dev/null @@ -1,33 +0,0 @@ -# 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 [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 -``` |