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
val is_arithmetic : t -> bool
Returns true if the value may not be a pointer.
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 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 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 backward_mult_int_left : right:t -> result:t -> t option Bottom.or_bottom
val backward_comp_int_left : Abstract_interp.Comp.t -> t -> t -> t
val backward_comp_float_left : Abstract_interp.Comp.t -> bool -> Fval.float_kind -> t -> t -> t
val forward_comp_int : signed:bool ->
Abstract_interp.Comp.t -> t -> t -> Abstract_interp.Comp.result
val inject_comp_result : Abstract_interp.Comp.result -> t
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:Fval.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 option
val cast_int_to_float : Fval.rounding_mode -> t -> t * bool
val cast_int_to_float_inverse : single_precision:bool -> t -> t option
val add_untyped : factor:Int_Base.t -> t -> t -> t
add_untyped ~factor e1 e2 computes e1+factor*e2 using C semantic for +, i.e. ptr+v is add_untyped ~factor:sizeof( *ptr ) ptr v. (Thus, factor is in bytes.) This function handles simultaneously PlusA, MinusA, PlusPI, MinusPI and sometimes MinusPP, by setting factor accordingly. This is more precise than having multiple functions, as computations such as (int)&t[1] - (int)&t[2] would not be treated precisely otherwise.
val add_untyped_under : factor:Int_Base.t -> t -> t -> t
Under-approximating variant of Cvalue.V.add_untyped. Takes two under-approximation, and returns an under-approximation.
val sub_untyped_pointwise : ?factor:Int_Base.t -> t -> t -> Ival.t * bool
See Locations.sub_pointwise. In this module, factor is expressed in bytes. 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 bitwise_not : t -> t
val bitwise_not_size : signed:bool -> size:int -> t -> t
val all_values : size:Abstract_interp.Int.t -> t -> bool
all_values ~size v returns true iff v contains all integer values representable in size bits.
val create_all_values : signed:bool -> size:int -> t