fact: Definition f_make_tinfo := {| fn_return := (tptr (Tstruct _thread_info noattr)); fn_callconv := cc_default; fn_params := nil; fn_vars := nil; fn_temps := ((_h, (tptr (Tstruct _heap noattr))) :: (_tinfo, (tptr (Tstruct _thread_info noattr))) :: (_t'2, (tptr tvoid)) :: (_t'1, (tptr (Tstruct _heap noattr))) :: (_t'4, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'3, (tptr (talignas 3%N (tptr tvoid)))) :: nil); fn_body := (Ssequence (Ssequence (Scall (Some _t'1) (Evar _create_heap (Tfunction Tnil (tptr (Tstruct _heap noattr)) cc_default)) nil) (Sset _h (Etempvar _t'1 (tptr (Tstruct _heap noattr))))) (Ssequence (Ssequence (Scall (Some _t'2) (Evar _malloc (Tfunction (Tcons tulong Tnil) (tptr tvoid) cc_default)) ((Esizeof (Tstruct _thread_info noattr) tulong) :: nil)) (Sset _tinfo (Ecast (Etempvar _t'2 (tptr tvoid)) (tptr (Tstruct _thread_info noattr))))) (Ssequence (Sifthenelse (Eunop Onotbool (Etempvar _tinfo (tptr (Tstruct _thread_info noattr))) tint) (Scall None (Evar _abort_with (Tfunction (Tcons (tptr tschar) Tnil) tvoid cc_default)) ((Evar ___stringlit_9 (tarray tschar 39)) :: nil)) Sskip) (Ssequence (Sassign (Efield (Ederef (Etempvar _tinfo (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr))) (Etempvar _h (tptr (Tstruct _heap noattr)))) (Ssequence (Ssequence (Sset _t'4 (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))))) (Sassign (Efield (Ederef (Etempvar _tinfo (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _alloc (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'4 (tptr (talignas 3%N (tptr tvoid)))))) (Ssequence (Ssequence (Sset _t'3 (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))))) (Sassign (Efield (Ederef (Etempvar _tinfo (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _limit (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'3 (tptr (talignas 3%N (tptr tvoid)))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _tinfo (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _fp (tptr (Tstruct _stack_frame noattr))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid))) (Ssequence (Sassign (Efield (Ederef (Etempvar _tinfo (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _nalloc tulong) (Econst_int (Int.repr 0) tint)) (Ssequence (Sassign (Efield (Ederef (Etempvar _tinfo (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _odata (tptr tvoid)) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid))) (Sreturn (Some (Etempvar _tinfo (tptr (Tstruct _thread_info noattr)))))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)