module type S =sig
..end
include Datatype.S
val top : t
val is_included : t -> t -> bool
val join : t -> t -> t
val join_and_is_included : t -> t -> t * bool
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 all_values : Cil_types.typ -> 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 reinterpret : Cil_types.exp -> Cil_types.typ -> t -> t Eval.evaluated
val do_promotion : src_typ:Cil_types.typ ->
dst_typ:Cil_types.typ -> Cil_types.exp -> t -> t Eval.evaluated
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
. 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
.