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 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 reduce_rel_from_type : Cil_types.typ ->
bool -> Cil_types.binop -> Cvalue.V.t -> Cvalue.V.t -> Cvalue.V.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 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:
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