83 open Hints_declaration
109 val sem_neg : Values.val0 -> Csyntax.type0 -> Values.val0 Types.option
111 val sem_notint : Values.val0 -> Values.val0 Types.option
113 val sem_notbool : Values.val0 -> Csyntax.type0 -> Values.val0 Types.option
116 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
120 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
121 Csyntax.type0 -> Values.val0 Types.option
124 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
128 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
132 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
135 val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option
137 val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option
139 val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option
141 val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option
144 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
147 val sem_cmp_mismatch : Integers.comparison -> Values.val0 Types.option
149 val sem_cmp_match : Integers.comparison -> Values.val0 Types.option
152 Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
153 Csyntax.type0 -> GenMem.mem -> Values.val0 Types.option
155 val cast_bool_to_target :
156 Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option
158 val sem_unary_operation :
159 Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
162 val sem_binary_operation :
163 Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
164 Csyntax.type0 -> GenMem.mem -> Csyntax.type0 -> Values.val0 Types.option
167 AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
170 type genv = Csyntax.clight_fundef Globalenvs.genv_t
172 type env = Pointers.block Identifiers.identifier_map
176 val load_value_of_type :
177 Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
178 Values.val0 Types.option
180 val store_value_of_type :
181 Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
182 Values.val0 -> GenMem.mem Types.option
184 val blocks_of_env : env -> Pointers.block List.list
187 AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
188 Csyntax.labeled_statements Types.option
190 val seq_of_labeled_statement :
191 Csyntax.labeled_statements -> Csyntax.statement
195 | Kseq of Csyntax.statement * cont
196 | Kwhile of Csyntax.expr * Csyntax.statement * cont
197 | Kdowhile of Csyntax.expr * Csyntax.statement * cont
198 | Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
199 | Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
201 | Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
202 Types.prod Types.option * Csyntax.function0 * env * cont
204 val cont_rect_Type4 :
205 'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
206 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
207 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
208 Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
209 (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
210 'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
211 Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
212 env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
214 val cont_rect_Type3 :
215 'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
216 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
217 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
218 Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
219 (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
220 'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
221 Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
222 env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
224 val cont_rect_Type2 :
225 'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
226 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
227 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
228 Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
229 (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
230 'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
231 Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
232 env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
234 val cont_rect_Type1 :
235 'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
236 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
237 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
238 Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
239 (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
240 'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
241 Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
242 env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
244 val cont_rect_Type0 :
245 'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
246 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
247 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
248 Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
249 (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
250 'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
251 Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
252 env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
254 val cont_inv_rect_Type4 :
255 cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
256 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
257 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
258 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
259 (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
260 Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
261 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
262 Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
263 -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
265 val cont_inv_rect_Type3 :
266 cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
267 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
268 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
269 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
270 (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
271 Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
272 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
273 Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
274 -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
276 val cont_inv_rect_Type2 :
277 cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
278 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
279 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
280 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
281 (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
282 Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
283 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
284 Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
285 -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
287 val cont_inv_rect_Type1 :
288 cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
289 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
290 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
291 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
292 (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
293 Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
294 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
295 Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
296 -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
298 val cont_inv_rect_Type0 :
299 cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
300 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
301 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
302 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
303 (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
304 Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
305 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
306 Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
307 -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
309 val cont_discr : cont -> cont -> __
311 val cont_jmdiscr : cont -> cont -> __
313 val call_cont : cont -> cont
316 | State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem
317 | Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
319 | Returnstate of Values.val0 * cont * GenMem.mem
320 | Finalstate of Integers.int
322 val state_rect_Type4 :
323 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
324 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
325 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
326 (Integers.int -> 'a1) -> state -> 'a1
328 val state_rect_Type5 :
329 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
330 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
331 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
332 (Integers.int -> 'a1) -> state -> 'a1
334 val state_rect_Type3 :
335 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
336 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
337 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
338 (Integers.int -> 'a1) -> state -> 'a1
340 val state_rect_Type2 :
341 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
342 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
343 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
344 (Integers.int -> 'a1) -> state -> 'a1
346 val state_rect_Type1 :
347 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
348 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
349 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
350 (Integers.int -> 'a1) -> state -> 'a1
352 val state_rect_Type0 :
353 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
354 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
355 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
356 (Integers.int -> 'a1) -> state -> 'a1
358 val state_inv_rect_Type4 :
359 state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
360 GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
361 Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
362 -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
364 val state_inv_rect_Type3 :
365 state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
366 GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
367 Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
368 -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
370 val state_inv_rect_Type2 :
371 state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
372 GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
373 Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
374 -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
376 val state_inv_rect_Type1 :
377 state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
378 GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
379 Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
380 -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
382 val state_inv_rect_Type0 :
383 state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
384 GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
385 Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
386 -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
388 val state_discr : state -> state -> __
390 val state_jmdiscr : state -> state -> __
393 Csyntax.label -> Csyntax.labeled_statements -> cont -> (Csyntax.statement,
394 cont) Types.prod Types.option
397 Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
398 Types.prod Types.option
400 val fun_typeof : Csyntax.expr -> Csyntax.type0