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 one : t
val top_int : t
val inject_int : Cil_types.typ -> Integer.t -> t
Abstract address for the given varinfo. (With type "pointer to the type of the variable" if the abstract values are typed.)
These functions are used to create the alarms that report undesirable
behaviors, when a value abstraction does not meet the prerequisites of an
operation. Thereafter, the value is assumed to meet them to continue the
analysis.
See the documentation of the truth
type for more details.
val assume_non_zero : t -> t Abstract_value.truth
val assume_bounded : Abstract_value.bound_kind ->
Abstract_value.bound -> t -> t Abstract_value.truth
val assume_not_nan : assume_finite:bool -> Cil_types.fkind -> t -> t Abstract_value.truth
val assume_pointer : t -> t Abstract_value.truth
Assumes that the abstract value only represents well-formed pointer values: pointers either to an element of an array object or one past the last element of an array object. (A pointer to an object that is not an element of an array is viewed as a pointer to the first element of an array of length one with the type of the object as its element type.) The NULL pointer is always a valid pointer value. Function pointers are also considered as valid pointer values for now.
val assume_comparable : Abstract_value.pointer_comparison -> t -> t -> (t * t) Abstract_value.truth
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 : Cil_types.typ -> Cil_types.unop -> t -> t Eval.or_bottom
forward_unop typ unop v
evaluates the value unop v
, resulting from the
application of the unary operator unop
to the value v
. typ
is the
type of v
.
val forward_binop : Cil_types.typ -> Cil_types.binop -> t -> t -> t Eval.or_bottom
forward_binop typ binop v1 v2
evaluates the value v1 binop v2
,
resulting from the application of the binary operator binop
to the
values v1
and v2
. typ
is the type of v1
.
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
, assuming 2's complement.
val forward_cast : src_type:Eval_typ.scalar_typ ->
dst_type:Eval_typ.scalar_typ -> t -> t Eval.or_bottom
Abstract evaluation of casts operators from src_type
to dst_type
.
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 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
.