13 open Hints_declaration
133 open MemoryInjections
135 val convert_break_to_goto :
136 Csyntax.statement -> Csyntax.label -> Csyntax.statement
139 Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
140 Csyntax.label -> ((Csyntax.statement, Csyntax.label) Types.prod,
141 Identifiers.universe) Types.prod
143 val simplify_switch :
144 Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
145 (Csyntax.statement, Identifiers.universe) Types.prod
147 val 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
153 Csyntax.statement -> Identifiers.universe -> ((Csyntax.statement,
154 (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
155 Identifiers.universe) Types.prod
158 (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
159 Identifiers.universe) Types.prod -> 'a1
162 (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
163 Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
167 (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
168 Identifiers.universe) Types.prod -> Identifiers.universe
170 val least_identifier : PreIdentifiers.identifier
172 val max_of_expr : Csyntax.expr -> AST.ident
174 val max_of_ls : Csyntax.labeled_statements -> AST.ident
176 val max_of_statement : Csyntax.statement -> AST.ident
178 val max_id_of_function : Csyntax.function0 -> AST.ident
180 val function_switch_removal :
181 Csyntax.function0 -> (Csyntax.function0, (AST.ident, Csyntax.type0)
182 Types.prod List.list) Types.prod
184 val fundef_switch_removal : Csyntax.clight_fundef -> Csyntax.clight_fundef
186 val program_switch_removal : Csyntax.clight_program -> Csyntax.clight_program
188 val nonempty_block_rect_Type4 :
189 GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
191 val nonempty_block_rect_Type5 :
192 GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
194 val nonempty_block_rect_Type3 :
195 GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
197 val nonempty_block_rect_Type2 :
198 GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
200 val nonempty_block_rect_Type1 :
201 GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
203 val nonempty_block_rect_Type0 :
204 GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
206 val nonempty_block_inv_rect_Type4 :
207 GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
209 val nonempty_block_inv_rect_Type3 :
210 GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
212 val nonempty_block_inv_rect_Type2 :
213 GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
215 val nonempty_block_inv_rect_Type1 :
216 GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
218 val nonempty_block_inv_rect_Type0 :
219 GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
221 val nonempty_block_discr : GenMem.mem -> Pointers.block -> __
223 val nonempty_block_jmdiscr : GenMem.mem -> Pointers.block -> __
225 val sr_memext_rect_Type4 :
226 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
229 val sr_memext_rect_Type5 :
230 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
233 val sr_memext_rect_Type3 :
234 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
237 val sr_memext_rect_Type2 :
238 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
241 val sr_memext_rect_Type1 :
242 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
245 val sr_memext_rect_Type0 :
246 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
249 val sr_memext_inv_rect_Type4 :
250 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
253 val sr_memext_inv_rect_Type3 :
254 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
257 val sr_memext_inv_rect_Type2 :
258 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
261 val sr_memext_inv_rect_Type1 :
262 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
265 val sr_memext_inv_rect_Type0 :
266 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
269 val sr_memext_discr :
270 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __
272 val sr_memext_jmdiscr :
273 GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __
276 Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
277 Pointers.block Frontend_misc.lset