module Builtins:sig
..end
Set of functions overridden by a builtin.
exception Invalid_nb_of_args of int
val register_builtin : string ->
?replace:string -> ?typ:Db.Value.builtin_type -> Db.Value.builtin -> unit
register_builtin name ?replace ?typ f
registers the ocaml function f
as a builtin to be used instead of the C function of name name
.
If replace
is provided, the builtin is also used instead of the C function
of name replace
, unless option -eva-builtin-auto is disabled.
If typ
is provided, consistency between the expected typ
and the type of
the C function is checked before using the builtin.val prepare_builtins : unit -> unit
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.type
builtin
typecall =
(Precise_locs.precise_location, Cvalue.V.t) Eval.call
typeresult =
Cvalue.Model.t * Locals_scoping.clobbered_set
val is_builtin_overridden : Cil_types.kernel_function -> bool
val find_builtin_override : Cil_types.kernel_function ->
(string * builtin * Cil_types.funspec) option
prepare_builtins
should have been called before using this function.val apply_builtin : builtin ->
call ->
Cvalue.Model.t -> result list * Value_types.cacheable