Eva.Builtins
Eva analysis builtins for the cvalue domain, more efficient than their equivalent in C.
type builtin_type =
unit ->
Frama_c_kernel.Cil_types.typ * Frama_c_kernel.Cil_types.typ list
Can the results of a builtin be cached? See Eval
for more details.
type full_result = {
c_values : (Frama_c_kernel.Cvalue.V.t option * Frama_c_kernel.Cvalue.Model.t)
list; | (* A list of results, consisting of:
|
c_clobbered : Frama_c_kernel.Base.SetLattice.t; | (* An over-approximation of the bases in which addresses of local variables might have been written *) |
c_from : (Frama_c_kernel.Function_Froms.froms * Frama_c_kernel.Locations.Zone.t)
option; | (* 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 Frama_c_kernel.Cvalue.Model.t list | (* 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 Frama_c_kernel.Cvalue.V.t list | (* 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 full_result | (* See |
The result of a builtin can be given in different forms.
type builtin =
Frama_c_kernel.Cvalue.Model.t ->
(Frama_c_kernel.Cil_types.exp * Frama_c_kernel.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
.