Module type Abstract_value.S

module type S = sig .. end

Signature of abstract numerical values.

include Datatype.S

val pretty_typ : Cil_types.typ option -> t 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 Eval.or_bottom

Constructors

val zero : t

val one : t

val top_int : t

val inject_int : Cil_types.typ -> 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 -> t Abstract_value.truth

val assume_bounded : Abstract_value.bound_kind ->
       Abstract_value.bound -> t -> t Abstract_value.truth

val assume_not_nan : assume_finite:bool -> Cil_types.fkind -> t -> t Abstract_value.truth

val assume_pointer : t -> t Abstract_value.truth

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 : Abstract_value.pointer_comparison -> t -> t -> (t * t) Abstract_value.truth

Forward Operations

val constant : Cil_types.exp -> 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 : Cil_types.typ -> Cil_types.unop -> t -> t 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 : Cil_types.typ -> Cil_types.binop -> t -> t -> t 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 : 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.

val forward_cast : src_type:Eval_typ.scalar_typ ->
       dst_type:Eval_typ.scalar_typ -> t -> t 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:Cil_types.typ ->
       resulting_type:Cil_types.typ ->
       Cil_types.binop ->
       left:t -> right:t -> result:t -> (t option * t option) 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:Cil_types.typ ->
       Cil_types.unop -> arg:t -> res:t -> t option 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:Cil_types.typ ->
       dst_typ:Cil_types.typ -> src_val:t -> dst_val:t -> t option 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 -> Kernel_function.t list 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 : 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.