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

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: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 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 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 restrict_float : remove_infinite:bool ->
Cil_types.exp -> Cil_types.fkind -> t -> t Eval.evaluated

restrict_float expr fkind t removes NaN from the abstract value t. It also removes infinities if remove_infinite is set to true. Produces is_nan_or_infinite alarms if necessary.

val cast : 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 : 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 `Toptrue.