Module Cil_builtins

module Cil_builtins: sig .. end

Builtins management

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

Since Fluorine-20130401
Returns true if the given variable refers to a Frama-C builtin.

val is_unused_builtin : Cil_types.varinfo -> bool

Returns true if the given variable refers to a Frama-C builtin that is not used in the current program. Plugins may (and in fact should) hide this builtin from their outputs

val is_special_builtin : string -> bool

Since Carbon-20101201
Returns 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

val add_special_builtin_family : (string -> bool) -> unit

Since Carbon-20101201

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.

Since 23.0-Vanadium

val builtinLoc : Cil_types.location

This is used as the location of the prototypes of builtin functions.