Module Eval_op

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 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 ->
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 do_promotion : with_alarms:CilE.warn_mode ->
Fval.rounding_mode ->
src_typ:Cil_types.typ -> dst_typ:Cil_types.typ -> Cvalue.V.t -> Cvalue.V.t
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 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 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