package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-eva.core/Eva/Builtins/index.html

Module `Eva.Builtins`Source

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 ->
  Frama_c_kernel.Cil_types.typ * Frama_c_kernel.Cil_types.typ list

type cacheable = Eval.cacheable =

| Cacheable
| NoCache
| NoCacheCallers

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:
- the value returned (ie. what is after the 'return' C keyword)
- the memory state after the function has been executed.
*)
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_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 =

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

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:

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?