Module Eva.Builtins

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
type builtin_type = unit -> Cil_types.typ * Cil_types.typ list 
type cacheable = Eva.Eval.cacheable = 
| Cacheable
| NoCache
| NoCacheCallers

Can the results of a builtin be cached? See for more details.

type full_result = {
   c_values : (Cvalue.V.t option * Cvalue.Model.t) list; (*

A list of results, consisting of:

  • the value returned (ie. what is after the 'return' C keyword)
  • the memory state after the function has been executed.
*)
   c_clobbered : Base.SetLattice.t; (*

An over-approximation of the bases in which addresses of local variables might have been written

*)
   c_from : (Function_Froms.froms * 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 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 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 full_result type.

*)

The result of a builtin can be given in different forms.

type builtin = 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?