aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight/README.md
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2021-09-16 11:03:40 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2021-09-22 16:00:31 +0200
commitd32955030937937706b71a96dc6584800f0b8722 (patch)
treed82b440a150f3339715d9f0a208966ee66219a65 /exportclight/README.md
parent9e30fa95607cf357ab7c18a4773edf6b6f84c7d7 (diff)
downloadcompcert-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 'exportclight/README.md')
-rw-r--r--exportclight/README.md33
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
-```