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 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 literal constant, 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 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.

Reinterpret and Cast

val truncate_integer : Cil_types.exp -> Eval_typ.integer_range -> t -> t Eval.evaluated

truncate_integer expr irange t truncates the abstract value t to the integer range irange. Produces overflow alarms if t does not already fit into irange, attached to the expression expr.

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. Does not produce any alarms.

val cast_float : Cil_types.exp -> Cil_types.fkind -> t -> t Eval.evaluated

cast_float expr fkind t recasts the abstract value t resulting from a floating-point operation to the precision type fkind. Produces is_nan_or_infinite alarms (attached to the expression expr) if necessary.

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

Abstract evaluation of casts operators from scr_typ to dst_typ.

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.