source: extracted/semantics.mli @ 3019

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

New extraction after ERTLptr abortion.

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