From 5df29e2caa1ec95a3ddbcaf49d686998b0696855 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 10 Jan 2018 10:32:43 +0100
Subject: Change README to markdown.

---
 exportclight/README.md | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 exportclight/README.md

(limited to 'exportclight/README.md')

diff --git a/exportclight/README.md b/exportclight/README.md
new file mode 100644
index 00000000..7252ff8a
--- /dev/null
+++ b/exportclight/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
+```
-- 
cgit