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.
val top : t
val is_included : t -> t -> bool
val join : t -> t -> t
val narrow : t -> t -> t Eval.or_bottom
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.)
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.
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
.
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 `Top, true
.