fact: Definition f_exch := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_j, tuint) :: (_k, tuint) :: (_arr, (tptr (Tstruct _structItem noattr))) :: (_lookup, (tptr tuint)) :: nil); fn_vars := nil; fn_temps := ((_priority, tint) :: (_data, tint) :: (_key1, tuint) :: (_key2, tuint) :: (_t'2, tint) :: (_t'1, tint) :: nil); fn_body := (Ssequence (Sset _priority (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _j tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _priority tint)) (Ssequence (Sset _data (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _j tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _data tint)) (Ssequence (Sset _key1 (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _j tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _key tuint)) (Ssequence (Sset _key2 (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _k tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _key tuint)) (Ssequence (Ssequence (Sset _t'2 (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _k tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _priority tint)) (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _j tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _priority tint) (Etempvar _t'2 tint))) (Ssequence (Ssequence (Sset _t'1 (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _k tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _data tint)) (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _j tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _data tint) (Etempvar _t'1 tint))) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _j tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _key tuint) (Etempvar _key2 tuint)) (Ssequence (Sassign (Ederef (Ebinop Oadd (Etempvar _lookup (tptr tuint)) (Etempvar _key2 tuint) (tptr tuint)) tuint) (Etempvar _j tuint)) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _k tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _priority tint) (Etempvar _priority tint)) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _k tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _data tint) (Etempvar _data tint)) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _k tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _key tuint) (Etempvar _key1 tuint)) (Sassign (Ederef (Ebinop Oadd (Etempvar _lookup (tptr tuint)) (Etempvar _key1 tuint) (tptr tuint)) tuint) (Etempvar _k tuint))))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)