StateKey (soteria-rust.Soteria_rust_lib.State.Tree

include module type of struct include Typed end

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

Phantom types

module T = Soteria_rust_lib.Typed.T

type +'a ty = 'a Soteria.Bv_values.Typed.ty

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 get_ty : 'a Soteria.Bv_values.Typed.t -> Soteria.Bv_values.Svalue.ty

val type_type : Soteria.Bv_values.Svalue.ty -> 'a ty

val untype_type : 'a ty -> Soteria.Bv_values.Svalue.ty

val kind : 'a Soteria.Bv_values.Typed.t -> Soteria.Bv_values.Svalue.t_kind

val mk_var : Soteria.Symex.Var.t -> 'a ty -> 'a Soteria.Bv_values.Typed.t

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 : 'a Soteria.Bv_values.Typed.t -> 'b Soteria.Bv_values.Typed.t

val is_float : 'a ty -> bool

val size_of_int : [< T.sint ] Soteria.Bv_values.Typed.t -> int

val untyped : 'a Soteria.Bv_values.Typed.t -> Soteria.Bv_values.Svalue.t

val untyped_list : 
  'a Soteria.Bv_values.Typed.t list ->
  Soteria.Bv_values.Svalue.t list

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

val sem_eq : 
  'a Soteria.Bv_values.Typed.t ->
  'a Soteria.Bv_values.Typed.t ->
  sbool Soteria.Bv_values.Typed.t

val sem_eq_untyped : 
  'a Soteria.Bv_values.Typed.t ->
  'b Soteria.Bv_values.Typed.t ->
  sbool Soteria.Bv_values.Typed.t

Boolean operations

module type Bool_ := sig ... end

include Bool_

val v_true : [> sbool ] Soteria.Bv_values.Typed.t

val v_false : [> sbool ] Soteria.Bv_values.Typed.t

val of_bool : bool -> [> sbool ] Soteria.Bv_values.Typed.t

val to_bool : 'a Soteria.Bv_values.Typed.t -> bool option

val and_ : 
  [< sbool ] Soteria.Bv_values.Typed.t ->
  [< sbool ] Soteria.Bv_values.Typed.t ->
  [> sbool ] Soteria.Bv_values.Typed.t

val and_lazy : 
  [< sbool ] Soteria.Bv_values.Typed.t ->
  (unit -> [< sbool ] Soteria.Bv_values.Typed.t) ->
  [> 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 conj : 
  [< sbool ] Soteria.Bv_values.Typed.t list ->
  [> sbool ] Soteria.Bv_values.Typed.t

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

val or_ : 
  [< sbool ] Soteria.Bv_values.Typed.t ->
  [< sbool ] Soteria.Bv_values.Typed.t ->
  [> sbool ] Soteria.Bv_values.Typed.t

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

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.

val not : 
  [< sbool ] Soteria.Bv_values.Typed.t ->
  [> sbool ] Soteria.Bv_values.Typed.t

val ite : 
  [< sbool ] Soteria.Bv_values.Typed.t ->
  'a Soteria.Bv_values.Typed.t ->
  'a Soteria.Bv_values.Typed.t ->
  'a Soteria.Bv_values.Typed.t

module Bool = Soteria_rust_lib.Typed.Bool

Floating point operations

module SSeq = Soteria_rust_lib.Typed.SSeq

module Infix = Soteria_rust_lib.Typed.Infix

module Expr = Soteria_rust_lib.Typed.Expr

exception CastError of T.any Soteria.Bv_values.Typed.t * T.any ty * T.any ty

CastError (value, expected, got)

val cast_error : 
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero ]
    Soteria.Bv_values.Typed.t ->
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero ]
    ty ->
  'a

val t_ptr : unit -> [> T.sptr ] ty

val t_loc : unit -> [> T.sloc ] ty

val t_usize : unit -> [> T.sint ] ty

val t_lit : Charon.Types.literal_type -> [< T.cval Float NonZero Zero ] ty

val t_float : Charon.Types.float_type -> T.sfloat ty

val cast_checked : 
  ty:
    ([< `Bool
     | `Float
     | `List of T.any & T.any
     | `Loc
     | `NonZero
     | `Overflowed
     | `Ptr
     | `Zero ] as 'a)
      ty ->
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero ]
    Soteria.Bv_values.Typed.t ->
  'a Soteria.Bv_values.Typed.t

val cast_checked2 : 
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero ]
    Soteria.Bv_values.Typed.t ->
  'a Soteria.Bv_values.Typed.t ->
  'b Soteria.Bv_values.Typed.t * 'c Soteria.Bv_values.Typed.t * 'd ty

val cast_lit : 
  Charon.Types.literal_type ->
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero ]
    Soteria.Bv_values.Typed.t ->
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero NonZero Zero ]
    Soteria.Bv_values.Typed.t

val cast_i : 
  Charon.Values.u_int_ty ->
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero ]
    Soteria.Bv_values.Typed.t ->
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero NonZero Zero ]
    Soteria.Bv_values.Typed.t

val cast_f : 
  Charon.Types.float_type ->
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero ]
    Soteria.Bv_values.Typed.t ->
  T.sfloat Soteria.Bv_values.Typed.t

val cast_float : 
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero ]
    Soteria.Bv_values.Typed.t ->
  [> T.sfloat ] Soteria.Bv_values.Typed.t

val cast_int : 
  [< `Bool
  | `Float
  | `List of T.any & T.any
  | `Loc
  | `NonZero
  | `Overflowed
  | `Ptr
  | `Zero ]
    Soteria.Bv_values.Typed.t ->
  [> T.sint ] Soteria.Bv_values.Typed.t * int

DEPRECATED: it is unlikely you need this; the interpreter should be well typed

module BitVec = Typed.BitVec

module BV = Soteria_rust_lib.Typed.BV

module Float = Typed.Float

module Ptr = Typed.Ptr

module Syntax = Typed.Syntax

type t = T.sloc Typed.t

type syn = Expr.t

val pp_syn : 
  Ppx_deriving_runtime.Format.formatter ->
  syn ->
  Ppx_deriving_runtime.unit

val show_syn : syn -> Ppx_deriving_runtime.string

val to_syn : 'a Soteria__Bv_values__Typed.t -> Expr.t

val learn_eq : syn -> t -> (unit, 'a) DecayMapMonad.Consumer.t

val exprs_syn : 'a -> 'a list

val subst : 
  (Expr.t -> 'a Soteria__Bv_values__Typed.t) ->
  Expr.t ->
  'b Soteria__Bv_values__Typed.t

val pp : Stdlib.Format.formatter -> 'a Soteria.Bv_values.Typed.t -> unit

val show : [ `Loc ] Soteria.Bv_values.Typed.t -> string

val to_int : [< T.any ] Soteria.Bv_values.Typed.t -> int

val concrete_loc : int Stdlib.ref

val simplify : 
  'a DecayMapMonad.Value.t ->
  'a DecayMapMonad.Value.t DecayMapMonad.t

val distinct : 
  'a Soteria.Bv_values.Typed.t list ->
  [> sbool ] Soteria.Bv_values.Typed.t

val fresh : 
  unit ->
  [> Soteria__Bv_values__Typed.T.sloc ] DecayMapMonad.Value.t DecayMapMonad.t