Frama-C API - Eval_op
Numeric evaluation. Factored with evaluation in the logic.
val offsetmap_of_v : typ:Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V_Offsetmap.tTransformation a value into an offsetmap of size sizeof(typ) bytes.
val offsetmap_of_loc : Frama_c_kernel.Precise_locs.precise_location -> Frama_c_kernel.Cvalue.Model.t -> Frama_c_kernel.Cvalue.V_Offsetmap.t Eval.or_bottomReturns the offsetmap at a precise_location from a state.
val backward_comp_left_from_type : Frama_c_kernel.Cil_types.logic_type -> bool -> Frama_c_kernel.Abstract_interp.Comp.t -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Cvalue.V.tReduction 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 : (Frama_c_kernel.Cvalue.V_Or_Uninitialized.t -> Frama_c_kernel.Cvalue.V_Or_Uninitialized.t) -> Frama_c_kernel.Locations.location -> Frama_c_kernel.Cvalue.Model.t -> Frama_c_kernel.Cvalue.Model.tval apply_on_all_locs : (Frama_c_kernel.Locations.location -> 'a -> 'a) -> Frama_c_kernel.Locations.location -> 'a -> 'aapply_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 -> Frama_c_kernel.Locations.access -> Frama_c_kernel.Locations.location -> Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cvalue.Model.t -> Frama_c_kernel.Cvalue.Model.tval make_loc_contiguous : Frama_c_kernel.Locations.location -> Frama_c_kernel.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 : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cvalue.V_Offsetmap.t -> unitval pretty_offsetmap : Frama_c_kernel.Cil_types.typ -> Stdlib.Format.formatter -> Frama_c_kernel.Cvalue.V_Offsetmap.t -> unitval find_under_approximation : Frama_c_kernel.Cvalue.Model.t -> Frama_c_kernel.Locations.location -> Frama_c_kernel.Cvalue.V_Or_Uninitialized.t option