Module MemVal.S_bounded_int

include module type of struct include Typed end
include module type of struct include Soteria.Bv_values.Typed end

Phantom types

Types

val pp_ty : (Stdlib.Format.formatter -> 'a ty -> unit) -> Stdlib.Format.formatter -> 'a ty -> unit
val ppa_ty : Stdlib.Format.formatter -> 'a ty -> unit
val equal_ty : 'a ty -> 'b ty -> bool
val t_bool : [> T.sbool ] ty
val t_int : int -> [> T.sint ] ty
val t_seq : ([< T.any ] as 'a) ty -> [> 'a T.sseq ] ty
val t_f16 : [> T.sfloat ] ty
val t_f32 : [> T.sfloat ] ty
val t_f64 : [> T.sfloat ] ty
val t_f128 : [> T.sfloat ] ty

Typed svalues

type sbool = T.sbool

Basic value operations

val is_bool_ty : 'a ty -> bool
val type_type : Soteria.Bv_values.Svalue.ty -> 'a ty
val untype_type : 'a ty -> Soteria.Bv_values.Svalue.ty
val iter_vars : 'a Soteria.Bv_values.Typed.t -> ((Soteria.Symex.Var.t * 'b ty) -> unit) -> unit
val type_ : Soteria.Bv_values.Svalue.t -> 'a Soteria.Bv_values.Typed.t
val type_checked : Soteria.Bv_values.Svalue.t -> 'a ty -> 'a Soteria.Bv_values.Typed.t option
val cast_checked : 'a Soteria.Bv_values.Typed.t -> 'b ty -> 'b Soteria.Bv_values.Typed.t option
val cast_int : 'a Soteria.Bv_values.Typed.t -> ([> T.sint ] Soteria.Bv_values.Typed.t * int) option
val is_float : 'a ty -> bool
val size_of_int : [< T.sint ] Soteria.Bv_values.Typed.t -> int
val untyped_list : 'a Soteria.Bv_values.Typed.t list -> Soteria.Bv_values.Svalue.t list
val pp : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a Soteria.Bv_values.Typed.t -> unit
val ppa : Stdlib.Format.formatter -> 'a Soteria.Bv_values.Typed.t -> unit
val equal : ([< T.any ] as 'a) Soteria.Bv_values.Typed.t -> 'a Soteria.Bv_values.Typed.t -> bool
val compare : ([< T.any ] as 'a) Soteria.Bv_values.Typed.t -> 'a Soteria.Bv_values.Typed.t -> int
val hash : ('a -> int) -> 'a Soteria.Bv_values.Typed.t -> int
val hasha : 'a Soteria.Bv_values.Typed.t -> int
val unique_tag : [< T.any ] Soteria.Bv_values.Typed.t -> int

Typed constructors

Boolean operations

module type Bool_ := sig ... end
include Bool_
val v_false : [> sbool ] Soteria.Bv_values.Typed.t

Similar to and_, but the rhs is only evaluated if the lhs is not the concrete false. In other words, this is a short-circuiting and. Avoids some errors, like a division by zero in 0 != x && n / x when x is 0.

val split_ands : [< sbool ] Soteria.Bv_values.Typed.t -> ([> sbool ] Soteria.Bv_values.Typed.t -> unit) -> unit

Similar to or_, but the rhs is only evaluated if the lhs is not the concrete true. In other words, this is a short-circuiting or. Avoids some errors, like a division by zero in 0 == x || n / x when x is 0.

Floating point operations

val ptr_bits : int
val c_int_bits : int
val t_loc : [> T.sloc ] ty
val t_ptr : [> T.sptr ] ty
val t_usize : [> T.sint ] ty
module BitVec = Typed.BitVec
module Ptr = Typed.Ptr
module Syntax = Typed.Syntax
include module type of struct include Typed.BitVec end
include module type of struct include Soteria.Bv_values.Typed.BitVec end
val mki_masked : int -> int -> [> Soteria.Bv_values.Typed.T.sint ] Soteria.Bv_values.Typed.t
val bv_to_z : bool -> int -> Z.t -> Z.t
val mod_ : [< Soteria.Bv_values.Typed.T.sint ] Soteria.Bv_values.Typed.t -> [< Soteria.Bv_values.Typed.T.sint ] Soteria.Bv_values.Typed.t -> [> Soteria.Bv_values.Typed.T.sint_ovf ] Soteria.Bv_values.Typed.t
val and_ : [< Soteria.Bv_values.Typed.T.sint ] Soteria.Bv_values.Typed.t -> [< Soteria.Bv_values.Typed.T.sint ] Soteria.Bv_values.Typed.t -> [> Soteria.Bv_values.Typed.T.sint ] Soteria.Bv_values.Typed.t
val or_ : [< Soteria.Bv_values.Typed.T.sint ] Soteria.Bv_values.Typed.t -> [< Soteria.Bv_values.Typed.T.sint ] Soteria.Bv_values.Typed.t -> [> Soteria.Bv_values.Typed.T.sint ] Soteria.Bv_values.Typed.t
val of_bool : [< Soteria__Bv_values__Typed.sbool ] Soteria__Bv_values__Typed.t -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
val usize : Z.t -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
val usizenz : Z.t -> [> Soteria__Bv_values__Typed.T.nonzero ] Soteria__Bv_values__Typed.t
val usizei : int -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
val usizeinz : int -> [> Soteria__Bv_values__Typed.T.nonzero ] Soteria__Bv_values__Typed.t
val isize_max : [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
val sure_is_zero : [< Soteria__Bv_values__Typed.T.any ] Soteria__Bv_values__Typed.t -> bool
val fit_to : ?signed:bool -> int -> [ `NonZero | `Zero ] Typed.t -> [ `NonZero | `Zero ] Typed.t
val cast_to_size_t : 'a Typed.t -> Soteria_c_lib.Typed.T.sint Typed.t option
type t = T.sint
val of_z : Z.t -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
val zero : unit -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
val one : unit -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
val lt : [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t -> [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t -> [> Soteria__Bv_values__Typed.sbool ] Soteria__Bv_values__Typed.t
val leq : [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t -> [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t -> [> Soteria__Bv_values__Typed.sbool ] Soteria__Bv_values__Typed.t
val add : [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t -> [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
val sub : [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t -> [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
val is_in_bound : t Typed.t -> sbool Typed.t