Unverified Commit 5df29e2c authored by Bernhard Schommer's avatar Bernhard Schommer
Browse files

Change README to markdown.

parent d270d2e1
The clightgen tool
# 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
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
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment