Frama-C:
Plug-ins:
Libraries:

Frama-C API - Val

include Frama_c_kernel.Datatype.S
include Frama_c_kernel.Datatype.S_no_copy
include Frama_c_kernel.Datatype.Ty
type t
val name : string

Unique name of the datatype.

Datatype descriptor.

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.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

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

Pretty print each value in an user-friendly way.

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.

type context = Ctx.t

A numerical value abstraction can optionally require some context from abstract domains. Most transfer functions take the context as argument; it is provided by the abstract state in which operations are performed. See Abstract_context for more details about contexts. For values that don't need context, this type can be defined as unit and the context argument can be safely ignored.

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

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 : context Eva__.Abstract_value.enriched -> Eva.Eva_ast.exp -> Eva.Eva_ast.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 : context Eva__.Abstract_value.enriched -> Frama_c_kernel.Cil_types.typ -> Eva.Eva_ast.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 : context Eva__.Abstract_value.enriched -> Frama_c_kernel.Cil_types.typ -> Eva.Eva_ast.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 : context Eva__.Abstract_value.enriched -> 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 : context Eva__.Abstract_value.enriched -> 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 : context Eva__.Abstract_value.enriched -> input_type:Frama_c_kernel.Cil_types.typ -> resulting_type:Frama_c_kernel.Cil_types.typ -> Eva.Eva_ast.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 : context Eva__.Abstract_value.enriched -> typ_arg:Frama_c_kernel.Cil_types.typ -> Eva.Eva_ast.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 : context Eva__.Abstract_value.enriched -> 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 = {
  1. 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 = {
  1. 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 = {
  1. 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