fact: Definition f_fiddle := {| fn_return := tint; fn_callconv := cc_default; fn_params := ((_p, (tptr tuint)) :: nil); fn_vars := nil; fn_temps := ((_sum, tuint) :: (_size, tuint) :: (_i, tuint) :: (_tagword, tuint) :: (_t'1, tuint) :: nil); fn_body := (Ssequence (Sset _tagword (Ederef (Ebinop Oadd (Etempvar _p (tptr tuint)) (Eunop Oneg (Econst_int (Int.repr 1) tint) tint) (tptr tuint)) tuint)) (Ssequence (Sset _sum (Ebinop Oand (Etempvar _tagword tuint) (Econst_int (Int.repr 255) tint) tuint)) (Ssequence (Sset _size (Ebinop Oshr (Etempvar _tagword tuint) (Econst_int (Int.repr 10) tint) tuint)) (Ssequence (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tuint) (Etempvar _size tuint) tint) Sskip Sbreak) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _p (tptr tuint)) (Etempvar _i tuint) (tptr tuint)) tuint)) (Sset _sum (Ebinop Oadd (Etempvar _sum tuint) (Etempvar _t'1 tuint) tuint)))) (Sset _i (Ebinop Oadd (Etempvar _i tuint) (Econst_int (Int.repr 1) tint) tuint)))) (Sreturn (Some (Etempvar _sum tuint))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)