Module Builtins

module Builtins: sig .. end
Value analysis builtin shipped with Frama-C, more efficient than their equivalent in C

exception Invalid_nb_of_args of int
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 registered_builtins : unit -> (string * Db.Value.builtin_sig) list
Returns a list of the pairs (name, builtin_sig) registered via register_builtin.
Since Aluminium-20160501
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 clobbered_set_from_ret : Cvalue.Model.t -> Cvalue.V.t -> Base.SetLattice.t
clobbered_set_from_ret state ret can be used for functions that return a pointer to where they have written some data. It returns all the bases of ret whose contents may contain local variables.
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
val emit_alarm : kind:string -> text:string -> unit
Emit an ACSL assert (using \warning predicate) to signal that the builtin encountered an alarm described by the string. kind is used to describe the alarm, similarly to Alarms.get_name.