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 -> ?replace: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 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 warn_definitions_overridden_by_builtins : unit -> unit
Emits warnings for each function definition that will be overridden by an
Eva built-in.
Does not include definitions in the Frama-C stdlib.
Since Phosphorus-20170501-beta1
type
builtin
type
call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
type
result = Cvalue.Model.t * Locals_scoping.clobbered_set
val find_builtin_override : Cil_types.kernel_function ->
(string * builtin * Cil_types.funspec) option
Returns the cvalue builtin for a function, if any. Also returns the name of
the builtin and the specification of the function; the preconditions must be
evaluated along with the builtin.
val apply_builtin : builtin ->
call ->
Cvalue.Model.t -> result list * Value_types.cacheable