source:
extracted/compiler.mli
@
2743
Last change on this file since 2743 was 2743, checked in by , 7 years ago | |
---|---|
File size: 3.0 KB |
Line | |
---|---|
1 | open Preamble |
2 | |
3 | open BitVectorTrie |
4 | |
5 | open CostLabel |
6 | |
7 | open Coqlib |
8 | |
9 | open Proper |
10 | |
11 | open PositiveMap |
12 | |
13 | open Deqsets |
14 | |
15 | open ErrorMessages |
16 | |
17 | open PreIdentifiers |
18 | |
19 | open Errors |
20 | |
21 | open Extralib |
22 | |
23 | open Setoids |
24 | |
25 | open Monad |
26 | |
27 | open Option |
28 | |
29 | open Lists |
30 | |
31 | open Positive |
32 | |
33 | open Identifiers |
34 | |
35 | open Exp |
36 | |
37 | open Arithmetic |
38 | |
39 | open Vector |
40 | |
41 | open Div_and_mod |
42 | |
43 | open Jmeq |
44 | |
45 | open Russell |
46 | |
47 | open List |
48 | |
49 | open Util |
50 | |
51 | open FoldStuff |
52 | |
53 | open BitVector |
54 | |
55 | open Extranat |
56 | |
57 | open Bool |
58 | |
59 | open Relations |
60 | |
61 | open Nat |
62 | |
63 | open Integers |
64 | |
65 | open Hints_declaration |
66 | |
67 | open Core_notation |
68 | |
69 | open Pts |
70 | |
71 | open Logic |
72 | |
73 | open Types |
74 | |
75 | open AST |
76 | |
77 | open Csyntax |
78 | |
79 | open Label |
80 | |
81 | open Sets |
82 | |
83 | open Listb |
84 | |
85 | open Star |
86 | |
87 | open Frontend_misc |
88 | |
89 | open CexecInd |
90 | |
91 | open CexecSound |
92 | |
93 | open Casts |
94 | |
95 | open ClassifyOp |
96 | |
97 | open Smallstep |
98 | |
99 | open Extra_bool |
100 | |
101 | open FrontEndVal |
102 | |
103 | open Hide |
104 | |
105 | open ByteValues |
106 | |
107 | open GenMem |
108 | |
109 | open FrontEndMem |
110 | |
111 | open Globalenvs |
112 | |
113 | open Csem |
114 | |
115 | open SmallstepExec |
116 | |
117 | open Division |
118 | |
119 | open Z |
120 | |
121 | open BitVectorZ |
122 | |
123 | open Pointers |
124 | |
125 | open Values |
126 | |
127 | open Events |
128 | |
129 | open IOMonad |
130 | |
131 | open IO |
132 | |
133 | open Cexec |
134 | |
135 | open TypeComparison |
136 | |
137 | open SimplifyCasts |
138 | |
139 | open MemProperties |
140 | |
141 | open MemoryInjections |
142 | |
143 | open Fresh |
144 | |
145 | open SwitchRemoval |
146 | |
147 | open FrontEndOps |
148 | |
149 | open Cminor_syntax |
150 | |
151 | open ToCminor |
152 | |
153 | open Initialisation |
154 | |
155 | open Graphs |
156 | |
157 | open Order |
158 | |
159 | open Registers |
160 | |
161 | open RTLabs_syntax |
162 | |
163 | open ToRTLabs |
164 | |
165 | open Deqsets_extra |
166 | |
167 | open CostMisc |
168 | |
169 | open Listb_extra |
170 | |
171 | open CostSpec |
172 | |
173 | open CostCheck |
174 | |
175 | open Executions |
176 | |
177 | open StructuredTraces |
178 | |
179 | open RTLabs_semantics |
180 | |
181 | open RTLabs_abstract |
182 | |
183 | open RTLabs_traces |
184 | |
185 | open CostInj |
186 | |
187 | val front_end : |
188 | Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program) |
189 | Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res |
190 | |
191 | open State |
192 | |
193 | open Bind_new |
194 | |
195 | open BindLists |
196 | |
197 | open Blocks |
198 | |
199 | open TranslateUtils |
200 | |
201 | open AssocList |
202 | |
203 | open String |
204 | |
205 | open LabelledObjects |
206 | |
207 | open I8051 |
208 | |
209 | open BackEndOps |
210 | |
211 | open Joint |
212 | |
213 | open RTL |
214 | |
215 | open RTLabsToRTL |
216 | |
217 | open ERTL |
218 | |
219 | open RegisterSet |
220 | |
221 | open RTLToERTL |
222 | |
223 | open ERTLptr |
224 | |
225 | open ERTLToERTLptr |
226 | |
227 | open Fixpoints |
228 | |
229 | open Set_adt |
230 | |
231 | open Liveness |
232 | |
233 | open Interference |
234 | |
235 | open Joint_LTL_LIN |
236 | |
237 | open LTL |
238 | |
239 | open ERTLptrToLTL |
240 | |
241 | open LIN |
242 | |
243 | open Linearise |
244 | |
245 | open LTLToLIN |
246 | |
247 | open ASM |
248 | |
249 | open BitVectorTrieSet |
250 | |
251 | open LINToASM |
252 | |
253 | val compute_fixpoint : Fixpoints.fixpoint_computer |
254 | |
255 | val colour_graph : Interference.coloured_graph_computer |
256 | |
257 | val back_end : RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program |
258 | |
259 | type object_code = BitVector.byte List.list |
260 | |
261 | type costlabel_map1 = CostLabel.costlabel BitVectorTrie.bitVectorTrie |
262 | |
263 | open Assembly |
264 | |
265 | open Status |
266 | |
267 | open Fetch |
268 | |
269 | open PolicyFront |
270 | |
271 | open PolicyStep |
272 | |
273 | open Policy |
274 | |
275 | val assembler : |
276 | ASM.pseudo_assembly_program -> (object_code, costlabel_map1) Types.prod |
277 | Errors.res |
278 | |
279 | open AbstractStatus |
280 | |
281 | open StatusProofs |
282 | |
283 | open Interpret |
284 | |
285 | open ASMCosts |
286 | |
287 | val lift_cost_map_back_to_front : |
288 | Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie -> |
289 | CostLabel.costlabel BitVectorTrie.bitVectorTrie -> (CostLabel.costlabel -> |
290 | (__, __) Types.sum) -> StructuredTraces.as_cost_map -> |
291 | Label.clight_cost_map |
292 | |
293 | open UtilBranch |
294 | |
295 | open ASMCostsSplit |
296 | |
297 | val compile : |
298 | Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod, |
299 | (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod |
300 | Errors.res |
301 |
Note: See TracBrowser
for help on using the repository browser.