source: extracted/semantics.mli @ 2829

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

Semantics files committed.

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