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 =
Eva.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?