source: extracted/compiler.mli @ 2743

Last change on this file since 2743 was 2743, checked in by sacerdot, 7 years ago

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