fact: Definition f_swim := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_k, tuint) :: (_arr, (tptr (Tstruct _structItem noattr))) :: (_lookup, (tptr tuint)) :: nil); fn_vars := nil; fn_temps := ((_t'2, tint) :: (_t'1, tint) :: nil); fn_body := (Sloop (Ssequence (Ssequence (Sifthenelse (Ebinop Ogt (Etempvar _k tuint) (Econst_int (Int.repr 0) tuint) tint) (Ssequence (Scall (Some _t'2) (Evar _less (Tfunction (Tcons tuint (Tcons tuint (Tcons (tptr (Tstruct _structItem noattr)) Tnil))) tint cc_default)) ((Etempvar _k tuint) :: (Ebinop Odiv (Ebinop Osub (Etempvar _k tuint) (Econst_int (Int.repr 1) tuint) tuint) (Econst_int (Int.repr 2) tuint) tuint) :: (Etempvar _arr (tptr (Tstruct _structItem noattr))) :: nil)) (Sset _t'1 (Ecast (Etempvar _t'2 tint) tbool))) (Sset _t'1 (Econst_int (Int.repr 0) tint))) (Sifthenelse (Etempvar _t'1 tint) Sskip Sbreak)) (Ssequence (Scall None (Evar _exch (Tfunction (Tcons tuint (Tcons tuint (Tcons (tptr (Tstruct _structItem noattr)) (Tcons (tptr tuint) Tnil)))) tvoid cc_default)) ((Etempvar _k tuint) :: (Ebinop Odiv (Ebinop Osub (Etempvar _k tuint) (Econst_int (Int.repr 1) tuint) tuint) (Econst_int (Int.repr 2) tuint) tuint) :: (Etempvar _arr (tptr (Tstruct _structItem noattr))) :: (Etempvar _lookup (tptr tuint)) :: nil)) (Sset _k (Ebinop Odiv (Ebinop Osub (Etempvar _k tuint) (Econst_int (Int.repr 1) tuint) tuint) (Econst_int (Int.repr 2) tuint) tuint)))) Sskip) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)