source: extracted/semantics.mli @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 5.0 KB
Line 
1open Preamble
2
3open UtilBranch
4
5open ASMCostsSplit
6
7open StructuredTraces
8
9open AbstractStatus
10
11open StatusProofs
12
13open Interpret
14
15open ASMCosts
16
17open Assembly
18
19open Status
20
21open Fetch
22
23open PolicyFront
24
25open PolicyStep
26
27open Policy
28
29open AssocList
30
31open Uses
32
33open ASM
34
35open BitVectorTrieSet
36
37open LINToASM
38
39open LIN
40
41open Linearise
42
43open LTLToLIN
44
45open Fixpoints
46
47open Set_adt
48
49open Liveness
50
51open Interference
52
53open Joint_LTL_LIN
54
55open LTL
56
57open ERTLptrToLTL
58
59open ERTLptr
60
61open ERTLToERTLptr
62
63open ERTL
64
65open RegisterSet
66
67open RTLToERTL
68
69open State
70
71open Bind_new
72
73open BindLists
74
75open Blocks
76
77open TranslateUtils
78
79open String
80
81open LabelledObjects
82
83open I8051
84
85open BackEndOps
86
87open Joint
88
89open RTL
90
91open RTLabsToRTL
92
93open CostInj
94
95open Deqsets_extra
96
97open CostMisc
98
99open Listb_extra
100
101open CostSpec
102
103open CostCheck
104
105open BitVectorTrie
106
107open Graphs
108
109open Order
110
111open Registers
112
113open RTLabs_syntax
114
115open ToRTLabs
116
117open FrontEndOps
118
119open Cminor_syntax
120
121open ToCminor
122
123open MemProperties
124
125open MemoryInjections
126
127open Fresh
128
129open SwitchRemoval
130
131open Sets
132
133open Listb
134
135open Star
136
137open Frontend_misc
138
139open CexecInd
140
141open CexecSound
142
143open Casts
144
145open ClassifyOp
146
147open Smallstep
148
149open Extra_bool
150
151open FrontEndVal
152
153open Hide
154
155open ByteValues
156
157open GenMem
158
159open FrontEndMem
160
161open Globalenvs
162
163open Csem
164
165open SmallstepExec
166
167open Division
168
169open Z
170
171open BitVectorZ
172
173open Pointers
174
175open Values
176
177open Events
178
179open IOMonad
180
181open IO
182
183open Cexec
184
185open TypeComparison
186
187open SimplifyCasts
188
189open CostLabel
190
191open Coqlib
192
193open Proper
194
195open PositiveMap
196
197open Deqsets
198
199open ErrorMessages
200
201open PreIdentifiers
202
203open Errors
204
205open Extralib
206
207open Lists
208
209open Positive
210
211open Identifiers
212
213open Exp
214
215open Arithmetic
216
217open Vector
218
219open Div_and_mod
220
221open Util
222
223open FoldStuff
224
225open BitVector
226
227open Jmeq
228
229open Russell
230
231open List
232
233open Setoids
234
235open Monad
236
237open Option
238
239open Extranat
240
241open Bool
242
243open Relations
244
245open Nat
246
247open Integers
248
249open Hints_declaration
250
251open Core_notation
252
253open Pts
254
255open Logic
256
257open Types
258
259open AST
260
261open Csyntax
262
263open Label
264
265open Compiler
266
267open Stacksize
268
269open Executions
270
271open Measurable
272
273open Clight_abstract
274
275open Clight_classified_system
276
277open Cminor_semantics
278
279open Cminor_abstract
280
281open Cminor_classified_system
282
283open RTLabs_semantics
284
285open RTLabs_abstract
286
287open RTLabs_classified_system
288
289open ExtraMonads
290
291open ExtraGlobalenvs
292
293open I8051bis
294
295open BEMem
296
297open Joint_semantics
298
299open SemanticsUtils
300
301open Traces
302
303open Joint_fullexec
304
305open RTL_semantics
306
307open ERTL_semantics
308
309open ERTLptr_semantics
310
311open Joint_LTL_LIN_semantics
312
313open LTL_semantics
314
315open LIN_semantics
316
317open Interpret2
318
319type preclassified_system_pass =
320  Measurable.preclassified_system
321  (* singleton inductive, whose constructor was mk_preclassified_system_pass *)
322
323val preclassified_system_pass_rect_Type4 :
324  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
325  preclassified_system_pass -> 'a1
326
327val preclassified_system_pass_rect_Type5 :
328  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
329  preclassified_system_pass -> 'a1
330
331val preclassified_system_pass_rect_Type3 :
332  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
333  preclassified_system_pass -> 'a1
334
335val preclassified_system_pass_rect_Type2 :
336  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
337  preclassified_system_pass -> 'a1
338
339val preclassified_system_pass_rect_Type1 :
340  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
341  preclassified_system_pass -> 'a1
342
343val preclassified_system_pass_rect_Type0 :
344  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
345  preclassified_system_pass -> 'a1
346
347val pcs_pcs :
348  Compiler.pass -> preclassified_system_pass ->
349  Measurable.preclassified_system
350
351val preclassified_system_pass_inv_rect_Type4 :
352  Compiler.pass -> preclassified_system_pass ->
353  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
354
355val preclassified_system_pass_inv_rect_Type3 :
356  Compiler.pass -> preclassified_system_pass ->
357  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
358
359val preclassified_system_pass_inv_rect_Type2 :
360  Compiler.pass -> preclassified_system_pass ->
361  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
362
363val preclassified_system_pass_inv_rect_Type1 :
364  Compiler.pass -> preclassified_system_pass ->
365  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
366
367val preclassified_system_pass_inv_rect_Type0 :
368  Compiler.pass -> preclassified_system_pass ->
369  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
370
371val pcs_pcs__o__pcs_exec :
372  Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
373  SmallstepExec.fullexec
374
375val pcs_pcs__o__pcs_exec__o__es1 :
376  Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
377  SmallstepExec.trans_system
378
379val preclassified_system_of_pass :
380  Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass
381
382val run_and_print :
383  Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
384  Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
385  (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->
386  Types.unit0
387
Note: See TracBrowser for help on using the repository browser.