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