fact: Definition f_certicoq_modify := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_ti, (tptr (Tstruct _thread_info noattr))) :: (_p_cell, (tptr (talignas 3%N (tptr tvoid)))) :: (_p_val, (talignas 3%N (tptr tvoid))) :: nil); fn_vars := nil; fn_temps := ((_t'2, tint) :: (_t'1, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'5, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'4, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'3, (tptr (talignas 3%N (tptr tvoid)))) :: nil); fn_body := (Ssequence (Ssequence (Sset _t'4 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _alloc (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'5 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Sifthenelse (Ebinop Olt (Etempvar _t'4 (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'5 (tptr (talignas 3%N (tptr tvoid)))) tint) Sskip (Ssequence (Scall None (Evar _printf (Tfunction (Tcons (tptr tschar) Tnil) tint {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ((Evar ___stringlit_4 (tarray tschar 30)) :: (Evar ___stringlit_3 (tarray tschar 11)) :: (Econst_int (Int.repr 523) tint) :: (Evar ___stringlit_13 (tarray tschar 22)) :: nil)) (Scall None (Evar _abort (Tfunction Tnil tvoid cc_default)) nil))))) (Ssequence (Sassign (Ederef (Etempvar _p_cell (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid))) (Etempvar _p_val (talignas 3%N (tptr tvoid)))) (Ssequence (Scall (Some _t'2) (Evar _is_ptr (Tfunction (Tcons (talignas 3%N (tptr tvoid)) Tnil) tint cc_default)) ((Etempvar _p_val (talignas 3%N (tptr tvoid))) :: nil)) (Sifthenelse (Etempvar _t'2 tint) (Ssequence (Ssequence (Ssequence (Sset _t'3 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Sset _t'1 (Ecast (Ebinop Osub (Etempvar _t'3 (tptr (talignas 3%N (tptr tvoid)))) (Econst_int (Int.repr 1) tint) (tptr (talignas 3%N (tptr tvoid)))) (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 _t'1 (tptr (talignas 3%N (tptr tvoid)))))) (Sassign (Ederef (Ecast (Etempvar _t'1 (tptr (talignas 3%N (tptr tvoid)))) (tptr (tptr (talignas 3%N (tptr tvoid))))) (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _p_cell (tptr (talignas 3%N (tptr tvoid)))))) Sskip)))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)