Module Eval_op

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: