source: extracted/semantics.mli @ 3059

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

New extraction

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 Casts
138
139open ClassifyOp
140
141open Smallstep
142
143open Extra_bool
144
145open FrontEndVal
146
147open Hide
148
149open ByteValues
150
151open GenMem
152
153open FrontEndMem
154
155open Globalenvs
156
157open Csem
158
159open SmallstepExec
160
161open Division
162
163open Z
164
165open BitVectorZ
166
167open Pointers
168
169open Values
170
171open Events
172
173open IOMonad
174
175open IO
176
177open Cexec
178
179open TypeComparison
180
181open SimplifyCasts
182
183open CostLabel
184
185open Coqlib
186
187open Proper
188
189open PositiveMap
190
191open Deqsets
192
193open ErrorMessages
194
195open PreIdentifiers
196
197open Errors
198
199open Extralib
200
201open Lists
202
203open Positive
204
205open Identifiers
206
207open Exp
208
209open Arithmetic
210
211open Vector
212
213open Div_and_mod
214
215open Util
216
217open FoldStuff
218
219open BitVector
220
221open Jmeq
222
223open Russell
224
225open List
226
227open Setoids
228
229open Monad
230
231open Option
232
233open Extranat
234
235open Bool
236
237open Relations
238
239open Nat
240
241open Integers
242
243open Hints_declaration
244
245open Core_notation
246
247open Pts
248
249open Logic
250
251open Types
252
253open AST
254
255open Csyntax
256
257open Label
258
259open Compiler
260
261open Stacksize
262
263open Executions
264
265open Measurable
266
267open Clight_abstract
268
269open Clight_classified_system
270
271open Cminor_semantics
272
273open Cminor_abstract
274
275open Cminor_classified_system
276
277open RTLabs_semantics
278
279open RTLabs_abstract
280
281open RTLabs_classified_system
282
283open ExtraMonads
284
285open ExtraGlobalenvs
286
287open I8051bis
288
289open BEMem
290
291open Joint_semantics
292
293open SemanticsUtils
294
295open Traces
296
297open Joint_fullexec
298
299open RTL_semantics
300
301open ERTL_semantics
302
303open Joint_LTL_LIN_semantics
304
305open LTL_semantics
306
307open LIN_semantics
308
309open Interpret2
310
311type preclassified_system_pass =
312  Measurable.preclassified_system
313  (* singleton inductive, whose constructor was mk_preclassified_system_pass *)
314
315val preclassified_system_pass_rect_Type4 :
316  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
317  preclassified_system_pass -> 'a1
318
319val preclassified_system_pass_rect_Type5 :
320  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
321  preclassified_system_pass -> 'a1
322
323val preclassified_system_pass_rect_Type3 :
324  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
325  preclassified_system_pass -> 'a1
326
327val preclassified_system_pass_rect_Type2 :
328  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
329  preclassified_system_pass -> 'a1
330
331val preclassified_system_pass_rect_Type1 :
332  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
333  preclassified_system_pass -> 'a1
334
335val preclassified_system_pass_rect_Type0 :
336  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
337  preclassified_system_pass -> 'a1
338
339val pcs_pcs :
340  Compiler.pass -> preclassified_system_pass ->
341  Measurable.preclassified_system
342
343val preclassified_system_pass_inv_rect_Type4 :
344  Compiler.pass -> preclassified_system_pass ->
345  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
346
347val preclassified_system_pass_inv_rect_Type3 :
348  Compiler.pass -> preclassified_system_pass ->
349  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
350
351val preclassified_system_pass_inv_rect_Type2 :
352  Compiler.pass -> preclassified_system_pass ->
353  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
354
355val preclassified_system_pass_inv_rect_Type1 :
356  Compiler.pass -> preclassified_system_pass ->
357  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
358
359val preclassified_system_pass_inv_rect_Type0 :
360  Compiler.pass -> preclassified_system_pass ->
361  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
362
363val pcs_pcs__o__pcs_exec :
364  Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
365  SmallstepExec.fullexec
366
367val pcs_pcs__o__pcs_exec__o__es1 :
368  Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
369  SmallstepExec.trans_system
370
371val preclassified_system_of_pass :
372  Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass
373
374val run_and_print :
375  Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
376  Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
377  (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->
378  Types.unit0
379
Note: See TracBrowser for help on using the repository browser.