fact: Definition public_idents : list ident := (_main :: _n :: _copy :: _mallocN :: ___builtin_debug :: ___builtin_fmin :: ___builtin_fmax :: ___builtin_fnmsub :: ___builtin_fnmadd :: ___builtin_fmsub :: ___builtin_fmadd :: ___builtin_clsll :: ___builtin_clsl :: ___builtin_cls :: ___builtin_fence :: ___builtin_expect :: ___builtin_unreachable :: ___builtin_va_end :: ___builtin_va_copy :: ___builtin_va_arg :: ___builtin_va_start :: ___builtin_membar :: ___builtin_annot_intval :: ___builtin_annot :: ___builtin_sel :: ___builtin_memcpy_aligned :: ___builtin_sqrt :: ___builtin_fsqrt :: ___builtin_fabsf :: ___builtin_fabs :: ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz :: ___builtin_clzll :: ___builtin_clzl :: ___builtin_clz :: ___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap :: ___builtin_bswap64 :: ___compcert_i64_umulh :: ___compcert_i64_smulh :: ___compcert_i64_sar :: ___compcert_i64_shr :: ___compcert_i64_shl :: ___compcert_i64_umod :: ___compcert_i64_smod :: ___compcert_i64_udiv :: ___compcert_i64_sdiv :: ___compcert_i64_utof :: ___compcert_i64_stof :: ___compcert_i64_utod :: ___compcert_i64_stod :: ___compcert_i64_dtou :: ___compcert_i64_dtos :: ___compcert_va_composite :: ___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 :: nil).
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)