module type S =sig
..end
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 float_zeros : t
val top_int : t
val inject_int : Cil_types.typ -> Integer.t -> t
val inject_address : Cil_types.varinfo -> t
val constant : Cil_types.exp -> Cil_types.constant -> t Eval.evaluated
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.
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 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
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
.