diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-16 11:03:40 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-22 16:00:31 +0200 |
commit | d32955030937937706b71a96dc6584800f0b8722 (patch) | |
tree | d82b440a150f3339715d9f0a208966ee66219a65 /export/README.md | |
parent | 9e30fa95607cf357ab7c18a4773edf6b6f84c7d7 (diff) | |
download | compcert-kvx-d32955030937937706b71a96dc6584800f0b8722.tar.gz compcert-kvx-d32955030937937706b71a96dc6584800f0b8722.zip |
Refactor clightgen
Split reusable parts of ExportClight.ml off, into
ExportBase.ml and ExportCtypes.ml.
Rename exportclight/ directory to export/
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..85e0790b --- /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, 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 +``` |