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.gui/Eva_gui/Gui_eval/Make/argument-1-X/Val/index.html

Module `X.Val`

include Frama_c_kernel.Datatype.S

include Frama_c_kernel.Datatype.S_no_copy

include Frama_c_kernel.Datatype.Ty

type t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val ty : t Frama_c_kernel.Type.t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val name : string

Unique name of the datatype.

val descr : t Frama_c_kernel.Descr.t

Datatype descriptor.

val packed_descr : Frama_c_kernel.Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val mem_project : (Frama_c_kernel.Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

val pretty_typ : 
  Frama_c_kernel.Cil_types.typ option ->
  t Frama_c_kernel.Pretty_utils.formatter

Pretty the abstract value assuming it has the type given as argument.

Lattice Structure

val top : t

val is_included : t -> t -> bool

val join : t -> t -> t

val narrow : t -> t -> t Eva.Eval.or_bottom

Constructors

val zero : t

val one : t

val top_int : t

val inject_int : Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Integer.t -> t

Abstract address for the given varinfo. (With type "pointer to the type of the variable" if the abstract values are typed.)

Alarms

These functions are used to create the alarms that report undesirable behaviors, when a value abstraction does not meet the prerequisites of an operation. Thereafter, the value is assumed to meet them to continue the analysis. See the documentation of the truth type for more details.

val assume_non_zero : 
  t ->
  [ `False | `Unknown of t | `True | `TrueReduced of t | `Unreachable ]

val assume_bounded : 
  Frama_c_kernel.Alarms.bound_kind ->
  Eva__.Abstract_value.bound ->
  t ->
  [ `False | `Unknown of t | `True | `TrueReduced of t | `Unreachable ]

val assume_not_nan : 
  assume_finite:bool ->
  Frama_c_kernel.Cil_types.fkind ->
  t ->
  [ `False | `Unknown of t | `True | `TrueReduced of t | `Unreachable ]

val assume_pointer : 
  t ->
  [ `False | `Unknown of t | `True | `TrueReduced of t | `Unreachable ]

Assumes that the abstract value only represents well-formed pointer values: pointers either to an element of an array object or one past the last element of an array object. (A pointer to an object that is not an element of an array is viewed as a pointer to the first element of an array of length one with the type of the object as its element type.) The NULL pointer is always a valid pointer value. Function pointers are also considered as valid pointer values for now.

val assume_comparable : 
  Eva__.Abstract_value.pointer_comparison ->
  t ->
  t ->
  [ `False | `Unknown of t * t | `True | `TrueReduced of t * t | `Unreachable ]

Forward Operations

val constant : 
  Frama_c_kernel.Cil_types.exp ->
  Frama_c_kernel.Cil_types.constant ->
  t

Embeds C constants into value abstractions: returns an abstract value for the given constant. The constant cannot be an enumeration constant.

val forward_unop : 
  Frama_c_kernel.Cil_types.typ ->
  Frama_c_kernel.Cil_types.unop ->
  t ->
  t Eva.Eval.or_bottom

forward_unop typ unop v evaluates the value unop v, resulting from the application of the unary operator unop to the value v. typ is the type of v.

val forward_binop : 
  Frama_c_kernel.Cil_types.typ ->
  Frama_c_kernel.Cil_types.binop ->
  t ->
  t ->
  t Eva.Eval.or_bottom

forward_binop typ binop v1 v2 evaluates the value v1 binop v2, resulting from the application of the binary operator binop to the values v1 and v2. typ is the type of v1.

val rewrap_integer : Eva__.Eval_typ.integer_range -> t -> t

rewrap_integer irange t wraps around the abstract value t to fit the integer range irange, assuming 2's complement. Also used on absolute addresses for pointer values, seen as unsigned integers.

val forward_cast : 
  src_type:Eva__.Eval_typ.scalar_typ ->
  dst_type:Eva__.Eval_typ.scalar_typ ->
  t ->
  t Eva.Eval.or_bottom

Abstract evaluation of casts operators from src_type to dst_type.

Backward Operations

For an unary forward operation F, the inverse backward operator B tries to reduce the argument values of the operation, given its result.

It must satisfy: if B arg res = v then ∀ a ⊆ arg such that F a ⊆ res, a ⊆ v

i.e. B arg res returns a value v larger than all subvalues of arg whose result through F is included in res.

If F arg ∈ res is impossible, then v should be bottom. If the value arg cannot be reduced, then v should be None.

Any n-ary operator may be considered as a unary operator on a vector of values, the inclusion being lifted pointwise.

val backward_binop : 
  input_type:Frama_c_kernel.Cil_types.typ ->
  resulting_type:Frama_c_kernel.Cil_types.typ ->
  Frama_c_kernel.Cil_types.binop ->
  left:t ->
  right:t ->
  result:t ->
  (t option * t option) Eva.Eval.or_bottom

Backward evaluation of the binary operation left binop right = result; tries to reduce the argument left and right according to result. input_type is the type of left, resulting_type the type of result.

val backward_unop : 
  typ_arg:Frama_c_kernel.Cil_types.typ ->
  Frama_c_kernel.Cil_types.unop ->
  arg:t ->
  res:t ->
  t option Eva.Eval.or_bottom

Backward evaluation of the unary operation unop arg = res; tries to reduce the argument arg according to res. typ_arg is the type of arg.

val backward_cast : 
  src_typ:Frama_c_kernel.Cil_types.typ ->
  dst_typ:Frama_c_kernel.Cil_types.typ ->
  src_val:t ->
  dst_val:t ->
  t option Eva.Eval.or_bottom

Backward evaluation of the cast of the value src_val of type src_typ into the value dst_val of type dst_typ. Tries to reduce scr_val according to dst_val.

Misc

val resolve_functions : 
  t ->
  Frama_c_kernel.Kernel_function.t list Eva.Eval.or_top * bool

resolve_functions v returns the list of functions that may be pointed to by the abstract value v (representing a function pointer). The returned boolean must be true if some of the values represented by v do not correspond to functions. It is always safe to return `Top, true.

val replace_base : Frama_c_kernel.Base.substitution -> t -> t

For pointer values, replace_base substitution value replaces the bases pointed to by value according to substitution. For arithmetic values, this function returns the value unchanged.

val structure : t Eva__.Abstract.Value.structure

val mem : 'a Eva__.Structure.Key_Value.key -> bool

Tests whether a key belongs to the module.

val get : 'a Eva__.Structure.Key_Value.key -> (t -> 'a) option

For a key of type k key:

if the values of type t contain a subpart of type k from a module identified by the key, then get key returns an accessor for it.
otherwise, get key returns None.

val set : 'a Eva__.Structure.Key_Value.key -> 'a -> t -> t

For a key of type k key:

if the values of type t contain a subpart of type k from a module identified by the key, then set key v t returns the value t in which this subpart has been replaced by v.
otherwise, set key _ is the identity function.

Iterators on the components of a structure.

type polymorphic_iter_fun = {

iter : 'a. 'a Eva__.Structure.Key_Value.key -> (module Eva__.Abstract_value.S with type t = 'a) -> 'a -> unit;

}

val iter : polymorphic_iter_fun -> t -> unit

type 'b polymorphic_fold_fun = {

fold : 'a. 'a Eva__.Structure.Key_Value.key -> (module Eva__.Abstract_value.S with type t = 'a) -> 'a -> 'b -> 'b;

}

val fold : 'b polymorphic_fold_fun -> t -> 'b -> 'b

type polymorphic_map_fun = {

map : 'a. 'a Eva__.Structure.Key_Value.key -> (module Eva__.Abstract_value.S with type t = 'a) -> 'a -> 'a;

}

val map : polymorphic_map_fun -> t -> t

val reduce : t -> t

On This Page

Lattice Structure
Constructors
Alarms
Forward Operations
Backward Operations
Misc