-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcompcert.driver.Compopts.html
123 lines (94 loc) · 7.94 KB
/
compcert.driver.Compopts.html
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>compcert.driver.Compopts</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library compcert.driver.Compopts</h1>
<div class="code">
<br/>
</div>
<div class="doc">
Compilation options
<div class="paragraph"> </div>
This file collects Coq functions to query the command-line
options that influence the code generated by the verified
part of CompCert. These functions are mapped by extraction
to accessors for the flags in <span class="inlinecode"><span class="id" title="var">Clflags.ml</span></span>.
<div class="paragraph"> </div>
Flag <span class="inlinecode">-<span class="id" title="var">Os</span></span>. For instruction selection (mainly).
</div>
<div class="code">
<span class="id" title="keyword">Parameter</span> <a name="optim_for_size"><span class="id" title="axiom">optim_for_size</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
</div>
<div class="doc">
Flag <span class="inlinecode">-<span class="id" title="var">ffloat</span>-<span class="id" title="var">const</span>-<span class="id" title="var">prop</span></span>. For value analysis and constant propagation.
</div>
<div class="code">
<span class="id" title="keyword">Parameter</span> <a name="propagate_float_constants"><span class="id" title="axiom">propagate_float_constants</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<span class="id" title="keyword">Parameter</span> <a name="generate_float_constants"><span class="id" title="axiom">generate_float_constants</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
</div>
<div class="doc">
For value analysis. Currently always false.
</div>
<div class="code">
<span class="id" title="keyword">Parameter</span> <a name="va_strict"><span class="id" title="axiom">va_strict</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
</div>
<div class="doc">
Flag -ftailcalls. For tail call optimization.
</div>
<div class="code">
<span class="id" title="keyword">Parameter</span> <a name="optim_tailcalls"><span class="id" title="axiom">optim_tailcalls</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
</div>
<div class="doc">
Flag -fconstprop. For constant propagation.
</div>
<div class="code">
<span class="id" title="keyword">Parameter</span> <a name="optim_constprop"><span class="id" title="axiom">optim_constprop</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
</div>
<div class="doc">
Flag -fcse. For common subexpression elimination.
</div>
<div class="code">
<span class="id" title="keyword">Parameter</span> <a name="optim_CSE"><span class="id" title="axiom">optim_CSE</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
</div>
<div class="doc">
Flag -fredundancy. For dead code elimination.
</div>
<div class="code">
<span class="id" title="keyword">Parameter</span> <a name="optim_redundancy"><span class="id" title="axiom">optim_redundancy</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
</div>
<div class="doc">
Flag -fthumb. For the ARM back-end.
</div>
<div class="code">
<span class="id" title="keyword">Parameter</span> <a name="thumb"><span class="id" title="axiom">thumb</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
</div>
<div class="doc">
Flag -g. For insertion of debugging information.
</div>
<div class="code">
<span class="id" title="keyword">Parameter</span> <a name="debug"><span class="id" title="axiom">debug</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
</div>
</div>
<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>