blob: 3fd8c0aef6fcf615e9ff987bef9c0c162a575597 (
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
34
|
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 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
|
