fact: Definition f_resume := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_ti, (tptr (Tstruct _thread_info noattr))) :: nil); fn_vars := nil; fn_temps := ((_h, (tptr (Tstruct _heap noattr))) :: (_lo, (tptr (talignas 3%N (tptr tvoid)))) :: (_hi, (tptr (talignas 3%N (tptr tvoid)))) :: (_num_allocs, tulong) :: nil); fn_body := (Ssequence (Sset _h (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr)))) (Ssequence (Sset _num_allocs (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _nalloc tulong)) (Ssequence (Sifthenelse (Etempvar _h (tptr (Tstruct _heap noattr))) Sskip (Ssequence (Scall None (Evar _printf (Tfunction (Tcons (tptr tschar) Tnil) tint {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ((Evar ___stringlit_5 (tarray tschar 30)) :: (Evar ___stringlit_4 (tarray tschar 5)) :: (Econst_int (Int.repr 377) tint) :: (Evar ___stringlit_10 (tarray tschar 2)) :: nil)) (Scall None (Evar _abort (Tfunction Tnil tvoid cc_default)) nil))) (Ssequence (Sset _lo (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 45)) (Econst_int (Int.repr 0) tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _hi (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 45)) (Econst_int (Int.repr 0) tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sifthenelse (Ebinop Olt (Ebinop Osub (Etempvar _hi (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _lo (tptr (talignas 3%N (tptr tvoid)))) tlong) (Etempvar _num_allocs tulong) tint) (Scall None (Evar _abort_with (Tfunction (Tcons (tptr tschar) Tnil) tvoid cc_default)) ((Evar ___stringlit_11 (tarray tschar 48)) :: nil)) Sskip) (Ssequence (Sassign (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _alloc (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _lo (tptr (talignas 3%N (tptr tvoid))))) (Sassign (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _limit (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _hi (tptr (talignas 3%N (tptr tvoid)))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)