fact: Definition global_definitions : list (ident * globdef fundef type) := ((___compcert_va_int32, Gfun(External (EF_runtime "__compcert_va_int32" (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) (Tcons (tptr tvoid) Tnil) tuint cc_default)) :: (___compcert_va_int64, Gfun(External (EF_runtime "__compcert_va_int64" (mksignature (AST.Tlong :: nil) AST.Tlong cc_default)) (Tcons (tptr tvoid) Tnil) tulong cc_default)) :: (___compcert_va_float64, Gfun(External (EF_runtime "__compcert_va_float64" (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) (Tcons (tptr tvoid) Tnil) tdouble cc_default)) :: (___compcert_va_composite, Gfun(External (EF_runtime "__compcert_va_composite" (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong cc_default)) (Tcons (tptr tvoid) (Tcons tulong Tnil)) (tptr tvoid) cc_default)) :: (___compcert_i64_dtos, Gfun(External (EF_runtime "__compcert_i64_dtos" (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default)) (Tcons tdouble Tnil) tlong cc_default)) :: (___compcert_i64_dtou, Gfun(External (EF_runtime "__compcert_i64_dtou" (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default)) (Tcons tdouble Tnil) tulong cc_default)) :: (___compcert_i64_stod, Gfun(External (EF_runtime "__compcert_i64_stod" (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) (Tcons tlong Tnil) tdouble cc_default)) :: (___compcert_i64_utod, Gfun(External (EF_runtime "__compcert_i64_utod" (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) (Tcons tulong Tnil) tdouble cc_default)) :: (___compcert_i64_stof, Gfun(External (EF_runtime "__compcert_i64_stof" (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default)) (Tcons tlong Tnil) tfloat cc_default)) :: (___compcert_i64_utof, Gfun(External (EF_runtime "__compcert_i64_utof" (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default)) (Tcons tulong Tnil) tfloat cc_default)) :: (___compcert_i64_sdiv, Gfun(External (EF_runtime "__compcert_i64_sdiv" (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) :: (___compcert_i64_udiv, Gfun(External (EF_runtime "__compcert_i64_udiv" (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) :: (___compcert_i64_smod, Gfun(External (EF_runtime "__compcert_i64_smod" (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) :: (___compcert_i64_umod, Gfun(External (EF_runtime "__compcert_i64_umod" (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) :: (___compcert_i64_shl, Gfun(External (EF_runtime "__compcert_i64_shl" (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong cc_default)) :: (___compcert_i64_shr, Gfun(External (EF_runtime "__compcert_i64_shr" (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong cc_default)) (Tcons tulong (Tcons tint Tnil)) tulong cc_default)) :: (___compcert_i64_sar, Gfun(External (EF_runtime "__compcert_i64_sar" (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong cc_default)) :: (___compcert_i64_smulh, Gfun(External (EF_runtime "__compcert_i64_smulh" (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) :: (___compcert_i64_umulh, Gfun(External (EF_runtime "__compcert_i64_umulh" (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) :: (___builtin_bswap64, Gfun(External (EF_builtin "__builtin_bswap64" (mksignature (AST.Tlong :: nil) AST.Tlong cc_default)) (Tcons tulong Tnil) tulong cc_default)) :: (___builtin_bswap, Gfun(External (EF_builtin "__builtin_bswap" (mksignature (AST.Tint :: nil) AST.Tint cc_default)) (Tcons tuint Tnil) tuint cc_default)) :: (___builtin_bswap32, Gfun(External (EF_builtin "__builtin_bswap32" (mksignature (AST.Tint :: nil) AST.Tint cc_default)) (Tcons tuint Tnil) tuint cc_default)) :: (___builtin_bswap16, Gfun(External (EF_builtin "__builtin_bswap16" (mksignature (AST.Tint :: nil) AST.Tint16unsigned cc_default)) (Tcons tushort Tnil) tushort cc_default)) :: (___builtin_clz, Gfun(External (EF_builtin "__builtin_clz" (mksignature (AST.Tint :: nil) AST.Tint cc_default)) (Tcons tuint Tnil) tint cc_default)) :: (___builtin_clzl, Gfun(External (EF_builtin "__builtin_clzl" (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) (Tcons tulong Tnil) tint cc_default)) :: (___builtin_clzll, Gfun(External (EF_builtin "__builtin_clzll" (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) (Tcons tulong Tnil) tint cc_default)) :: (___builtin_ctz, Gfun(External (EF_builtin "__builtin_ctz" (mksignature (AST.Tint :: nil) AST.Tint cc_default)) (Tcons tuint Tnil) tint cc_default)) :: (___builtin_ctzl, Gfun(External (EF_builtin "__builtin_ctzl" (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) (Tcons tulong Tnil) tint cc_default)) :: (___builtin_ctzll, Gfun(External (EF_builtin "__builtin_ctzll" (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) (Tcons tulong Tnil) tint cc_default)) :: (___builtin_fabs, Gfun(External (EF_builtin "__builtin_fabs" (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) (Tcons tdouble Tnil) tdouble cc_default)) :: (___builtin_fabsf, Gfun(External (EF_builtin "__builtin_fabsf" (mksignature (AST.Tsingle :: nil) AST.Tsingle cc_default)) (Tcons tfloat Tnil) tfloat cc_default)) :: (___builtin_fsqrt, Gfun(External (EF_builtin "__builtin_fsqrt" (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) (Tcons tdouble Tnil) tdouble cc_default)) :: (___builtin_sqrt, Gfun(External (EF_builtin "__builtin_sqrt" (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) (Tcons tdouble Tnil) tdouble cc_default)) :: (___builtin_memcpy_aligned, Gfun(External (EF_builtin "__builtin_memcpy_aligned" (mksignature (AST.Tlong :: AST.Tlong :: AST.Tlong :: AST.Tlong :: nil) AST.Tvoid cc_default)) (Tcons (tptr tvoid) (Tcons (tptr tvoid) (Tcons tulong (Tcons tulong Tnil)))) tvoid cc_default)) :: (___builtin_sel, Gfun(External (EF_builtin "__builtin_sel" (mksignature (AST.Tint :: nil) AST.Tvoid {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) (Tcons tbool Tnil) tvoid {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: (___builtin_annot, Gfun(External (EF_builtin "__builtin_annot" (mksignature (AST.Tlong :: nil) AST.Tvoid {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) (Tcons (tptr tschar) Tnil) tvoid {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: (___builtin_annot_intval, Gfun(External (EF_builtin "__builtin_annot_intval" (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tint cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil)) tint cc_default)) :: (___builtin_membar, Gfun(External (EF_builtin "__builtin_membar" (mksignature nil AST.Tvoid cc_default)) Tnil tvoid cc_default)) :: (___builtin_va_start, Gfun(External (EF_builtin "__builtin_va_start" (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default)) (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: (___builtin_va_arg, Gfun(External (EF_builtin "__builtin_va_arg" (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil)) tvoid cc_default)) :: (___builtin_va_copy, Gfun(External (EF_builtin "__builtin_va_copy" (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tvoid cc_default)) (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) :: (___builtin_va_end, Gfun(External (EF_builtin "__builtin_va_end" (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default)) (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: (___builtin_unreachable, Gfun(External (EF_builtin "__builtin_unreachable" (mksignature nil AST.Tvoid cc_default)) Tnil tvoid cc_default)) :: (___builtin_expect, Gfun(External (EF_builtin "__builtin_expect" (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) :: (___builtin_fence, Gfun(External (EF_builtin "__builtin_fence" (mksignature nil AST.Tvoid cc_default)) Tnil tvoid cc_default)) :: (___builtin_cls, Gfun(External (EF_builtin "__builtin_cls" (mksignature (AST.Tint :: nil) AST.Tint cc_default)) (Tcons tint Tnil) tint cc_default)) :: (___builtin_clsl, Gfun(External (EF_builtin "__builtin_clsl" (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) (Tcons tlong Tnil) tint cc_default)) :: (___builtin_clsll, Gfun(External (EF_builtin "__builtin_clsll" (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) (Tcons tlong Tnil) tint cc_default)) :: (___builtin_fmadd, Gfun(External (EF_builtin "__builtin_fmadd" (mksignature (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat cc_default)) (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble cc_default)) :: (___builtin_fmsub, Gfun(External (EF_builtin "__builtin_fmsub" (mksignature (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat cc_default)) (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble cc_default)) :: (___builtin_fnmadd, Gfun(External (EF_builtin "__builtin_fnmadd" (mksignature (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat cc_default)) (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble cc_default)) :: (___builtin_fnmsub, Gfun(External (EF_builtin "__builtin_fnmsub" (mksignature (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat cc_default)) (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble cc_default)) :: (___builtin_fmax, Gfun(External (EF_builtin "__builtin_fmax" (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat cc_default)) (Tcons tdouble (Tcons tdouble Tnil)) tdouble cc_default)) :: (___builtin_fmin, Gfun(External (EF_builtin "__builtin_fmin" (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat cc_default)) (Tcons tdouble (Tcons tdouble Tnil)) tdouble cc_default)) :: (___builtin_debug, Gfun(External (EF_external "__builtin_debug" (mksignature (AST.Tint :: nil) AST.Tvoid {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) (Tcons tint Tnil) tvoid {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: (_find, Gfun(Internal f_find)) :: nil).
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)