source: extracted/switchRemoval.mli @ 2716

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

...

File size: 7.4 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75open Fresh
76
77open TypeComparison
78
79open ClassifyOp
80
81open Smallstep
82
83open Extra_bool
84
85open FrontEndVal
86
87open Hide
88
89open ByteValues
90
91open GenMem
92
93open FrontEndMem
94
95open Globalenvs
96
97open Csem
98
99open SmallstepExec
100
101open Division
102
103open Z
104
105open BitVectorZ
106
107open Pointers
108
109open Values
110
111open Events
112
113open IOMonad
114
115open IO
116
117open Cexec
118
119open CexecInd
120
121open Sets
122
123open Listb
124
125open Star
126
127open Frontend_misc
128
129open MemProperties
130
131open MemoryInjections
132
133type switch_free = __
134
135type branches_switch_free = __
136
137val convert_break_to_goto :
138  Csyntax.statement -> Csyntax.label -> Csyntax.statement
139
140val produce_cond :
141  Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
142  Csyntax.label -> ((Csyntax.statement, Csyntax.label) Types.prod,
143  Identifiers.universe) Types.prod
144
145val simplify_switch :
146  Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
147  (Csyntax.statement, Identifiers.universe) Types.prod
148
149val switch_removal_branches :
150  Csyntax.labeled_statements -> Identifiers.universe ->
151  ((Csyntax.labeled_statements, (AST.ident, Csyntax.type0) Types.prod
152  List.list) Types.prod, Identifiers.universe) Types.prod
153
154val switch_removal :
155  Csyntax.statement -> Identifiers.universe -> ((Csyntax.statement,
156  (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
157  Identifiers.universe) Types.prod
158
159val ret_st :
160  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
161  Identifiers.universe) Types.prod -> 'a1
162
163val ret_vars :
164  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
165  Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
166  List.list
167
168val ret_u :
169  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
170  Identifiers.universe) Types.prod -> Identifiers.universe
171
172val least_identifier : PreIdentifiers.identifier
173
174val max_of_expr : Csyntax.expr -> AST.ident
175
176val max_of_ls : Csyntax.labeled_statements -> AST.ident
177
178val max_of_statement : Csyntax.statement -> AST.ident
179
180val max_id_of_function : Csyntax.function0 -> AST.ident
181
182val function_switch_removal :
183  Csyntax.function0 -> (Csyntax.function0, (AST.ident, Csyntax.type0)
184  Types.prod List.list) Types.prod
185
186val fundef_switch_removal : Csyntax.clight_fundef -> Csyntax.clight_fundef
187
188val program_switch_removal : Csyntax.clight_program -> Csyntax.clight_program
189
190type substatement_ls = __
191
192type substatement_P = __
193
194val nonempty_block_rect_Type4 :
195  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
196
197val nonempty_block_rect_Type5 :
198  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
199
200val nonempty_block_rect_Type3 :
201  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
202
203val nonempty_block_rect_Type2 :
204  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
205
206val nonempty_block_rect_Type1 :
207  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
208
209val nonempty_block_rect_Type0 :
210  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
211
212val nonempty_block_inv_rect_Type4 :
213  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
214
215val nonempty_block_inv_rect_Type3 :
216  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
217
218val nonempty_block_inv_rect_Type2 :
219  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
220
221val nonempty_block_inv_rect_Type1 :
222  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
223
224val nonempty_block_inv_rect_Type0 :
225  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
226
227val nonempty_block_discr : GenMem.mem1 -> Pointers.block -> __
228
229val nonempty_block_jmdiscr : GenMem.mem1 -> Pointers.block -> __
230
231val sr_memext_rect_Type4 :
232  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
233  -> 'a1) -> 'a1
234
235val sr_memext_rect_Type5 :
236  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
237  -> 'a1) -> 'a1
238
239val sr_memext_rect_Type3 :
240  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
241  -> 'a1) -> 'a1
242
243val sr_memext_rect_Type2 :
244  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
245  -> 'a1) -> 'a1
246
247val sr_memext_rect_Type1 :
248  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
249  -> 'a1) -> 'a1
250
251val sr_memext_rect_Type0 :
252  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
253  -> 'a1) -> 'a1
254
255val sr_memext_inv_rect_Type4 :
256  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
257  -> __ -> 'a1) -> 'a1
258
259val sr_memext_inv_rect_Type3 :
260  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
261  -> __ -> 'a1) -> 'a1
262
263val sr_memext_inv_rect_Type2 :
264  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
265  -> __ -> 'a1) -> 'a1
266
267val sr_memext_inv_rect_Type1 :
268  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
269  -> __ -> 'a1) -> 'a1
270
271val sr_memext_inv_rect_Type0 :
272  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
273  -> __ -> 'a1) -> 'a1
274
275val sr_memext_discr :
276  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> __
277
278val sr_memext_jmdiscr :
279  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> __
280
281val env_codomain :
282  Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
283  Pointers.block Frontend_misc.lset
284
285val switch_removal_globals_rect_Type4 :
286  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
287  -> __ -> 'a2) -> 'a2
288
289val switch_removal_globals_rect_Type5 :
290  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
291  -> __ -> 'a2) -> 'a2
292
293val switch_removal_globals_rect_Type3 :
294  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
295  -> __ -> 'a2) -> 'a2
296
297val switch_removal_globals_rect_Type2 :
298  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
299  -> __ -> 'a2) -> 'a2
300
301val switch_removal_globals_rect_Type1 :
302  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
303  -> __ -> 'a2) -> 'a2
304
305val switch_removal_globals_rect_Type0 :
306  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
307  -> __ -> 'a2) -> 'a2
308
309val switch_removal_globals_inv_rect_Type4 :
310  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
311  -> __ -> __ -> 'a2) -> 'a2
312
313val switch_removal_globals_inv_rect_Type3 :
314  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
315  -> __ -> __ -> 'a2) -> 'a2
316
317val switch_removal_globals_inv_rect_Type2 :
318  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
319  -> __ -> __ -> 'a2) -> 'a2
320
321val switch_removal_globals_inv_rect_Type1 :
322  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
323  -> __ -> __ -> 'a2) -> 'a2
324
325val switch_removal_globals_inv_rect_Type0 :
326  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
327  -> __ -> __ -> 'a2) -> 'a2
328
329val switch_removal_globals_discr :
330  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
331
332val switch_removal_globals_jmdiscr :
333  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
334
Note: See TracBrowser for help on using the repository browser.