module Eval_op: sig
.. end
Numeric evaluation. Factored with evaluation in the logic.
val pp_v : Cvalue.V.t -> Format.formatter -> unit
val offsetmap_of_v : typ:Cil_types.typ -> Cvalue.V.t -> Cvalue.V_Offsetmap.t
Transformation a value into an offsetmap of size sizeof(typ)
bytes.
val wrap_int : Cvalue.V.t -> Cvalue.V_Offsetmap.t option
val wrap_ptr : Cvalue.V.t -> Cvalue.V_Offsetmap.t option
val wrap_double : Cvalue.V.t -> Cvalue.V_Offsetmap.t option
val wrap_float : Cvalue.V.t -> Cvalue.V_Offsetmap.t option
val wrap_size_t : Cvalue.V.t -> Cvalue.V_Offsetmap.t option
Specialization of the function above for standard types
val is_bitfield : Cil_types.typ -> bool
Bitfields
val sizeof_lval_typ : Cil_types.typ -> Int_Base.t
Size of the type of a lval, taking into account that the lval might have
been a bitfield.
val cast_lval_if_bitfield : Cil_types.typ -> Int_Base.i -> Cvalue.V.t -> Cvalue.V.t
if needed, cast the given abstract value to the given size. Useful
to handle bitfield. The type given as argument must be the type of
the l-value the abstract value is written into, which is of size size
.
val reinterpret_int : with_alarms:CilE.warn_mode -> Cil_types.ikind -> Cvalue.V.t -> Cvalue.V.t
Read the given value value as an int of the given ikind
. Warn if the
value contains an address.
val reinterpret_float : with_alarms:CilE.warn_mode -> Cil_types.fkind -> Cvalue.V.t -> Cvalue.V.t
Read the given value value as a float int of the given fkind
. Warn if the
value contains an address, or is not representable as a finite float.
val reinterpret : with_alarms:CilE.warn_mode -> Cil_types.typ -> Cvalue.V.t -> Cvalue.V.t
val v_uninit_of_offsetmap : with_alarms:CilE.warn_mode ->
typ:Cil_types.typ -> Cvalue.V_Offsetmap.t -> Cvalue.V_Offsetmap.v
Reads the contents of the offsetmap (assuming it contains sizeof(typ)
bytes), and return them as an uninterpreted value.
val v_of_offsetmap : with_alarms:CilE.warn_mode ->
typ:Cil_types.typ -> Cvalue.V_Offsetmap.t -> Cvalue.V.t
Reads the contents of the offsetmap (assuming it contains sizeof(typ)
bytes) as a value of type V.t, then convert the result to type typ
val do_promotion : with_alarms:CilE.warn_mode ->
Ival.Float_abstract.rounding_mode ->
src_typ:Cil_types.typ ->
dst_typ:Cil_types.typ ->
Cvalue.V.t -> (Format.formatter -> unit) -> Cvalue.V.t
val handle_overflow : with_alarms:CilE.warn_mode ->
warn_unsigned:bool -> Cil_types.typ -> Cvalue.V.t -> Cvalue.V.t
val eval_binop_float : with_alarms:CilE.warn_mode ->
Ival.Float_abstract.rounding_mode ->
Cil_types.fkind option ->
Cvalue.V.t -> Cil_types.binop -> Cvalue.V.t -> Cvalue.V.t
val eval_minus_pp : with_alarms:CilE.warn_mode ->
te1:Cil_types.typ -> Cvalue.V.t -> Cvalue.V.t -> Cvalue.V.t
val eval_binop_int : with_alarms:CilE.warn_mode ->
te1:Cil_types.typ ->
Cvalue.V.t -> Cil_types.binop -> Cvalue.V.t -> Cvalue.V.t
val eval_uneg : with_alarms:CilE.warn_mode -> Cvalue.V.t -> Cil_types.typ -> Cvalue.V.t
val eval_unop : check_overflow:bool ->
with_alarms:CilE.warn_mode ->
Cvalue.V.t -> Cil_types.typ -> Cil_types.unop -> Cvalue.V.t
val inv_binop_rel : Cil_types.binop -> Cil_types.binop
val reduce_rel_int : bool ->
Cil_types.binop ->
Locations.Location_Bytes.t ->
Locations.Location_Bytes.t -> Locations.Location_Bytes.t
val reduce_rel_float_double : bool ->
Ival.Float_abstract.float_kind ->
bool -> Cil_types.binop -> Cvalue.V.t -> Cvalue.V.t -> Cvalue.V.t
val reduce_rel_from_type : Cil_types.typ ->
bool ->
Cil_types.binop ->
Locations.Location_Bytes.t ->
Locations.Location_Bytes.t -> Locations.Location_Bytes.t
Reduction of a Cvalue.V.t
by ==
, !=
, >=
, >
, <=
and <
.
reduce_rel_from_type typ positive op vexpr v
reduces v
so that the relation v op vexpr
holds. typ
is the type of the
expression being reduced.
val eval_float_constant : with_alarms:CilE.warn_mode ->
float -> Cil_types.fkind -> string option -> Cvalue.V.t
The arguments are the approximate float value computed during parsing, the
size of the floating-point type, and the string representing the initial
constant if available. Return an abstract value that may be bottom if the
constant is outside of the representable range, or that may be imprecise
if it is not exactly representable.
val make_volatile : ?typ:Cil_types.typ -> Cvalue.V.t -> Cvalue.V.t
make_volatile ?typ v
makes the value v
more general (to account for
external modifications), whenever typ
is None
or when it has type
qualifier volatile
val add_binding_unspecified : with_alarms:CilE.warn_mode ->
?remove_invalid:bool ->
exact:bool ->
Cvalue.Model.t ->
Locations.Location.t -> Cvalue.V_Or_Uninitialized.t -> Cvalue.Model.t
Temporary. Re-export of Cvalue.Model.add_binding_unspecifed
with a
with_alarms
argument
val add_binding : with_alarms:CilE.warn_mode ->
?remove_invalid:bool ->
exact:bool ->
Cvalue.Model.t -> Locations.Location.t -> Cvalue.V.t -> Cvalue.Model.t
Temporary. Re-export of Cvalue.Model.add_binding
with a with_alarms
argument
val copy_offsetmap : with_alarms:CilE.warn_mode ->
Locations.Location_Bits.t ->
Integer.t ->
Cvalue.Model.t -> [ `Bottom | `Map of Cvalue.Model.offsetmap | `Top ]
Tempory. Re-export of Cvalue.Model.copy_offsetmap
with a with_alarms
argument
val paste_offsetmap : with_alarms:CilE.warn_mode ->
?remove_invalid:bool ->
reducing:bool ->
from:Cvalue.Model.offsetmap ->
dst_loc:Locations.Location_Bits.t ->
size:Integer.t -> exact:bool -> Cvalue.Model.t -> Cvalue.Model.t
Temporary. Re-exportation of Cvalue.Model.paste_offsetmap
with a
~with_alarms
argument. If remove_invalid
is set to true
(default
is false
, dst_loc
will be pre-reduced to its valid part. Should be
set unless you reduce dst_loc
yourself.
val project_with_alarms : with_alarms:CilE.warn_mode ->
conflate_bottom:bool ->
Locations.location -> Cvalue.V_Or_Uninitialized.t -> Cvalue.V.t
val find : with_alarms:CilE.warn_mode ->
?conflate_bottom:bool -> Cvalue.Model.t -> Locations.location -> Cvalue.V.t
Tempory. Re-export of Cvalue.Model.find
with a ~with_alarms
argument
exception Unchanged
exception Reduce_to_bottom
val reduce_by_initialized_defined : (Cvalue.V_Or_Uninitialized.t -> Cvalue.V_Or_Uninitialized.t) ->
Locations.location -> Cvalue.Model.t -> Cvalue.Model.t
val reduce_by_valid_loc : positive:bool ->
for_writing:bool ->
Locations.location -> Cil_types.typ -> Cvalue.Model.t -> Cvalue.Model.t
val apply_on_all_locs : (Locations.location -> 'a -> 'a) -> Locations.location -> 'a -> 'a
apply_all_locs f loc state
folds f
on all the atomic locations
in loc
, provided there are less than plevel
. Useful mainly
when loc
is exact or an over-approximation.
val write_abstract_value : with_alarms:CilE.warn_mode ->
Cvalue.Model.t ->
Cil_types.lval ->
Cil_types.typ -> Locations.Location.t -> Cvalue.V.t -> Cvalue.Model.t
write_abstract_value ~with_alarms state lv typ_lv loc_lv v
writes
v
at
loc_lv
in
state
, casting
v
to respect the type
typ_lv
of
lv
. Currently Does 4 things:
- cast the value to the type of the bitfield it is written into, if needed
- honor an eventual "volatile" qualifier on
lv
- check that
loc_lv
is not catastrophically imprecise.
- perform the actual abstract write