fact: Definition composites : list composite_definition := (Composite ___sbuf Struct (Member_plain __base (tptr tuchar) :: Member_plain __size tint :: nil) noattr :: Composite ___sFILE 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 __cookie (tptr tvoid) :: Member_plain __close (tptr (Tfunction (Tcons (tptr tvoid) Tnil) tint cc_default)) :: Member_plain __read (tptr (Tfunction (Tcons (tptr tvoid) (Tcons (tptr tschar) (Tcons tint Tnil))) tint cc_default)) :: Member_plain __seek (tptr (Tfunction (Tcons (tptr tvoid) (Tcons tlong (Tcons tint Tnil))) tlong cc_default)) :: Member_plain __write (tptr (Tfunction (Tcons (tptr tvoid) (Tcons (tptr tschar) (Tcons tint Tnil))) tint cc_default)) :: Member_plain __ub (Tstruct ___sbuf noattr) :: Member_plain __extra (tptr (Tstruct ___sFILEX noattr)) :: 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 __offset tlong :: nil) noattr :: Composite _stack_frame Struct (Member_plain _next (tptr (talignas 3%N (tptr tvoid))) :: Member_plain _root (tptr (talignas 3%N (tptr tvoid))) :: Member_plain _prev (tptr (Tstruct _stack_frame noattr)) :: nil) noattr :: Composite _thread_info Struct (Member_plain _alloc (tptr (talignas 3%N (tptr tvoid))) :: Member_plain _limit (tptr (talignas 3%N (tptr tvoid))) :: Member_plain _heap (tptr (Tstruct _heap noattr)) :: Member_plain _args (tarray (talignas 3%N (tptr tvoid)) 1024) :: Member_plain _fp (tptr (Tstruct _stack_frame noattr)) :: Member_plain _nalloc tulong :: Member_plain _odata (tptr tvoid) :: nil) noattr :: Composite _space Struct (Member_plain _start (tptr (talignas 3%N (tptr tvoid))) :: Member_plain _next (tptr (talignas 3%N (tptr tvoid))) :: Member_plain _limit (tptr (talignas 3%N (tptr tvoid))) :: Member_plain _rem_limit (tptr (talignas 3%N (tptr tvoid))) :: nil) noattr :: Composite _heap Struct (Member_plain _spaces (tarray (Tstruct _space noattr) 45) :: nil) noattr :: nil).
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)