source: extracted/semantics.mli @ 2875

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

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

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
319open Interpret2
320
321type preclassified_system_pass =
322  Measurable.preclassified_system
323  (* singleton inductive, whose constructor was mk_preclassified_system_pass *)
324
325val preclassified_system_pass_rect_Type4 :
326  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
327  preclassified_system_pass -> 'a1
328
329val preclassified_system_pass_rect_Type5 :
330  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
331  preclassified_system_pass -> 'a1
332
333val preclassified_system_pass_rect_Type3 :
334  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
335  preclassified_system_pass -> 'a1
336
337val preclassified_system_pass_rect_Type2 :
338  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
339  preclassified_system_pass -> 'a1
340
341val preclassified_system_pass_rect_Type1 :
342  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
343  preclassified_system_pass -> 'a1
344
345val preclassified_system_pass_rect_Type0 :
346  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
347  preclassified_system_pass -> 'a1
348
349val pcs_pcs :
350  Compiler.pass -> preclassified_system_pass ->
351  Measurable.preclassified_system
352
353val preclassified_system_pass_inv_rect_Type4 :
354  Compiler.pass -> preclassified_system_pass ->
355  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
356
357val preclassified_system_pass_inv_rect_Type3 :
358  Compiler.pass -> preclassified_system_pass ->
359  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
360
361val preclassified_system_pass_inv_rect_Type2 :
362  Compiler.pass -> preclassified_system_pass ->
363  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
364
365val preclassified_system_pass_inv_rect_Type1 :
366  Compiler.pass -> preclassified_system_pass ->
367  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
368
369val preclassified_system_pass_inv_rect_Type0 :
370  Compiler.pass -> preclassified_system_pass ->
371  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
372
373val pcs_pcs__o__pcs_exec :
374  Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
375  SmallstepExec.fullexec
376
377val pcs_pcs__o__pcs_exec__o__es1 :
378  Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
379  SmallstepExec.trans_system
380
381val preclassified_system_of_pass :
382  Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass
383
384val run_and_print :
385  Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
386  Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
387  (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->
388  Types.unit0
389
Note: See TracBrowser for help on using the repository browser.