module Cil_builtins:sig
..end
module Frama_c_builtins:State_builder.Hashtbl
with type key = string and type data = varinfo
This module associates the name of a built-in function that might be used during elaboration with the corresponding varinfo.
val is_builtin : Cil_types.varinfo -> bool
val is_unused_builtin : Cil_types.varinfo -> bool
val is_special_builtin : string -> bool
true
if the given name refers to a special built-in function.
A special built-in function can have any number of arguments. It is up to
the plug-ins to know what to do with it.val add_special_builtin : string -> unit
register a new special built-in function
val add_special_builtin_family : (string -> bool) -> unit
register a new family of special built-in functions.
val init_builtins : unit -> unit
initialize the C built-ins. Should be called once per project, after the machine has been set.
module Builtin_functions:State_builder.Hashtbl
with type key = string and type data = typ * typ list * bool
A list of the built-in functions for the current compiler (GCC or
MSVC, depending on !msvcMode
).
val add_custom_builtin : (unit -> string * Cil_types.typ * Cil_types.typ list * bool) -> unit
Register a new builtin. The function will be called after setting
the machdep and initializing machine-dependent builtins. Hence, types
such Cil.uint16_t
might be used if needed.
val builtinLoc : Cil_types.location
This is used as the location of the prototypes of builtin functions.