Module Eva.Builtins

Register OCaml builtins to be used by the cvalue domain instead of analysing the body of some C functions.

exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
type builtin_type = unit -> Eva_ast.typ * Eva_ast.typ list
type cacheable = Eval.cacheable =
  1. | Cacheable
  2. | NoCache
  3. | NoCacheCallers

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

type full_result = {
  1. c_values : (Frama_c_kernel.Cvalue.V.t option * Frama_c_kernel.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.
    *)
  2. c_clobbered : Frama_c_kernel.Base.SetLattice.t;
    (*

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

    *)
  3. c_assigns : (Assigns.t * Frama_c_kernel.Memory_zone.t) option;
    (*

    If not None:

    • the assigns of the function, i.e. the dependencies of the result and of each zone written to.
    • and its sure outputs, i.e. an under-approximation of written zones.
    *)
  4. cacheable : cacheable;
    (*

    Can this result of the function call be cached with memexec?

    *)
}
type call_result =
  1. | 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 these results can be cached and reused for other calls with the same entry state, and if the C function:

    • does not write the address of any local variables;
    • does not read other memory locations than the call arguments;
    • does not write other locations than the result.
    *)
  2. | 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. Can only be used in the same condition than States above.

    *)
  3. | Full of full_result
    (*

    See full_result type.

    *)

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

Type of a cvalue builtin, whose arguments are:

  • the memory state at the beginning of the function call;
  • the list of arguments of the function call.
val register_builtin : string -> ?replace:string -> ?typ:builtin_type -> builtin -> unit

register_builtin name ?replace ?typ 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.

val unregister_builtin : string -> unit

unregister_builtin name unregisters a builtin previously registered with register_builtinname. If there is no builtin with this name, this function has no effect.

val is_builtin : string -> bool

Has a builtin been registered with the given name?