source: extracted/semantics.mli @ 2867

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

New extraction after indianess bug fixes by Paolo.

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