Module Cvalue.V

module V: sig .. end
Values.

include Location_Bytes
Values are essentially bytes-indexed locations, the NULL base representing basic integers or float. Operations that are not related to locations (ie that are not present in Location_Bytes) are defined below.
include Offsetmap_lattice_with_isotropy
val pretty_typ : Cil_types.typ option -> t Pretty_utils.formatter
exception Not_based_on_null
val project_ival : t -> Ival.t
Raises Not_based_on_null if the value may be a pointer.
val project_ival_bottom : t -> Ival.t
val min_and_max_float : t -> Ival.F.t * Ival.F.t
val is_imprecise : t -> bool
val is_topint : t -> bool
val is_bottom : t -> bool
val is_isotropic : t -> bool
val contains_zero : t -> bool
val contains_non_zero : t -> bool
val of_char : char -> t
val of_int64 : int64 -> t
val subdiv_float_interval : size:int -> t -> t * t
val compare_min_float : t -> t -> int
val compare_max_float : t -> t -> int
val compare_min_int : t -> t -> int
val compare_max_int : t -> t -> int
val filter_le_ge_lt_gt_int : Cil_types.binop -> t -> cond_expr:t -> t
val filter_le_ge_lt_gt_float : Cil_types.binop ->
bool -> Ival.Float_abstract.float_kind -> t -> cond_expr:t -> t
val eval_comp : signed:bool -> Cil_types.binop -> t -> t -> t
Can only be called on the 6 comparison operators
val inject_int : Abstract_interp.Int.t -> t
val interp_boolean : contains_zero:bool -> contains_non_zero:bool -> t
val cast : size:Abstract_interp.Int.t -> signed:bool -> t -> t * bool
cast ~size ~signed v applies to the abstract value v the conversion to the integer type described by size and signed. The results are new_value, ok. The boolean ok, when true, indicates that no imprecision was introduced. Offsets of bases other than Null are not clipped. If they were clipped, they should be clipped at the validity of the base. The C standard does not say that p+(1ULL<<32+1) is the same as p+1, it says that p+(1ULL<<32+1) is invalid.
val cast_float : rounding_mode:Ival.Float_abstract.rounding_mode -> t -> bool * bool * t
val cast_double : t -> bool * bool * t
val cast_float_to_int : signed:bool -> size:int -> t -> bool * bool * (bool * bool) * t
val cast_float_to_int_inverse : single_precision:bool -> t -> t
val cast_int_to_float : Ival.Float_abstract.rounding_mode -> t -> t * bool
val add_untyped : Int_Base.t -> t -> t -> t
val add_untyped_under : Int_Base.t -> t -> t -> t
val sub_untyped_pointwise : t -> t -> Ival.t * bool
Substracts two pointers (assumed to have type char*) and returns the difference of their offsets. The two pointers are supposed to be pointing to the same base; the returned boolean indicates that this assumption might be incorrect.
val mul : t -> t -> t
val div : t -> t -> t
val c_rem : t -> t -> t
val shift_right : t -> t -> t
val shift_left : t -> t -> t
val bitwise_and : signed:bool -> size:int -> t -> t -> t
val bitwise_xor : t -> t -> t
val bitwise_or : t -> t -> t
val all_values : size:Abstract_interp.Int.t -> t -> bool
val create_all_values : modu:Abstract_interp.Int.t -> signed:bool -> size:int -> t