fact: Definition composites : list composite_definition := (Composite __140 Union (Member_plain ___wch tuint :: Member_plain ___wchb (tarray tuchar 4) :: nil) noattr :: Composite __139 Struct (Member_plain ___count tint :: Member_plain ___value (Tunion __140 noattr) :: nil) noattr :: Composite __Bigint Struct (Member_plain __next (tptr (Tstruct __Bigint noattr)) :: Member_plain __k tint :: Member_plain __maxwds tint :: Member_plain __sign tint :: Member_plain __wds tint :: Member_plain __x (tarray tuint 1) :: nil) noattr :: Composite ___tm Struct (Member_plain ___tm_sec tint :: Member_plain ___tm_min tint :: Member_plain ___tm_hour tint :: Member_plain ___tm_mday tint :: Member_plain ___tm_mon tint :: Member_plain ___tm_year tint :: Member_plain ___tm_wday tint :: Member_plain ___tm_yday tint :: Member_plain ___tm_isdst tint :: nil) noattr :: Composite __on_exit_args Struct (Member_plain __fnargs (tarray (tptr tvoid) 32) :: Member_plain __dso_handle (tarray (tptr tvoid) 32) :: Member_plain __fntypes tuint :: Member_plain __is_cxa tuint :: nil) noattr :: Composite __atexit Struct (Member_plain __next (tptr (Tstruct __atexit noattr)) :: Member_plain __ind tint :: Member_plain __fns (tarray (tptr (Tfunction Tnil tvoid cc_default)) 32) :: Member_plain __on_exit_args (Tstruct __on_exit_args noattr) :: nil) noattr :: Composite ___sbuf Struct (Member_plain __base (tptr tuchar) :: Member_plain __size tint :: nil) noattr :: Composite ___sFILE64 Struct (Member_plain __p (tptr tuchar) :: Member_plain __r tint :: Member_plain __w tint :: Member_plain __flags tshort :: Member_plain __file tshort :: Member_plain __bf (Tstruct ___sbuf noattr) :: Member_plain __lbfsize tint :: Member_plain __data (tptr (Tstruct __reent noattr)) :: Member_plain __cookie (tptr tvoid) :: Member_plain __read (tptr (Tfunction (Tcons (tptr (Tstruct __reent noattr)) (Tcons (tptr tvoid) (Tcons (tptr tschar) (Tcons tuint Tnil)))) tint cc_default)) :: Member_plain __write (tptr (Tfunction (Tcons (tptr (Tstruct __reent noattr)) (Tcons (tptr tvoid) (Tcons (tptr tschar) (Tcons tuint Tnil)))) tint cc_default)) :: Member_plain __seek (tptr (Tfunction (Tcons (tptr (Tstruct __reent noattr)) (Tcons (tptr tvoid) (Tcons tint (Tcons tint Tnil)))) tint cc_default)) :: Member_plain __close (tptr (Tfunction (Tcons (tptr (Tstruct __reent noattr)) (Tcons (tptr tvoid) Tnil)) tint cc_default)) :: Member_plain __ub (Tstruct ___sbuf noattr) :: Member_plain __up (tptr tuchar) :: Member_plain __ur tint :: Member_plain __ubuf (tarray tuchar 3) :: Member_plain __nbuf (tarray tuchar 1) :: Member_plain __lb (Tstruct ___sbuf noattr) :: Member_plain __blksize tint :: Member_plain __flags2 tint :: Member_plain __offset tlong :: Member_plain __seek64 (tptr (Tfunction (Tcons (tptr (Tstruct __reent noattr)) (Tcons (tptr tvoid) (Tcons tlong (Tcons tint Tnil)))) tlong cc_default)) :: Member_plain __lock (tptr tvoid) :: Member_plain __mbstate (Tstruct __139 noattr) :: nil) noattr :: Composite __glue Struct (Member_plain __next (tptr (Tstruct __glue noattr)) :: Member_plain __niobs tint :: Member_plain __iobs (tptr (Tstruct ___sFILE64 noattr)) :: nil) noattr :: Composite __rand48 Struct (Member_plain __seed (tarray tushort 3) :: Member_plain __mult (tarray tushort 3) :: Member_plain __add tushort :: nil) noattr :: Composite __214 Struct (Member_plain __unused_rand tuint :: Member_plain __strtok_last (tptr tschar) :: Member_plain __asctime_buf (tarray tschar 26) :: Member_plain __localtime_buf (Tstruct ___tm noattr) :: Member_plain __gamma_signgam tint :: Member_plain __rand_next tulong :: Member_plain __r48 (Tstruct __rand48 noattr) :: Member_plain __mblen_state (Tstruct __139 noattr) :: Member_plain __mbtowc_state (Tstruct __139 noattr) :: Member_plain __wctomb_state (Tstruct __139 noattr) :: Member_plain __l64a_buf (tarray tschar 8) :: Member_plain __signal_buf (tarray tschar 24) :: Member_plain __getdate_err tint :: Member_plain __mbrlen_state (Tstruct __139 noattr) :: Member_plain __mbrtowc_state (Tstruct __139 noattr) :: Member_plain __mbsrtowcs_state (Tstruct __139 noattr) :: Member_plain __wcrtomb_state (Tstruct __139 noattr) :: Member_plain __wcsrtombs_state (Tstruct __139 noattr) :: Member_plain __h_errno tint :: nil) noattr :: Composite __215 Struct (Member_plain __nextf (tarray (tptr tuchar) 30) :: Member_plain __nmalloc (tarray tuint 30) :: nil) noattr :: Composite __213 Union (Member_plain __reent (Tstruct __214 noattr) :: Member_plain __unused (Tstruct __215 noattr) :: nil) noattr :: Composite __reent Struct (Member_plain __errno tint :: Member_plain __stdin (tptr (Tstruct ___sFILE64 noattr)) :: Member_plain __stdout (tptr (Tstruct ___sFILE64 noattr)) :: Member_plain __stderr (tptr (Tstruct ___sFILE64 noattr)) :: Member_plain __inc tint :: Member_plain __emergency (tarray tschar 25) :: Member_plain __unspecified_locale_info tint :: Member_plain __locale (tptr (Tstruct ___locale_t noattr)) :: Member_plain ___sdidinit tint :: Member_plain ___cleanup (tptr (Tfunction (Tcons (tptr (Tstruct __reent noattr)) Tnil) tvoid cc_default)) :: Member_plain __result (tptr (Tstruct __Bigint noattr)) :: Member_plain __result_k tint :: Member_plain __p5s (tptr (Tstruct __Bigint noattr)) :: Member_plain __freelist (tptr (tptr (Tstruct __Bigint noattr))) :: Member_plain __cvtlen tint :: Member_plain __cvtbuf (tptr tschar) :: Member_plain __new (Tunion __213 noattr) :: Member_plain __atexit (tptr (Tstruct __atexit noattr)) :: Member_plain __atexit0 (Tstruct __atexit noattr) :: Member_plain __sig_func (tptr (tptr (Tfunction (Tcons tint Tnil) tvoid cc_default))) :: Member_plain ___sglue (Tstruct __glue noattr) :: Member_plain ___sf (tarray (Tstruct ___sFILE64 noattr) 3) :: nil) noattr :: Composite _thread_info Struct (Member_plain _alloc (tptr (talignas 2%N (tptr tvoid))) :: Member_plain _limit (tptr (talignas 2%N (tptr tvoid))) :: Member_plain _heap (tptr (Tstruct _heap noattr)) :: Member_plain _args (tarray (talignas 2%N (tptr tvoid)) 1024) :: nil) noattr :: Composite _space Struct (Member_plain _start (tptr (talignas 2%N (tptr tvoid))) :: Member_plain _next (tptr (talignas 2%N (tptr tvoid))) :: Member_plain _limit (tptr (talignas 2%N (tptr tvoid))) :: nil) noattr :: Composite _heap Struct (Member_plain _spaces (tarray (Tstruct _space noattr) 12) :: nil) noattr :: nil).
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)