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 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 inject_address : Cil_types.varinfo -> t
Abstract address for the given varinfo. (With type "pointer to the type of the variable" if the abstract values are typed.)

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 argres 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. The returned boolean indicates the possibility of an alarm, i.e. that some of the values represented by v do not correspond to functions, or to functions with an incompatible type. It is always safe to return `Top, true.

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.