83 open Hints_declaration
110 Values.val0 -> Csyntax.type0 -> Values.val0 Types.option **)
111 let rec sem_neg v = function
112 | Csyntax.Tvoid -> Types.None
113 | Csyntax.Tint (sz, x) ->
115 | Values.Vundef -> Types.None
116 | Values.Vint (sz', n) ->
117 (match AST.eq_intsize sz sz' with
119 Types.Some (Values.Vint (sz',
120 (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz') n)))
121 | Bool.False -> Types.None)
122 | Values.Vnull -> Types.None
123 | Values.Vptr x0 -> Types.None)
124 | Csyntax.Tpointer x -> Types.None
125 | Csyntax.Tarray (x, x0) -> Types.None
126 | Csyntax.Tfunction (x, x0) -> Types.None
127 | Csyntax.Tstruct (x, x0) -> Types.None
128 | Csyntax.Tunion (x, x0) -> Types.None
129 | Csyntax.Tcomp_ptr x -> Types.None
131 (** val sem_notint : Values.val0 -> Values.val0 Types.option **)
132 let rec sem_notint = function
133 | Values.Vundef -> Types.None
134 | Values.Vint (sz, n) ->
135 Types.Some (Values.Vint (sz,
136 (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
138 | Values.Vnull -> Types.None
139 | Values.Vptr x -> Types.None
141 (** val sem_notbool :
142 Values.val0 -> Csyntax.type0 -> Values.val0 Types.option **)
143 let rec sem_notbool v = function
144 | Csyntax.Tvoid -> Types.None
145 | Csyntax.Tint (sz, x) ->
147 | Values.Vundef -> Types.None
148 | Values.Vint (sz', n) ->
149 (match AST.eq_intsize sz sz' with
153 (BitVector.eq_bv (AST.bitsize_of_intsize sz') n
154 (BitVector.zero (AST.bitsize_of_intsize sz'))))
155 | Bool.False -> Types.None)
156 | Values.Vnull -> Types.None
157 | Values.Vptr x0 -> Types.None)
158 | Csyntax.Tpointer x ->
160 | Values.Vundef -> Types.None
161 | Values.Vint (x0, x1) -> Types.None
162 | Values.Vnull -> Types.Some Values.vtrue
163 | Values.Vptr x0 -> Types.Some Values.vfalse)
164 | Csyntax.Tarray (x, x0) -> Types.None
165 | Csyntax.Tfunction (x, x0) -> Types.None
166 | Csyntax.Tstruct (x, x0) -> Types.None
167 | Csyntax.Tunion (x, x0) -> Types.None
168 | Csyntax.Tcomp_ptr x -> Types.None
171 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
172 Values.val0 Types.option **)
173 let rec sem_add v1 t1 v2 t2 =
174 match ClassifyOp.classify_add t1 t2 with
175 | ClassifyOp.Add_case_ii (x, x0) ->
177 | Values.Vundef -> Types.None
178 | Values.Vint (sz1, n1) ->
180 | Values.Vundef -> Types.None
181 | Values.Vint (sz2, n2) ->
182 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
184 (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))))
186 | Values.Vnull -> Types.None
187 | Values.Vptr x1 -> Types.None)
188 | Values.Vnull -> Types.None
189 | Values.Vptr x1 -> Types.None)
190 | ClassifyOp.Add_case_pi (x, ty, x0, sg) ->
192 | Values.Vundef -> Types.None
193 | Values.Vint (x1, x2) -> Types.None
196 | Values.Vundef -> Types.None
197 | Values.Vint (sz2, n2) ->
198 (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
199 (BitVector.zero (AST.bitsize_of_intsize sz2)) with
200 | Bool.True -> Types.Some Values.Vnull
201 | Bool.False -> Types.None)
202 | Values.Vnull -> Types.None
203 | Values.Vptr x1 -> Types.None)
204 | Values.Vptr ptr1 ->
206 | Values.Vundef -> Types.None
207 | Values.Vint (sz2, n2) ->
208 Types.Some (Values.Vptr
209 (Pointers.shift_pointer_n (AST.bitsize_of_intsize sz2) ptr1
210 (Csyntax.sizeof ty) sg n2))
211 | Values.Vnull -> Types.None
212 | Values.Vptr x1 -> Types.None))
213 | ClassifyOp.Add_case_ip (x, x0, sg, ty) ->
215 | Values.Vundef -> Types.None
216 | Values.Vint (sz1, n1) ->
218 | Values.Vundef -> Types.None
219 | Values.Vint (x1, x2) -> Types.None
221 (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
222 (BitVector.zero (AST.bitsize_of_intsize sz1)) with
223 | Bool.True -> Types.Some Values.Vnull
224 | Bool.False -> Types.None)
225 | Values.Vptr ptr2 ->
226 Types.Some (Values.Vptr
227 (Pointers.shift_pointer_n (AST.bitsize_of_intsize sz1) ptr2
228 (Csyntax.sizeof ty) sg n1)))
229 | Values.Vnull -> Types.None
230 | Values.Vptr x1 -> Types.None)
231 | ClassifyOp.Add_default (x, x0) -> Types.None
234 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
235 Csyntax.type0 -> Values.val0 Types.option **)
236 let rec sem_sub v1 t1 v2 t2 target =
237 match ClassifyOp.classify_sub t1 t2 with
238 | ClassifyOp.Sub_case_ii (x, x0) ->
240 | Values.Vundef -> Types.None
241 | Values.Vint (sz1, n1) ->
243 | Values.Vundef -> Types.None
244 | Values.Vint (sz2, n2) ->
245 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
247 (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2))))
249 | Values.Vnull -> Types.None
250 | Values.Vptr x1 -> Types.None)
251 | Values.Vnull -> Types.None
252 | Values.Vptr x1 -> Types.None)
253 | ClassifyOp.Sub_case_pi (x, ty, x0, sg) ->
255 | Values.Vundef -> Types.None
256 | Values.Vint (x1, x2) -> Types.None
259 | Values.Vundef -> Types.None
260 | Values.Vint (sz2, n2) ->
261 (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
262 (BitVector.zero (AST.bitsize_of_intsize sz2)) with
263 | Bool.True -> Types.Some Values.Vnull
264 | Bool.False -> Types.None)
265 | Values.Vnull -> Types.None
266 | Values.Vptr x1 -> Types.None)
267 | Values.Vptr ptr1 ->
269 | Values.Vundef -> Types.None
270 | Values.Vint (sz2, n2) ->
271 Types.Some (Values.Vptr
272 (Pointers.neg_shift_pointer_n (AST.bitsize_of_intsize sz2) ptr1
273 (Csyntax.sizeof ty) sg n2))
274 | Values.Vnull -> Types.None
275 | Values.Vptr x1 -> Types.None))
276 | ClassifyOp.Sub_case_pp (x, x0, ty, x1) ->
278 | Values.Vundef -> Types.None
279 | Values.Vint (x2, x3) -> Types.None
282 | Values.Vundef -> Types.None
283 | Values.Vint (x2, x3) -> Types.None
286 | Csyntax.Tvoid -> Types.None
287 | Csyntax.Tint (tsz, tsg) ->
288 Types.Some (Values.Vint (tsz,
289 (BitVector.zero (AST.bitsize_of_intsize tsz))))
290 | Csyntax.Tpointer x2 -> Types.None
291 | Csyntax.Tarray (x2, x3) -> Types.None
292 | Csyntax.Tfunction (x2, x3) -> Types.None
293 | Csyntax.Tstruct (x2, x3) -> Types.None
294 | Csyntax.Tunion (x2, x3) -> Types.None
295 | Csyntax.Tcomp_ptr x2 -> Types.None)
296 | Values.Vptr x2 -> Types.None)
297 | Values.Vptr ptr1 ->
299 | Values.Vundef -> Types.None
300 | Values.Vint (x2, x3) -> Types.None
301 | Values.Vnull -> Types.None
302 | Values.Vptr ptr2 ->
303 (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
305 (match Nat.eqb (Csyntax.sizeof ty) Nat.O with
306 | Bool.True -> Types.None
309 | Csyntax.Tvoid -> Types.None
310 | Csyntax.Tint (tsz, tsg) ->
311 (match Arithmetic.division_u (Nat.S (Nat.S (Nat.S (Nat.S
312 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
313 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
314 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
315 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
316 Nat.O)))))))))))))))))))))))))))))))
317 (Pointers.sub_offset (Nat.S (Nat.S (Nat.S (Nat.S
318 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
319 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
320 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
321 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
322 (Nat.S (Nat.S (Nat.S (Nat.S
323 Nat.O))))))))))))))))))))))))))))))))
324 ptr1.Pointers.poff ptr2.Pointers.poff)
325 (Integers.repr (Csyntax.sizeof ty)) with
326 | Types.None -> Types.None
328 Types.Some (Values.Vint (tsz,
329 (Arithmetic.zero_ext (Nat.S (Nat.S (Nat.S (Nat.S
330 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
331 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
332 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
333 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
334 Nat.O))))))))))))))))))))))))))))))))
335 (AST.bitsize_of_intsize tsz) v))))
336 | Csyntax.Tpointer x2 -> Types.None
337 | Csyntax.Tarray (x2, x3) -> Types.None
338 | Csyntax.Tfunction (x2, x3) -> Types.None
339 | Csyntax.Tstruct (x2, x3) -> Types.None
340 | Csyntax.Tunion (x2, x3) -> Types.None
341 | Csyntax.Tcomp_ptr x2 -> Types.None))
342 | Bool.False -> Types.None)))
343 | ClassifyOp.Sub_default (x, x0) -> Types.None
346 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
347 Values.val0 Types.option **)
348 let rec sem_mul v1 t1 v2 t2 =
349 match ClassifyOp.classify_aop t1 t2 with
350 | ClassifyOp.Aop_case_ii (x, x0) ->
352 | Values.Vundef -> Types.None
353 | Values.Vint (sz1, n1) ->
355 | Values.Vundef -> Types.None
356 | Values.Vint (sz2, n2) ->
357 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
359 (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
361 | Values.Vnull -> Types.None
362 | Values.Vptr x1 -> Types.None)
363 | Values.Vnull -> Types.None
364 | Values.Vptr x1 -> Types.None)
365 | ClassifyOp.Aop_default (x, x0) -> Types.None
368 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
369 Values.val0 Types.option **)
370 let rec sem_div v1 t1 v2 t2 =
371 match ClassifyOp.classify_aop t1 t2 with
372 | ClassifyOp.Aop_case_ii (x, sg) ->
374 | Values.Vundef -> Types.None
375 | Values.Vint (sz1, n1) ->
377 | Values.Vundef -> Types.None
378 | Values.Vint (sz2, n2) ->
381 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
382 Types.option_map (fun x0 -> Values.Vint (sz2, x0))
383 (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
386 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
387 Types.option_map (fun x0 -> Values.Vint (sz2, x0))
388 (Arithmetic.division_u
389 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
391 (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
392 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
393 Nat.O)))))))))) n10 n2)) Types.None)
394 | Values.Vnull -> Types.None
395 | Values.Vptr x0 -> Types.None)
396 | Values.Vnull -> Types.None
397 | Values.Vptr x0 -> Types.None)
398 | ClassifyOp.Aop_default (x, x0) -> Types.None
401 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
402 Values.val0 Types.option **)
403 let rec sem_mod v1 t1 v2 t2 =
404 match ClassifyOp.classify_aop t1 t2 with
405 | ClassifyOp.Aop_case_ii (sz, sg) ->
407 | Values.Vundef -> Types.None
408 | Values.Vint (sz1, n1) ->
410 | Values.Vundef -> Types.None
411 | Values.Vint (sz2, n2) ->
414 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
415 Types.option_map (fun x -> Values.Vint (sz2, x))
416 (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
419 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
420 Types.option_map (fun x -> Values.Vint (sz2, x))
421 (Arithmetic.modulus_u
422 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
424 (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
425 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
426 Nat.O)))))))))) n10 n2)) Types.None)
427 | Values.Vnull -> Types.None
428 | Values.Vptr x -> Types.None)
429 | Values.Vnull -> Types.None
430 | Values.Vptr x -> Types.None)
431 | ClassifyOp.Aop_default (x, x0) -> Types.None
433 (** val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
434 let rec sem_and v1 v2 =
436 | Values.Vundef -> Types.None
437 | Values.Vint (sz1, n1) ->
439 | Values.Vundef -> Types.None
440 | Values.Vint (sz2, n2) ->
441 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
443 (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
445 | Values.Vnull -> Types.None
446 | Values.Vptr x -> Types.None)
447 | Values.Vnull -> Types.None
448 | Values.Vptr x -> Types.None
450 (** val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
451 let rec sem_or v1 v2 =
453 | Values.Vundef -> Types.None
454 | Values.Vint (sz1, n1) ->
456 | Values.Vundef -> Types.None
457 | Values.Vint (sz2, n2) ->
458 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
460 (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
462 | Values.Vnull -> Types.None
463 | Values.Vptr x -> Types.None)
464 | Values.Vnull -> Types.None
465 | Values.Vptr x -> Types.None
467 (** val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
468 let rec sem_xor v1 v2 =
470 | Values.Vundef -> Types.None
471 | Values.Vint (sz1, n1) ->
473 | Values.Vundef -> Types.None
474 | Values.Vint (sz2, n2) ->
475 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
477 (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
479 | Values.Vnull -> Types.None
480 | Values.Vptr x -> Types.None)
481 | Values.Vnull -> Types.None
482 | Values.Vptr x -> Types.None
484 (** val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
485 let rec sem_shl v1 v2 =
487 | Values.Vundef -> Types.None
488 | Values.Vint (sz1, n1) ->
490 | Values.Vundef -> Types.None
491 | Values.Vint (sz2, n2) ->
492 (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
493 (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
494 (AST.bitsize_of_intsize sz1)) with
496 Types.Some (Values.Vint (sz1,
497 (Vector.shift_left (AST.bitsize_of_intsize sz1)
498 (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
500 | Bool.False -> Types.None)
501 | Values.Vnull -> Types.None
502 | Values.Vptr x -> Types.None)
503 | Values.Vnull -> Types.None
504 | Values.Vptr x -> Types.None
507 Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
508 Values.val0 Types.option **)
509 let rec sem_shr v1 t1 v2 t2 =
510 match ClassifyOp.classify_aop t1 t2 with
511 | ClassifyOp.Aop_case_ii (x, sg) ->
513 | Values.Vundef -> Types.None
514 | Values.Vint (sz1, n1) ->
516 | Values.Vundef -> Types.None
517 | Values.Vint (sz2, n2) ->
520 (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
521 (Arithmetic.bitvector_of_nat
522 (AST.bitsize_of_intsize sz2)
523 (AST.bitsize_of_intsize sz1)) with
525 Types.Some (Values.Vint (sz1,
527 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
529 (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
530 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
532 (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
535 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
537 (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
538 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
539 Nat.O)))))))))) n1))))
540 | Bool.False -> Types.None)
542 (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
543 (Arithmetic.bitvector_of_nat
544 (AST.bitsize_of_intsize sz2)
545 (AST.bitsize_of_intsize sz1)) with
547 Types.Some (Values.Vint (sz1,
549 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
551 (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
552 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
554 (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
556 | Bool.False -> Types.None))
557 | Values.Vnull -> Types.None
558 | Values.Vptr x0 -> Types.None)
559 | Values.Vnull -> Types.None
560 | Values.Vptr x0 -> Types.None)
561 | ClassifyOp.Aop_default (x, x0) -> Types.None
563 (** val sem_cmp_mismatch :
564 Integers.comparison -> Values.val0 Types.option **)
565 let rec sem_cmp_mismatch = function
566 | Integers.Ceq -> Types.Some Values.vfalse
567 | Integers.Cne -> Types.Some Values.vtrue
568 | Integers.Clt -> Types.None
569 | Integers.Cle -> Types.None
570 | Integers.Cgt -> Types.None
571 | Integers.Cge -> Types.None
573 (** val sem_cmp_match : Integers.comparison -> Values.val0 Types.option **)
574 let rec sem_cmp_match = function
575 | Integers.Ceq -> Types.Some Values.vtrue
576 | Integers.Cne -> Types.Some Values.vfalse
577 | Integers.Clt -> Types.None
578 | Integers.Cle -> Types.None
579 | Integers.Cgt -> Types.None
580 | Integers.Cge -> Types.None
583 Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
584 Csyntax.type0 -> GenMem.mem -> Values.val0 Types.option **)
585 let rec sem_cmp c v1 t1 v2 t2 m =
586 match ClassifyOp.classify_cmp t1 t2 with
587 | ClassifyOp.Cmp_case_ii (x, sg) ->
589 | Values.Vundef -> Types.None
590 | Values.Vint (sz1, n1) ->
592 | Values.Vundef -> Types.None
593 | Values.Vint (sz2, n2) ->
596 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
598 (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
601 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
603 (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
605 | Values.Vnull -> Types.None
606 | Values.Vptr x0 -> Types.None)
607 | Values.Vnull -> Types.None
608 | Values.Vptr x0 -> Types.None)
609 | ClassifyOp.Cmp_case_pp (x, x0) ->
611 | Values.Vundef -> Types.None
612 | Values.Vint (x1, x2) -> Types.None
615 | Values.Vundef -> Types.None
616 | Values.Vint (x1, x2) -> Types.None
617 | Values.Vnull -> sem_cmp_match c
618 | Values.Vptr ptr2 -> sem_cmp_mismatch c)
619 | Values.Vptr ptr1 ->
621 | Values.Vundef -> Types.None
622 | Values.Vint (x1, x2) -> Types.None
623 | Values.Vnull -> sem_cmp_mismatch c
624 | Values.Vptr ptr2 ->
625 (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
626 (FrontEndMem.valid_pointer m ptr2) with
628 (match Pointers.eq_block ptr1.Pointers.pblock
629 ptr2.Pointers.pblock with
633 (Values.cmp_offset c ptr1.Pointers.poff
635 | Bool.False -> sem_cmp_mismatch c)
636 | Bool.False -> Types.None)))
637 | ClassifyOp.Cmp_default (x, x0) -> Types.None
639 (** val cast_bool_to_target :
640 Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option **)
641 let cast_bool_to_target ty = function
642 | Types.None -> Types.None
645 | Csyntax.Tvoid -> Types.None
646 | Csyntax.Tint (sz, sg) -> Types.Some (Values.zero_ext sz v)
647 | Csyntax.Tpointer x -> Types.None
648 | Csyntax.Tarray (x, x0) -> Types.None
649 | Csyntax.Tfunction (x, x0) -> Types.None
650 | Csyntax.Tstruct (x, x0) -> Types.None
651 | Csyntax.Tunion (x, x0) -> Types.None
652 | Csyntax.Tcomp_ptr x -> Types.None)
654 (** val sem_unary_operation :
655 Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
657 let sem_unary_operation op v ty =
659 | Csyntax.Onotbool -> sem_notbool v ty
660 | Csyntax.Onotint -> sem_notint v
661 | Csyntax.Oneg -> sem_neg v ty
663 (** val sem_binary_operation :
664 Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
665 -> Csyntax.type0 -> GenMem.mem -> Csyntax.type0 -> Values.val0
667 let rec sem_binary_operation op v1 t1 v2 t2 m ty =
669 | Csyntax.Oadd -> sem_add v1 t1 v2 t2
670 | Csyntax.Osub -> sem_sub v1 t1 v2 t2 ty
671 | Csyntax.Omul -> sem_mul v1 t1 v2 t2
672 | Csyntax.Odiv -> sem_div v1 t1 v2 t2
673 | Csyntax.Omod -> sem_mod v1 t1 v2 t2
674 | Csyntax.Oand -> sem_and v1 v2
675 | Csyntax.Oor -> sem_or v1 v2
676 | Csyntax.Oxor -> sem_xor v1 v2
677 | Csyntax.Oshl -> sem_shl v1 v2
678 | Csyntax.Oshr -> sem_shr v1 t1 v2 t2
680 cast_bool_to_target ty (sem_cmp Integers.Ceq v1 t1 v2 t2 m)
682 cast_bool_to_target ty (sem_cmp Integers.Cne v1 t1 v2 t2 m)
684 cast_bool_to_target ty (sem_cmp Integers.Clt v1 t1 v2 t2 m)
686 cast_bool_to_target ty (sem_cmp Integers.Cgt v1 t1 v2 t2 m)
688 cast_bool_to_target ty (sem_cmp Integers.Cle v1 t1 v2 t2 m)
690 cast_bool_to_target ty (sem_cmp Integers.Cge v1 t1 v2 t2 m)
692 (** val cast_int_int :
693 AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
694 BitVector.bitVector **)
695 let rec cast_int_int sz sg dstsz i =
698 Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
699 (AST.bitsize_of_intsize dstsz) i
701 Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
702 (AST.bitsize_of_intsize dstsz) i
704 type genv = Csyntax.clight_fundef Globalenvs.genv_t
706 type env = Pointers.block Identifiers.identifier_map
708 (** val empty_env : env **)
710 Identifiers.empty_map PreIdentifiers.SymbolTag
712 (** val load_value_of_type :
713 Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
714 Values.val0 Types.option **)
715 let rec load_value_of_type ty m b ofs =
716 match Csyntax.access_mode ty with
717 | Csyntax.By_value chunk ->
718 FrontEndMem.loadv chunk m (Values.Vptr { Pointers.pblock = b;
719 Pointers.poff = ofs })
720 | Csyntax.By_reference ->
721 Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff = ofs })
722 | Csyntax.By_nothing x -> Types.None
724 (** val store_value_of_type :
725 Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
726 Values.val0 -> GenMem.mem Types.option **)
727 let rec store_value_of_type ty_dest m loc ofs v =
728 match Csyntax.access_mode ty_dest with
729 | Csyntax.By_value chunk ->
730 FrontEndMem.storev chunk m (Values.Vptr { Pointers.pblock = loc;
731 Pointers.poff = ofs }) v
732 | Csyntax.By_reference -> Types.None
733 | Csyntax.By_nothing x -> Types.None
735 (** val blocks_of_env : env -> Pointers.block List.list **)
736 let blocks_of_env e =
737 List.map (fun x -> x.Types.snd)
738 (Identifiers.elements PreIdentifiers.SymbolTag e)
740 (** val select_switch :
741 AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
742 Csyntax.labeled_statements Types.option **)
743 let rec select_switch sz n sl = match sl with
744 | Csyntax.LSdefault x -> Types.Some sl
745 | Csyntax.LScase (sz', c, s, sl') ->
746 AST.intsize_eq_elim sz sz' n (fun n0 ->
747 match BitVector.eq_bv (AST.bitsize_of_intsize sz') c n0 with
748 | Bool.True -> Types.Some sl
749 | Bool.False -> select_switch sz' n0 sl') Types.None
751 (** val seq_of_labeled_statement :
752 Csyntax.labeled_statements -> Csyntax.statement **)
753 let rec seq_of_labeled_statement = function
754 | Csyntax.LSdefault s -> s
755 | Csyntax.LScase (x, c, s, sl') ->
756 Csyntax.Ssequence (s, (seq_of_labeled_statement sl'))
760 | Kseq of Csyntax.statement * cont
761 | Kwhile of Csyntax.expr * Csyntax.statement * cont
762 | Kdowhile of Csyntax.expr * Csyntax.statement * cont
763 | Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
764 | Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
766 | Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
767 Types.prod Types.option * Csyntax.function0 * env * cont
769 (** val cont_rect_Type4 :
770 'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
771 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
772 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
773 Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
774 (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
775 'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
776 Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
777 -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
778 let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
780 | Kseq (x_8739, x_8738) ->
782 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
783 h_Kswitch h_Kcall x_8738)
784 | Kwhile (x_8742, x_8741, x_8740) ->
785 h_Kwhile x_8742 x_8741 x_8740
786 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
787 h_Kswitch h_Kcall x_8740)
788 | Kdowhile (x_8745, x_8744, x_8743) ->
789 h_Kdowhile x_8745 x_8744 x_8743
790 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
791 h_Kswitch h_Kcall x_8743)
792 | Kfor2 (x_8749, x_8748, x_8747, x_8746) ->
793 h_Kfor2 x_8749 x_8748 x_8747 x_8746
794 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
795 h_Kswitch h_Kcall x_8746)
796 | Kfor3 (x_8753, x_8752, x_8751, x_8750) ->
797 h_Kfor3 x_8753 x_8752 x_8751 x_8750
798 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
799 h_Kswitch h_Kcall x_8750)
802 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
803 h_Kswitch h_Kcall x_8754)
804 | Kcall (x_8758, x_8757, x_8756, x_8755) ->
805 h_Kcall x_8758 x_8757 x_8756 x_8755
806 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
807 h_Kswitch h_Kcall x_8755)
809 (** val cont_rect_Type3 :
810 'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
811 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
812 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
813 Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
814 (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
815 'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
816 Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
817 -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
818 let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
820 | Kseq (x_8799, x_8798) ->
822 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
823 h_Kswitch h_Kcall x_8798)
824 | Kwhile (x_8802, x_8801, x_8800) ->
825 h_Kwhile x_8802 x_8801 x_8800
826 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
827 h_Kswitch h_Kcall x_8800)
828 | Kdowhile (x_8805, x_8804, x_8803) ->
829 h_Kdowhile x_8805 x_8804 x_8803
830 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
831 h_Kswitch h_Kcall x_8803)
832 | Kfor2 (x_8809, x_8808, x_8807, x_8806) ->
833 h_Kfor2 x_8809 x_8808 x_8807 x_8806
834 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
835 h_Kswitch h_Kcall x_8806)
836 | Kfor3 (x_8813, x_8812, x_8811, x_8810) ->
837 h_Kfor3 x_8813 x_8812 x_8811 x_8810
838 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
839 h_Kswitch h_Kcall x_8810)
842 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
843 h_Kswitch h_Kcall x_8814)
844 | Kcall (x_8818, x_8817, x_8816, x_8815) ->
845 h_Kcall x_8818 x_8817 x_8816 x_8815
846 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
847 h_Kswitch h_Kcall x_8815)
849 (** val cont_rect_Type2 :
850 'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
851 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
852 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
853 Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
854 (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
855 'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
856 Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
857 -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
858 let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
860 | Kseq (x_8829, x_8828) ->
862 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
863 h_Kswitch h_Kcall x_8828)
864 | Kwhile (x_8832, x_8831, x_8830) ->
865 h_Kwhile x_8832 x_8831 x_8830
866 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
867 h_Kswitch h_Kcall x_8830)
868 | Kdowhile (x_8835, x_8834, x_8833) ->
869 h_Kdowhile x_8835 x_8834 x_8833
870 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
871 h_Kswitch h_Kcall x_8833)
872 | Kfor2 (x_8839, x_8838, x_8837, x_8836) ->
873 h_Kfor2 x_8839 x_8838 x_8837 x_8836
874 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
875 h_Kswitch h_Kcall x_8836)
876 | Kfor3 (x_8843, x_8842, x_8841, x_8840) ->
877 h_Kfor3 x_8843 x_8842 x_8841 x_8840
878 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
879 h_Kswitch h_Kcall x_8840)
882 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
883 h_Kswitch h_Kcall x_8844)
884 | Kcall (x_8848, x_8847, x_8846, x_8845) ->
885 h_Kcall x_8848 x_8847 x_8846 x_8845
886 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
887 h_Kswitch h_Kcall x_8845)
889 (** val cont_rect_Type1 :
890 'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
891 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
892 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
893 Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
894 (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
895 'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
896 Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
897 -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
898 let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
900 | Kseq (x_8859, x_8858) ->
902 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
903 h_Kswitch h_Kcall x_8858)
904 | Kwhile (x_8862, x_8861, x_8860) ->
905 h_Kwhile x_8862 x_8861 x_8860
906 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
907 h_Kswitch h_Kcall x_8860)
908 | Kdowhile (x_8865, x_8864, x_8863) ->
909 h_Kdowhile x_8865 x_8864 x_8863
910 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
911 h_Kswitch h_Kcall x_8863)
912 | Kfor2 (x_8869, x_8868, x_8867, x_8866) ->
913 h_Kfor2 x_8869 x_8868 x_8867 x_8866
914 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
915 h_Kswitch h_Kcall x_8866)
916 | Kfor3 (x_8873, x_8872, x_8871, x_8870) ->
917 h_Kfor3 x_8873 x_8872 x_8871 x_8870
918 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
919 h_Kswitch h_Kcall x_8870)
922 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
923 h_Kswitch h_Kcall x_8874)
924 | Kcall (x_8878, x_8877, x_8876, x_8875) ->
925 h_Kcall x_8878 x_8877 x_8876 x_8875
926 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
927 h_Kswitch h_Kcall x_8875)
929 (** val cont_rect_Type0 :
930 'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
931 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
932 Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
933 Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
934 (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
935 'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
936 Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
937 -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
938 let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
940 | Kseq (x_8889, x_8888) ->
942 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
943 h_Kswitch h_Kcall x_8888)
944 | Kwhile (x_8892, x_8891, x_8890) ->
945 h_Kwhile x_8892 x_8891 x_8890
946 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
947 h_Kswitch h_Kcall x_8890)
948 | Kdowhile (x_8895, x_8894, x_8893) ->
949 h_Kdowhile x_8895 x_8894 x_8893
950 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
951 h_Kswitch h_Kcall x_8893)
952 | Kfor2 (x_8899, x_8898, x_8897, x_8896) ->
953 h_Kfor2 x_8899 x_8898 x_8897 x_8896
954 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
955 h_Kswitch h_Kcall x_8896)
956 | Kfor3 (x_8903, x_8902, x_8901, x_8900) ->
957 h_Kfor3 x_8903 x_8902 x_8901 x_8900
958 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
959 h_Kswitch h_Kcall x_8900)
962 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
963 h_Kswitch h_Kcall x_8904)
964 | Kcall (x_8908, x_8907, x_8906, x_8905) ->
965 h_Kcall x_8908 x_8907 x_8906 x_8905
966 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
967 h_Kswitch h_Kcall x_8905)
969 (** val cont_inv_rect_Type4 :
970 cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
971 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
972 -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
973 __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
974 cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
975 -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
976 -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
977 Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
978 cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
979 let cont_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
980 let hcut = cont_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
982 (** val cont_inv_rect_Type3 :
983 cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
984 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
985 -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
986 __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
987 cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
988 -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
989 -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
990 Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
991 cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
992 let cont_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
993 let hcut = cont_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
995 (** val cont_inv_rect_Type2 :
996 cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
997 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
998 -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
999 __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1000 cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1001 -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1002 -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1003 Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1004 cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1005 let cont_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1006 let hcut = cont_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1008 (** val cont_inv_rect_Type1 :
1009 cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1010 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1011 -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1012 __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1013 cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1014 -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1015 -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1016 Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1017 cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1018 let cont_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1019 let hcut = cont_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1021 (** val cont_inv_rect_Type0 :
1022 cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1023 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1024 -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1025 __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1026 cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1027 -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1028 -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1029 Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1030 cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1031 let cont_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1032 let hcut = cont_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1034 (** val cont_discr : cont -> cont -> __ **)
1035 let cont_discr x y =
1036 Logic.eq_rect_Type2 x
1038 | Kstop -> Obj.magic (fun _ dH -> dH)
1039 | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1040 | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1041 | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1042 | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1043 | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1044 | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1045 | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1047 (** val cont_jmdiscr : cont -> cont -> __ **)
1048 let cont_jmdiscr x y =
1049 Logic.eq_rect_Type2 x
1051 | Kstop -> Obj.magic (fun _ dH -> dH)
1052 | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1053 | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1054 | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1055 | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1056 | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1057 | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1058 | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1060 (** val call_cont : cont -> cont **)
1061 let rec call_cont k = match k with
1063 | Kseq (s, k0) -> call_cont k0
1064 | Kwhile (e, s, k0) -> call_cont k0
1065 | Kdowhile (e, s, k0) -> call_cont k0
1066 | Kfor2 (e2, e3, s, k0) -> call_cont k0
1067 | Kfor3 (e2, e3, s, k0) -> call_cont k0
1068 | Kswitch k0 -> call_cont k0
1069 | Kcall (x, x0, x1, x2) -> k
1072 | State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem
1073 | Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
1075 | Returnstate of Values.val0 * cont * GenMem.mem
1076 | Finalstate of Integers.int
1078 (** val state_rect_Type4 :
1079 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1080 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1081 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1082 -> (Integers.int -> 'a1) -> state -> 'a1 **)
1083 let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
1084 | State (f, s, k, e, m) -> h_State f s k e m
1085 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1086 | Returnstate (res, k, m) -> h_Returnstate res k m
1087 | Finalstate r -> h_Finalstate r
1089 (** val state_rect_Type5 :
1090 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1091 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1092 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1093 -> (Integers.int -> 'a1) -> state -> 'a1 **)
1094 let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
1095 | State (f, s, k, e, m) -> h_State f s k e m
1096 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1097 | Returnstate (res, k, m) -> h_Returnstate res k m
1098 | Finalstate r -> h_Finalstate r
1100 (** val state_rect_Type3 :
1101 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1102 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1103 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1104 -> (Integers.int -> 'a1) -> state -> 'a1 **)
1105 let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
1106 | State (f, s, k, e, m) -> h_State f s k e m
1107 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1108 | Returnstate (res, k, m) -> h_Returnstate res k m
1109 | Finalstate r -> h_Finalstate r
1111 (** val state_rect_Type2 :
1112 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1113 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1114 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1115 -> (Integers.int -> 'a1) -> state -> 'a1 **)
1116 let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
1117 | State (f, s, k, e, m) -> h_State f s k e m
1118 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1119 | Returnstate (res, k, m) -> h_Returnstate res k m
1120 | Finalstate r -> h_Finalstate r
1122 (** val state_rect_Type1 :
1123 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1124 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1125 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1126 -> (Integers.int -> 'a1) -> state -> 'a1 **)
1127 let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
1128 | State (f, s, k, e, m) -> h_State f s k e m
1129 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1130 | Returnstate (res, k, m) -> h_Returnstate res k m
1131 | Finalstate r -> h_Finalstate r
1133 (** val state_rect_Type0 :
1134 (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1135 'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1136 cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1137 -> (Integers.int -> 'a1) -> state -> 'a1 **)
1138 let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
1139 | State (f, s, k, e, m) -> h_State f s k e m
1140 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1141 | Returnstate (res, k, m) -> h_Returnstate res k m
1142 | Finalstate r -> h_Finalstate r
1144 (** val state_inv_rect_Type4 :
1145 state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1146 GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1147 Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1148 -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1149 let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
1150 let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
1152 (** val state_inv_rect_Type3 :
1153 state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1154 GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1155 Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1156 -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1157 let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
1158 let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
1160 (** val state_inv_rect_Type2 :
1161 state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1162 GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1163 Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1164 -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1165 let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
1166 let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
1168 (** val state_inv_rect_Type1 :
1169 state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1170 GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1171 Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1172 -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1173 let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
1174 let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
1176 (** val state_inv_rect_Type0 :
1177 state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1178 GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1179 Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1180 -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1181 let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
1182 let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
1184 (** val state_discr : state -> state -> __ **)
1185 let state_discr x y =
1186 Logic.eq_rect_Type2 x
1188 | State (a0, a1, a2, a3, a4) ->
1189 Obj.magic (fun _ dH -> dH __ __ __ __ __)
1190 | Callstate (a0, a1, a2, a3, a4) ->
1191 Obj.magic (fun _ dH -> dH __ __ __ __ __)
1192 | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1193 | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1195 (** val state_jmdiscr : state -> state -> __ **)
1196 let state_jmdiscr x y =
1197 Logic.eq_rect_Type2 x
1199 | State (a0, a1, a2, a3, a4) ->
1200 Obj.magic (fun _ dH -> dH __ __ __ __ __)
1201 | Callstate (a0, a1, a2, a3, a4) ->
1202 Obj.magic (fun _ dH -> dH __ __ __ __ __)
1203 | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1204 | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1206 (** val find_label :
1207 Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
1208 Types.prod Types.option **)
1209 let rec find_label lbl s k =
1211 | Csyntax.Sskip -> Types.None
1212 | Csyntax.Sassign (x, x0) -> Types.None
1213 | Csyntax.Scall (x, x0, x1) -> Types.None
1214 | Csyntax.Ssequence (s1, s2) ->
1215 (match find_label lbl s1 (Kseq (s2, k)) with
1216 | Types.None -> find_label lbl s2 k
1217 | Types.Some sk -> Types.Some sk)
1218 | Csyntax.Sifthenelse (a, s1, s2) ->
1219 (match find_label lbl s1 k with
1220 | Types.None -> find_label lbl s2 k
1221 | Types.Some sk -> Types.Some sk)
1222 | Csyntax.Swhile (a, s1) -> find_label lbl s1 (Kwhile (a, s1, k))
1223 | Csyntax.Sdowhile (a, s1) -> find_label lbl s1 (Kdowhile (a, s1, k))
1224 | Csyntax.Sfor (a1, a2, a3, s1) ->
1225 (match find_label lbl a1 (Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3,
1228 (match find_label lbl s1 (Kfor2 (a2, a3, s1, k)) with
1229 | Types.None -> find_label lbl a3 (Kfor3 (a2, a3, s1, k))
1230 | Types.Some sk -> Types.Some sk)
1231 | Types.Some sk -> Types.Some sk)
1232 | Csyntax.Sbreak -> Types.None
1233 | Csyntax.Scontinue -> Types.None
1234 | Csyntax.Sreturn x -> Types.None
1235 | Csyntax.Sswitch (e, sl) -> find_label_ls lbl sl (Kswitch k)
1236 | Csyntax.Slabel (lbl', s') ->
1237 (match AST.ident_eq lbl lbl' with
1238 | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
1239 | Types.Inr _ -> find_label lbl s' k)
1240 | Csyntax.Sgoto x -> Types.None
1241 | Csyntax.Scost (c, s') -> find_label lbl s' k
1242 (** val find_label_ls :
1243 Csyntax.label -> Csyntax.labeled_statements -> cont ->
1244 (Csyntax.statement, cont) Types.prod Types.option **)
1245 and find_label_ls lbl sl k =
1247 | Csyntax.LSdefault s -> find_label lbl s k
1248 | Csyntax.LScase (x, x0, s, sl') ->
1249 (match find_label lbl s (Kseq ((seq_of_labeled_statement sl'), k)) with
1250 | Types.None -> find_label_ls lbl sl' k
1251 | Types.Some sk -> Types.Some sk)
1253 (** val fun_typeof : Csyntax.expr -> Csyntax.type0 **)
1255 match Csyntax.typeof e with
1256 | Csyntax.Tvoid -> Csyntax.Tvoid
1257 | Csyntax.Tint (a, b) -> Csyntax.Tint (a, b)
1258 | Csyntax.Tpointer ty -> ty
1259 | Csyntax.Tarray (a, b) -> Csyntax.Tarray (a, b)
1260 | Csyntax.Tfunction (a, b) -> Csyntax.Tfunction (a, b)
1261 | Csyntax.Tstruct (a, b) -> Csyntax.Tstruct (a, b)
1262 | Csyntax.Tunion (a, b) -> Csyntax.Tunion (a, b)
1263 | Csyntax.Tcomp_ptr a -> Csyntax.Tcomp_ptr a