module Builtins: sig
.. end
Value analysis builtin shipped with Frama-C, more efficient than their
equivalent in C
val register_builtin : string -> Db.Value.builtin_sig -> unit
Register the given OCaml function as a builtin, that will be used
instead of the Cil C function of the same name
val find_builtin : string -> Db.Value.builtin_sig
Find a previously registered builtin. Raises Not_found
if no such
builtin exists.
val mem_builtin : string -> bool
Does the builtin table contain an entry for name
?
val overridden_by_builtin : Kernel_function.t -> bool
Should the given function be replaced by a call to a builtin
val type_from_nb_elems : loc:Cil_types.location -> Cil_types.typ -> Integer.t -> Cil_types.typ
Helper function to create the best type for a new base.
Builds an array type with the appropriate number of elements if needed
val dump_state : Db.Value.builtin_sig
Builtins with multiple names; the lookup is done using a distinctive
prefix
val dump_args : string -> Db.Value.builtin_sig
val dump_state_file : string -> Db.Value.builtin_sig