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_float : t -> Fval.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 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_true : Abstract_interp.Comp.t -> Fval.kind -> t -> t -> t
val backward_comp_float_left_false : Abstract_interp.Comp.t -> Fval.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 inject_float : Fval.t -> t
val interp_boolean : contains_zero:bool -> contains_non_zero:bool -> t
val cast_int_to_int : size:Abstract_interp.Int.t -> signed:bool -> t -> t
cast_int_to_int ~size ~signed v applies to the abstract value v the conversion to the integer type described by size and signed. 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 reinterpret_as_float : Cil_types.fkind -> t -> t
val reinterpret_as_int : signed:bool -> size:Integer.t -> t -> t
val cast_float_to_float : Fval.kind -> t -> t
val cast_float_to_int : signed:bool -> size:int -> t -> t
val cast_float_to_int_inverse : single_precision:bool -> t -> t option
val cast_int_to_float : Fval.kind -> t -> t
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
See Locations.sub_pointwise. In this module, factor is expressed in bytes.
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 : t -> t -> t
val bitwise_xor : t -> t -> t
val bitwise_or : t -> t -> t
val bitwise_signed_not : t -> t
val bitwise_not : size:int -> signed:bool -> 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
val cardinal_estimate : t -> size:Abstract_interp.Int.t -> Abstract_interp.Int.t
cardinal_estimate v ~size returns an estimation of the cardinal of v, knowing that v fits in size bits.