module Builtins:sig
..end
Eva analysis builtins for the cvalue domain, more efficient than their equivalent in C.
exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
typebuiltin_type =
unit -> Cil_types.typ * Cil_types.typ list
typecacheable =
Eval.cacheable
=
| |
Cacheable |
| |
NoCache |
| |
NoCacheCallers |
Can the results of a builtin be cached? See for more details.
type
full_result = {
|
c_values : |
(* | A list of results, consisting of:
| *) |
|
c_clobbered : |
(* | An over-approximation of the bases in which addresses of local variables might have been written | *) |
|
c_from : |
(* | If not None, the froms of the function, and its sure outputs; i.e. the dependencies of the result and of each zone written to. | *) |
}
type
call_result =
| |
States of |
(* | A disjunctive list of post-states at the end of the C function. Can only be used if the C function does not write the address of local variables, does not read other locations than the call arguments, and does not write other locations than the result. | *) |
| |
Result of |
(* | A disjunctive list of resulting values. The specification is used to compute the post-state, in which the result is replaced by the values computed by the builtin. | *) |
| |
Full of |
(* | See | *) |
The result of a builtin can be given in different forms.
typebuiltin =
Cvalue.Model.t -> (Cil_types.exp * Cvalue.V.t) list -> call_result
Type of a cvalue builtin, whose arguments are:
val register_builtin : string ->
?replace:string ->
?typ:builtin_type -> cacheable -> builtin -> unit
register_builtin name ?replace ?typ cacheable f
registers the 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.
The results of the builtin are cached according to cacheable
.
val is_builtin : string -> bool
Has a builtin been registered with the given name?
val prepare_builtins : unit -> unit
Prepares the builtins to be used for an analysis. Must be called at the beginning of each Eva analysis. Warns about builtins of incompatible types, builtins without an available specification and builtins overriding function definitions.
val is_builtin_overridden : Cil_types.kernel_function -> bool
Is a given function replaced by 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.
typecall =
(Precise_locs.precise_location, Cvalue.V.t) Eval.call
typeresult =
Cvalue_domain.State.t
val find_builtin_override : Cil_types.kernel_function ->
(string * builtin * cacheable * 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.
prepare_builtins
should have been called before using this function.
val apply_builtin : builtin ->
call ->
pre:Cvalue.Model.t -> post:Cvalue.Model.t -> result list