module Make:
Parameters: |
|
include Datatype.S
val pretty_typ : Cil_types.typ option -> t Pretty_utils.formatter
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
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_comparable : Abstract_value.pointer_comparison -> t -> t -> (t * t) Abstract_value.truth
val constant : Cil_types.exp -> Cil_types.constant -> t
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
src_type
to dst_type
.
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
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
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
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
.