Module type Abstract_value.S

module type S = sig .. end

Signature of abstract numerical values.

include Datatype.S

Lattice Structure

val top : t

val is_included : t -> t -> bool

val join : t -> t -> t

val join_and_is_included : t -> t -> t * bool

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

Constructors

val zero : t

val float_zeros : t

val top_int : t

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

val all_values : Cil_types.typ -> t

Creates all abstract values corresponding to the given type.

Forward Operations

val constant : Cil_types.exp -> Cil_types.constant -> t Eval.evaluated

Returns the abstract value of a litteral constants, and potentially some alarms in case of floating point constants overflow.

val forward_unop : context:Eval.unop_context ->
       Cil_types.typ -> Cil_types.unop -> t -> t Eval.evaluated

forward_unop context typ unop v evaluates the value unop v, and the alarms resulting from the operations. See for details on the types. typ is the type of v, and context contains the expressions involved in the operation, needed to create the alarms.

val forward_binop : context:Eval.binop_context ->
       Cil_types.typ -> Cil_types.binop -> t -> t -> t Eval.evaluated

forward_binop context typ binop v1 v2 evaluates the value v1 binop v2, and the alarms resulting from the operations. See for details on the types. typ is the type of v1, and context contains the expressions involved in the operation, needed to create the alarms.

Backward Operations

For an unary forward operation F, the inverse backward opereror 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.

Reinterpret and Cast

val reinterpret : Cil_types.exp -> Cil_types.typ -> t -> t Eval.evaluated

Read the given value with the given type. Also returns an alarm if the type is floating-point type, and the value is not representable as finite float.

val do_promotion : src_typ:Cil_types.typ ->
       dst_typ:Cil_types.typ -> Cil_types.exp -> t -> t Eval.evaluated

val resolve_functions : typ_pointer:Cil_types.typ -> t -> Kernel_function.Hptset.t Eval.or_top * bool

resolve_functions ~typ_pointer v finds within v all the functions with a type compatible with typ_pointer. This function is used to resolve pointers calls. For consistency between analyses, the function Eval_typ.compatible_functions should be used to determine whether the functions v may point to are compatible with typ_pointer.