source: driver/extracted/switchRemoval.mli @ 3106

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

New extraction

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