blob: 7252ff8a480d8e5364f257e5748f5cd6e324a998 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
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
```
|
