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