63 open Hints_declaration
131 (** val reduce_bits :
132 Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
133 BitVector.bitVector Types.option **)
134 let rec reduce_bits n m exp v =
136 | Nat.O -> (fun v0 -> Types.Some v0)
139 match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp with
141 reduce_bits n' m exp (Vector.tail (Nat.plus n' (Nat.S m)) v0)
142 | Bool.False -> Types.None)) v
144 (** val pred_bitsize_of_intsize : AST.intsize -> Nat.nat **)
145 let pred_bitsize_of_intsize sz =
146 Nat.pred (AST.bitsize_of_intsize sz)
148 (** val signed : AST.signedness -> Bool.bool **)
149 let signed = function
150 | AST.Signed -> Bool.True
151 | AST.Unsigned -> Bool.False
153 (** val simplify_int :
154 AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness ->
155 AST.bvint -> AST.bvint Types.option **)
156 let rec simplify_int sz sz' sg sg' i =
158 Bool.andb (signed sg)
160 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
162 (Nat.times (AST.pred_size_intsize sz) (Nat.S (Nat.S (Nat.S (Nat.S
163 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) i)
165 (match Extranat.nat_compare (pred_bitsize_of_intsize sz)
166 (pred_bitsize_of_intsize sz') with
167 | Extranat.Nat_lt (x, x0) -> (fun i0 -> Types.None)
168 | Extranat.Nat_eq x -> (fun i0 -> Types.Some i0)
169 | Extranat.Nat_gt (x, y) ->
171 match reduce_bits (Nat.S x) y bit i0 with
172 | Types.None -> Types.None
174 (match signed sg' with
176 (match BitVector.eq_b bit (Vector.head' y i') with
177 | Bool.True -> Types.Some i'
178 | Bool.False -> Types.None)
179 | Bool.False -> Types.Some i'))) i
181 (** val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **)
182 let size_lt_dec = function
186 | AST.I8 -> Types.Inr __
187 | AST.I16 -> Types.Inl __
188 | AST.I32 -> Types.Inl __)
192 | AST.I8 -> Types.Inr __
193 | AST.I16 -> Types.Inr __
194 | AST.I32 -> Types.Inl __)
198 | AST.I8 -> Types.Inr __
199 | AST.I16 -> Types.Inr __
200 | AST.I32 -> Types.Inr __)
202 (** val size_not_lt_to_ge :
203 AST.intsize -> AST.intsize -> (__, __) Types.sum **)
204 let size_not_lt_to_ge clearme sz2 =
209 | AST.I8 -> (fun _ -> Types.Inl __)
210 | AST.I16 -> (fun _ -> Types.Inr __)
211 | AST.I32 -> (fun _ -> Types.Inr __))
215 | AST.I8 -> (fun _ -> Types.Inr __)
216 | AST.I16 -> (fun _ -> Types.Inl __)
217 | AST.I32 -> (fun _ -> Types.Inr __))
221 | AST.I8 -> (fun _ -> Types.Inr __)
222 | AST.I16 -> (fun _ -> Types.Inr __)
223 | AST.I32 -> (fun _ -> Types.Inl __))) sz2 __
225 (** val sign_eq_dect :
226 AST.signedness -> AST.signedness -> (__, __) Types.sum **)
227 let sign_eq_dect = function
231 | AST.Signed -> TypeComparison.sg_eq_dec AST.Signed AST.Signed
232 | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Signed AST.Unsigned)
236 | AST.Signed -> TypeComparison.sg_eq_dec AST.Unsigned AST.Signed
237 | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Unsigned AST.Unsigned)
239 (** val necessary_conditions :
240 AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness ->
242 let necessary_conditions src_sz src_sg target_sz target_sg =
243 match size_lt_dec target_sz src_sz with
244 | Types.Inl _ -> Bool.True
246 (match TypeComparison.sz_eq_dec target_sz src_sz with
248 (match sign_eq_dect src_sg target_sg with
249 | Types.Inl _ -> Bool.False
250 | Types.Inr _ -> Bool.True)
251 | Types.Inr _ -> Bool.False)
253 (** val assert_int_value :
254 Values.val0 Types.option -> AST.intsize -> BitVector.bitVector
256 let rec assert_int_value v expected_size =
258 | Types.None -> Types.None
261 | Values.Vundef -> Types.None
262 | Values.Vint (sz, i) ->
263 (match TypeComparison.sz_eq_dec sz expected_size with
266 (Extralib.eq_rect_Type0_r expected_size (fun i0 -> i0) sz i)
267 | Types.Inr _ -> Types.None)
268 | Values.Vnull -> Types.None
269 | Values.Vptr x -> Types.None)
271 (** val binop_simplifiable : Csyntax.binary_operation -> Bool.bool **)
272 let binop_simplifiable = function
273 | Csyntax.Oadd -> Bool.True
274 | Csyntax.Osub -> Bool.True
275 | Csyntax.Omul -> Bool.False
276 | Csyntax.Odiv -> Bool.False
277 | Csyntax.Omod -> Bool.False
278 | Csyntax.Oand -> Bool.False
279 | Csyntax.Oor -> Bool.False
280 | Csyntax.Oxor -> Bool.False
281 | Csyntax.Oshl -> Bool.False
282 | Csyntax.Oshr -> Bool.False
283 | Csyntax.Oeq -> Bool.False
284 | Csyntax.One -> Bool.False
285 | Csyntax.Olt -> Bool.False
286 | Csyntax.Ogt -> Bool.False
287 | Csyntax.Ole -> Bool.False
288 | Csyntax.Oge -> Bool.False
290 (** val simplify_expr :
291 Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool,
292 Csyntax.expr) Types.prod Types.sig0 **)
293 let rec simplify_expr e target_sz target_sg =
294 (let Csyntax.Expr (ed, ty) = e in
297 | Csyntax.Econst_int (cst_sz, i) ->
301 (fun _ -> { Types.fst = Bool.False; Types.snd = e })
302 | Csyntax.Tint (ty_sz, sg) ->
304 match TypeComparison.sz_eq_dec cst_sz ty_sz with
306 (match TypeComparison.type_eq_dec ty (Csyntax.Tint (target_sz,
308 | Types.Inl _ -> { Types.fst = Bool.True; Types.snd = e }
310 (match simplify_int cst_sz target_sz sg target_sg i with
312 (fun _ -> { Types.fst = Bool.False; Types.snd = e })
314 (fun _ -> { Types.fst = Bool.True; Types.snd =
315 (Csyntax.Expr ((Csyntax.Econst_int (target_sz, i')),
316 (Csyntax.Tint (target_sz, target_sg)))) })) __)
317 | Types.Inr _ -> { Types.fst = Bool.False; Types.snd = e })
318 | Csyntax.Tpointer x ->
319 (fun _ -> { Types.fst = Bool.False; Types.snd = e })
320 | Csyntax.Tarray (x, x0) ->
321 (fun _ -> { Types.fst = Bool.False; Types.snd = e })
322 | Csyntax.Tfunction (x, x0) ->
323 (fun _ -> { Types.fst = Bool.False; Types.snd = e })
324 | Csyntax.Tstruct (x, x0) ->
325 (fun _ -> { Types.fst = Bool.False; Types.snd = e })
326 | Csyntax.Tunion (x, x0) ->
327 (fun _ -> { Types.fst = Bool.False; Types.snd = e })
328 | Csyntax.Tcomp_ptr x ->
329 (fun _ -> { Types.fst = Bool.False; Types.snd = e })) __)
331 (fun _ -> { Types.fst =
332 (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
333 Types.snd = (Csyntax.Expr (ed, ty)) })
334 | Csyntax.Ederef e1 ->
336 (let e2 = simplify_inside e1 in
337 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
338 ((Csyntax.Ederef e2), ty)) })) __)
339 | Csyntax.Eaddrof e1 ->
341 (let e2 = simplify_inside e1 in
342 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
343 ((Csyntax.Eaddrof e2), ty)) })) __)
344 | Csyntax.Eunop (op, e1) ->
346 (let e2 = simplify_inside e1 in
347 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
348 ((Csyntax.Eunop (op, e2)), ty)) })) __)
349 | Csyntax.Ebinop (op, lhs, rhs) ->
351 (match binop_simplifiable op with
354 match TypeComparison.assert_type_eq ty (Csyntax.typeof lhs) with
356 (match TypeComparison.assert_type_eq (Csyntax.typeof lhs)
357 (Csyntax.typeof rhs) with
359 (let eta2033 = simplify_expr lhs target_sz target_sg in
361 (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
365 (let eta2032 = simplify_expr rhs target_sz target_sg in
367 (let { Types.fst = desired_type_rhs; Types.snd =
371 (match Bool.andb desired_type_lhs desired_type_rhs with
373 (fun _ -> { Types.fst = Bool.True; Types.snd =
374 (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)),
375 (Csyntax.Tint (target_sz, target_sg)))) })
378 (let lhs10 = simplify_inside lhs in
380 (let rhs10 = simplify_inside rhs in
381 (fun _ -> { Types.fst = Bool.False; Types.snd =
382 (Csyntax.Expr ((Csyntax.Ebinop (op, lhs10,
383 rhs10)), ty)) })) __)) __)) __)) __)) __)) __))
386 (let lhs1 = simplify_inside lhs in
388 (let rhs1 = simplify_inside rhs in
389 (fun _ -> { Types.fst = Bool.False; Types.snd =
390 (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)),
393 (let lhs1 = simplify_inside lhs in
395 (let rhs1 = simplify_inside rhs in
396 (fun _ -> { Types.fst = Bool.False; Types.snd =
397 (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) }))
401 (let lhs1 = simplify_inside lhs in
403 (let rhs1 = simplify_inside rhs in
404 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
405 ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) })) __)) __)) __)
406 | Csyntax.Ecast (cast_ty, castee) ->
411 (let castee1 = simplify_inside castee in
412 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
413 ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
414 | Csyntax.Tint (cast_sz, cast_sg) ->
416 match TypeComparison.type_eq_dec ty cast_ty with
418 (match necessary_conditions cast_sz cast_sg target_sz target_sg with
421 (let eta2035 = simplify_expr castee target_sz target_sg in
423 (let { Types.fst = desired_type; Types.snd = castee1 } =
427 (match desired_type with
429 (fun _ -> { Types.fst = Bool.True; Types.snd =
433 (let eta2034 = simplify_expr castee cast_sz cast_sg
436 (let { Types.fst = desired_type2; Types.snd =
440 (match desired_type2 with
442 (fun _ -> { Types.fst = Bool.False;
443 Types.snd = castee2 })
445 (fun _ -> { Types.fst = Bool.False;
446 Types.snd = (Csyntax.Expr ((Csyntax.Ecast
447 (ty, castee2)), cast_ty)) })) __)) __)) __))
451 (let eta2036 = simplify_expr castee cast_sz cast_sg in
453 (let { Types.fst = desired_type2; Types.snd =
457 (match desired_type2 with
459 (fun _ -> { Types.fst = Bool.False; Types.snd =
462 (fun _ -> { Types.fst = Bool.False; Types.snd =
463 (Csyntax.Expr ((Csyntax.Ecast (ty, castee2)),
464 cast_ty)) })) __)) __)) __)) __
466 (let castee1 = simplify_inside castee in
467 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
468 ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
469 | Csyntax.Tpointer x ->
471 (let castee1 = simplify_inside castee in
472 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
473 ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
474 | Csyntax.Tarray (x, x0) ->
476 (let castee1 = simplify_inside castee in
477 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
478 ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
479 | Csyntax.Tfunction (x, x0) ->
481 (let castee1 = simplify_inside castee in
482 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
483 ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
484 | Csyntax.Tstruct (x, x0) ->
486 (let castee1 = simplify_inside castee in
487 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
488 ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
489 | Csyntax.Tunion (x, x0) ->
491 (let castee1 = simplify_inside castee in
492 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
493 ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
494 | Csyntax.Tcomp_ptr x ->
496 (let castee1 = simplify_inside castee in
497 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
498 ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)) __)
499 | Csyntax.Econdition (cond, iftrue, iffalse) ->
501 (let cond1 = simplify_inside cond in
503 match TypeComparison.assert_type_eq ty (Csyntax.typeof iftrue) with
505 (match TypeComparison.assert_type_eq (Csyntax.typeof iftrue)
506 (Csyntax.typeof iffalse) with
508 (let eta2038 = simplify_expr iftrue target_sz target_sg in
510 (let { Types.fst = desired_true; Types.snd = iftrue1 } =
514 (let eta2037 = simplify_expr iffalse target_sz target_sg in
516 (let { Types.fst = desired_false; Types.snd = iffalse1 } =
520 (match Bool.andb desired_true desired_false with
522 (fun _ -> { Types.fst = Bool.True; Types.snd =
523 (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
524 iffalse1)), (Csyntax.Tint (target_sz, target_sg)))) })
527 (let iftrue10 = simplify_inside iftrue in
529 (let iffalse10 = simplify_inside iffalse in
530 (fun _ -> { Types.fst = Bool.False; Types.snd =
531 (Csyntax.Expr ((Csyntax.Econdition (cond1,
532 iftrue10, iffalse10)), ty)) })) __)) __)) __)) __))
535 (let iftrue1 = simplify_inside iftrue in
537 (let iffalse1 = simplify_inside iffalse in
538 (fun _ -> { Types.fst = Bool.False; Types.snd =
539 (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
540 iffalse1)), ty)) })) __)) __)
542 (let iftrue1 = simplify_inside iftrue in
544 (let iffalse1 = simplify_inside iffalse in
545 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
546 ((Csyntax.Econdition (cond1, iftrue1, iffalse1)), ty)) })) __))
548 | Csyntax.Eandbool (lhs, rhs) ->
550 (let lhs1 = simplify_inside lhs in
552 (let rhs1 = simplify_inside rhs in
553 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
554 ((Csyntax.Eandbool (lhs1, rhs1)), ty)) })) __)) __)
555 | Csyntax.Eorbool (lhs, rhs) ->
557 (let lhs1 = simplify_inside lhs in
559 (let rhs1 = simplify_inside rhs in
560 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
561 ((Csyntax.Eorbool (lhs1, rhs1)), ty)) })) __)) __)
562 | Csyntax.Esizeof t ->
563 (fun _ -> { Types.fst =
564 (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
565 Types.snd = (Csyntax.Expr (ed, ty)) })
566 | Csyntax.Efield (rec_expr, f) ->
568 (let rec_expr1 = simplify_inside rec_expr in
569 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
570 ((Csyntax.Efield (rec_expr1, f)), ty)) })) __)
571 | Csyntax.Ecost (l, e1) ->
573 match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
575 (let eta2039 = simplify_expr e1 target_sz target_sg in
577 (let { Types.fst = desired_type; Types.snd = e2 } = eta2039 in
578 (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
579 ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
581 (let e2 = simplify_inside e1 in
582 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
583 ((Csyntax.Ecost (l, e2)), ty)) })) __)) __)) __
584 (** val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0 **)
585 and simplify_inside e =
586 (let Csyntax.Expr (ed, ty) = e in
589 | Csyntax.Econst_int (x, x0) -> (fun _ -> e)
590 | Csyntax.Evar x -> (fun _ -> e)
591 | Csyntax.Ederef e1 ->
593 (let e2 = simplify_inside e1 in
594 (fun _ -> Csyntax.Expr ((Csyntax.Ederef e2), ty))) __)
595 | Csyntax.Eaddrof e1 ->
597 (let e2 = simplify_inside e1 in
598 (fun _ -> Csyntax.Expr ((Csyntax.Eaddrof e2), ty))) __)
599 | Csyntax.Eunop (op, e1) ->
601 (let e2 = simplify_inside e1 in
602 (fun _ -> Csyntax.Expr ((Csyntax.Eunop (op, e2)), ty))) __)
603 | Csyntax.Ebinop (op, lhs, rhs) ->
605 (let lhs1 = simplify_inside lhs in
607 (let rhs1 = simplify_inside rhs in
608 (fun _ -> Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)))
610 | Csyntax.Ecast (cast_ty, castee) ->
612 match TypeComparison.type_eq_dec ty cast_ty with
615 | Csyntax.Tvoid -> (fun _ -> e)
616 | Csyntax.Tint (cast_sz, cast_sg) ->
618 (let eta2040 = simplify_expr castee cast_sz cast_sg in
620 (let { Types.fst = success; Types.snd = castee1 } = eta2040
624 | Bool.True -> (fun _ -> castee1)
626 (fun _ -> Csyntax.Expr ((Csyntax.Ecast (cast_ty,
627 castee1)), ty))) __)) __)) __)
628 | Csyntax.Tpointer x -> (fun _ -> e)
629 | Csyntax.Tarray (x, x0) -> (fun _ -> e)
630 | Csyntax.Tfunction (x, x0) -> (fun _ -> e)
631 | Csyntax.Tstruct (x, x0) -> (fun _ -> e)
632 | Csyntax.Tunion (x, x0) -> (fun _ -> e)
633 | Csyntax.Tcomp_ptr x -> (fun _ -> e)) __
635 | Csyntax.Econdition (cond, iftrue, iffalse) ->
637 (let cond1 = simplify_inside cond in
639 (let iftrue1 = simplify_inside iftrue in
641 (let iffalse1 = simplify_inside iffalse in
642 (fun _ -> Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
643 iffalse1)), ty))) __)) __)) __)
644 | Csyntax.Eandbool (lhs, rhs) ->
646 (let lhs1 = simplify_inside lhs in
648 (let rhs1 = simplify_inside rhs in
649 (fun _ -> Csyntax.Expr ((Csyntax.Eandbool (lhs1, rhs1)), ty))) __))
651 | Csyntax.Eorbool (lhs, rhs) ->
653 (let lhs1 = simplify_inside lhs in
655 (let rhs1 = simplify_inside rhs in
656 (fun _ -> Csyntax.Expr ((Csyntax.Eorbool (lhs1, rhs1)), ty))) __))
658 | Csyntax.Esizeof x -> (fun _ -> e)
659 | Csyntax.Efield (rec_expr, f) ->
661 (let rec_expr1 = simplify_inside rec_expr in
662 (fun _ -> Csyntax.Expr ((Csyntax.Efield (rec_expr1, f)), ty))) __)
663 | Csyntax.Ecost (l, e1) ->
665 (let e2 = simplify_inside e1 in
666 (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e2)), ty))) __)) __)) __
668 (** val simplify_e : Csyntax.expr -> Csyntax.expr **)
670 Types.pi1 (simplify_inside e)
672 (** val simplify_statement : Csyntax.statement -> Csyntax.statement **)
673 let rec simplify_statement = function
674 | Csyntax.Sskip -> Csyntax.Sskip
675 | Csyntax.Sassign (e1, e2) ->
676 Csyntax.Sassign ((simplify_e e1), (simplify_e e2))
677 | Csyntax.Scall (eo, e, es) ->
678 Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e),
679 (List.map simplify_e es))
680 | Csyntax.Ssequence (s1, s2) ->
681 Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2))
682 | Csyntax.Sifthenelse (e, s1, s2) ->
683 Csyntax.Sifthenelse ((simplify_e e), (simplify_statement s1),
684 (simplify_statement s2))
685 | Csyntax.Swhile (e, s1) ->
686 Csyntax.Swhile ((simplify_e e), (simplify_statement s1))
687 | Csyntax.Sdowhile (e, s1) ->
688 Csyntax.Sdowhile ((simplify_e e), (simplify_statement s1))
689 | Csyntax.Sfor (s1, e, s2, s3) ->
690 Csyntax.Sfor ((simplify_statement s1), (simplify_e e),
691 (simplify_statement s2), (simplify_statement s3))
692 | Csyntax.Sbreak -> Csyntax.Sbreak
693 | Csyntax.Scontinue -> Csyntax.Scontinue
694 | Csyntax.Sreturn eo -> Csyntax.Sreturn (Types.option_map simplify_e eo)
695 | Csyntax.Sswitch (e, ls) ->
696 Csyntax.Sswitch ((simplify_e e), (simplify_ls ls))
697 | Csyntax.Slabel (l, s1) -> Csyntax.Slabel (l, (simplify_statement s1))
698 | Csyntax.Sgoto l -> Csyntax.Sgoto l
699 | Csyntax.Scost (l, s1) -> Csyntax.Scost (l, (simplify_statement s1))
700 (** val simplify_ls :
701 Csyntax.labeled_statements -> Csyntax.labeled_statements **)
702 and simplify_ls = function
703 | Csyntax.LSdefault s -> Csyntax.LSdefault (simplify_statement s)
704 | Csyntax.LScase (sz, i, s, ls') ->
705 Csyntax.LScase (sz, i, (simplify_statement s), (simplify_ls ls'))
707 (** val simplify_function : Csyntax.function0 -> Csyntax.function0 **)
708 let simplify_function f =
709 { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
710 f.Csyntax.fn_params; Csyntax.fn_vars = f.Csyntax.fn_vars;
711 Csyntax.fn_body = (simplify_statement f.Csyntax.fn_body) }
713 (** val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef **)
714 let simplify_fundef f = match f with
715 | Csyntax.CL_Internal f0 -> Csyntax.CL_Internal (simplify_function f0)
716 | Csyntax.CL_External (x, x0, x1) -> f
718 (** val simplify_program :
719 Csyntax.clight_program -> Csyntax.clight_program **)
720 let simplify_program p =
721 AST.transform_program p (fun x -> simplify_fundef)