package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 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.Locations.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.
    *)
}
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 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.

    *)
  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.

    *)
  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 -> 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?

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct