diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-01-10 10:32:43 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-01-10 10:32:43 +0100 |
| commit | 5df29e2caa1ec95a3ddbcaf49d686998b0696855 (patch) | |
| tree | 84d4a091b0951e9d0d8e57a80ed3e943eddfea90 /exportclight | |
| parent | d270d2e104fd81248c1020347bb63dad046e232f (diff) | |
| download | compcert-kvx-5df29e2caa1ec95a3ddbcaf49d686998b0696855.tar.gz compcert-kvx-5df29e2caa1ec95a3ddbcaf49d686998b0696855.zip | |
Change README to markdown.
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/README.md (renamed from exportclight/README) | 29 |
1 files changed, 14 insertions, 15 deletions
diff --git a/exportclight/README b/exportclight/README.md index 3fd8c0ae..7252ff8a 100644 --- a/exportclight/README +++ b/exportclight/README.md @@ -1,34 +1,33 @@ - The clightgen tool - ------------------ +# The clightgen tool -OVERVIEW +## 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 +## How to build Change to the top-level CompCert directory and issue - - make clightgen - - -USAGE - - clightgen [options] <C source files> - +``` + 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 http://compcert.inria.fr/man/manual003.html for full documentation): - +(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 - +``` |