module Eval_op: sig
.. end
Numeric evaluation. Factored with evaluation in the logic.
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_size_t : Cvalue.V.t -> Cvalue.V_Offsetmap.t option
Specialization of the function above for standard types
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 v_uninit_of_offsetmap : with_alarms:CilE.warn_mode ->
typ:Cil_types.typ -> Cvalue.V_Offsetmap.t -> Cvalue.V_Or_Uninitialized.t
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 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 eval_binop_float : with_alarms:CilE.warn_mode ->
Fval.rounding_mode ->
Cil_types.fkind option ->
Cvalue.V.t -> Cil_types.binop -> 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_unop : check_overflow:bool ->
with_alarms:CilE.warn_mode ->
Cvalue.V.t -> Cil_types.typ -> Cil_types.unop -> Cvalue.V.t
val handle_overflow : with_alarms:CilE.warn_mode ->
warn_unsigned:bool -> Cil_types.typ -> Cvalue.V.t -> Cvalue.V.t
val do_promotion : with_alarms:CilE.warn_mode ->
Fval.rounding_mode ->
src_typ:Cil_types.typ ->
dst_typ:Cil_types.typ ->
Cvalue.V.t -> (Format.formatter -> unit) -> Cvalue.V.t
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 backward_comp_left_from_type : Cil_types.typ ->
bool -> Abstract_interp.Comp.t -> Cvalue.V.t -> Cvalue.V.t -> Cvalue.V.t
Reduction of a Cvalue.V.t
by ==
, !=
, >=
, >
, <=
and <
.
backward_comp_left_from_type positive op l r
reduces l
so that the relation l op r
holds. typ
is the type of l
.
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
val add_binding : with_alarms:CilE.warn_mode ->
?remove_invalid:bool ->
exact:bool ->
Cvalue.Model.t -> Locations.location -> Cvalue.V.t -> Cvalue.Model.t
Temporary. Re-export of Cvalue.Model.add_binding
with a with_alarms
argument
val add_binding_unspecified : with_alarms:CilE.warn_mode ->
?remove_invalid:bool ->
exact:bool ->
Cvalue.Model.t ->
Locations.location -> Cvalue.V_Or_Uninitialized.t -> Cvalue.Model.t
Temporary. Re-export of Cvalue.Model.add_binding_unspecifed
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.V_Offsetmap.t | `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.V_Offsetmap.t ->
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 reduce_by_initialized_defined : (Cvalue.V_Or_Uninitialized.t -> Cvalue.V_Or_Uninitialized.t) ->
Locations.location -> 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 reduce_by_valid_loc : positive:bool ->
for_writing:bool ->
Locations.location -> Cil_types.typ -> Cvalue.Model.t -> Cvalue.Model.t
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
val make_loc_contiguous : Locations.location -> Locations.location
'Simplify' the location if it represents a contiguous zone: instead
of multiple offsets with a small size, change it into a single offset
with a size that covers the entire range.
val pretty_stitched_offsetmap : Format.formatter -> Cil_types.typ -> Cvalue.V_Offsetmap.t -> unit