fact: Definition f_print_heapsize := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_ti, (tptr (Tstruct _thread_info noattr))) :: nil); fn_vars := nil; fn_temps := ((_i, tint) :: (_allocated, tint) :: (_remembered, tint) :: (_t'1, tint) :: (_t'13, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'12, (tptr (Tstruct _heap noattr))) :: (_t'11, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'10, (tptr (Tstruct _heap noattr))) :: (_t'9, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'8, (tptr (Tstruct _heap noattr))) :: (_t'7, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'6, (tptr (Tstruct _heap noattr))) :: (_t'5, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'4, (tptr (Tstruct _heap noattr))) :: (_t'3, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'2, (tptr (Tstruct _heap noattr))) :: nil); fn_body := (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Ebinop Osub (Ebinop Omul (Econst_int (Int.repr 8) tint) (Esizeof (talignas 3%N (tptr tvoid)) tulong) tulong) (Ebinop Oadd (Ebinop Oadd (Econst_int (Int.repr 2) tint) (Econst_int (Int.repr 3) tint) tint) (Econst_int (Int.repr 16) tint) tint) tulong) tint) Sskip Sbreak) (Ssequence (Ssequence (Sset _t'10 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr)))) (Ssequence (Sset _t'11 (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _t'10 (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 43)) (Etempvar _i tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'12 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr)))) (Ssequence (Sset _t'13 (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _t'12 (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 43)) (Etempvar _i tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Sset _allocated (Ecast (Ebinop Osub (Etempvar _t'11 (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'13 (tptr (talignas 3%N (tptr tvoid)))) tlong) tint)))))) (Ssequence (Ssequence (Sset _t'6 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr)))) (Ssequence (Sset _t'7 (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _t'6 (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 43)) (Etempvar _i tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _rem_limit (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'8 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr)))) (Ssequence (Sset _t'9 (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _t'8 (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 43)) (Etempvar _i tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Sset _remembered (Ecast (Ebinop Osub (Etempvar _t'7 (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'9 (tptr (talignas 3%N (tptr tvoid)))) tlong) tint)))))) (Ssequence (Ssequence (Sifthenelse (Etempvar _allocated tint) (Sset _t'1 (Econst_int (Int.repr 1) tint)) (Sset _t'1 (Ecast (Etempvar _remembered tint) tbool))) (Sifthenelse (Eunop Onotbool (Etempvar _t'1 tint) tint) Scontinue Sskip)) (Ssequence (Scall None (Evar _printf (Tfunction (Tcons (tptr tschar) Tnil) tint {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ((Evar ___stringlit_14 (tarray tschar 16)) :: (Etempvar _i tint) :: nil)) (Ssequence (Ssequence (Sset _t'2 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr)))) (Ssequence (Sset _t'3 (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _t'2 (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 43)) (Etempvar _i tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _rem_limit (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'4 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr)))) (Ssequence (Sset _t'5 (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _t'4 (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 43)) (Etempvar _i tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Scall None (Evar _printf (Tfunction (Tcons (tptr tschar) Tnil) tint {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ((Evar ___stringlit_15 (tarray tschar 12)) :: (Ecast (Ebinop Osub (Etempvar _t'3 (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'5 (tptr (talignas 3%N (tptr tvoid)))) tlong) tint) :: nil)))))) (Ssequence (Scall None (Evar _printf (Tfunction (Tcons (tptr tschar) Tnil) tint {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ((Evar ___stringlit_16 (tarray tschar 17)) :: (Etempvar _allocated tint) :: nil)) (Scall None (Evar _printf (Tfunction (Tcons (tptr tschar) Tnil) tint {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ((Evar ___stringlit_17 (tarray tschar 18)) :: (Etempvar _remembered tint) :: nil))))))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)