Module Csymex.Tree_block

Parameters

module MemVal : sig ... end

Signature

module Expr : sig ... end
type nonrec (!'a, !'sint) tree = {
  1. node : 'a Soteria__Sym_states__Tree_block.node;
  2. range : 'sint * 'sint;
  3. children : (('a, 'sint) Soteria__Sym_states__Tree_block.tree * ('a, 'sint) Soteria__Sym_states__Tree_block.tree) option;
}
module Range : sig ... end
module Split_tree : sig ... end

A Split_tree is a simplified representation of a tree, that has no offset. It however indicates, on Nodes, at what offset the split occurs, relative to that node's start.

module Node : sig ... end
module Tree : sig ... end
type t = {
  1. root : Tree.t;
  2. bound : sint option;
}
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
module SM : sig ... end
val is_empty : t -> bool
val pp_pretty : Stdlib.Format.formatter -> t -> unit
type syn =
  1. | MemVal of {
    1. offset : Expr.t;
    2. len : Expr.t;
    3. v : MemVal.syn;
    }
  2. | Bound of Expr.t
val pp_syn : Ppx_deriving_runtime.Format.formatter -> syn -> Ppx_deriving_runtime.unit
val show_syn : syn -> Ppx_deriving_runtime.string
val ins_outs : syn -> Expr.t list * Expr.t list
val lift_fixes : offset:'a CSYMEX.Value.t -> len:'b CSYMEX.Value.t -> MemVal.syn list -> syn list
val lift_miss : offset:'a CSYMEX.Value.t -> len:'b CSYMEX.Value.t -> ('c, 'd, MemVal.syn list) CSYMEX.Result.t -> ('c, 'd, syn list) CSYMEX.Result.t
val lift_miss_c : offset:'a CSYMEX.Value.t -> len:'b CSYMEX.Value.t -> ('c, MemVal.syn list) CSYMEX.Consumer.t -> ('c, syn list) CSYMEX.Consumer.t
val of_opt : ?mk_fixes:(unit -> 'a list CSYMEX.t) -> 'b option -> ('b, 'c, 'a) CSYMEX.Result.t
val to_opt : t -> t option
val with_bound_check : ?mk_fixes:(unit -> syn list list CSYMEX.t) -> sint -> (Tree.t -> ('a * Tree.t, [> `OutOfBounds ] as 'b, syn list) CSYMEX.Result.t) -> ('a, 'b, syn list) SM.Result.t
val assert_exclusively_owned : t option -> (unit, 'a, syn list) CSYMEX.Result.t
val get_raw_tree_owned : MemVal.S_bounded_int.t CSYMEX.Value.t -> MemVal.S_bounded_int.t CSYMEX.Value.t -> ((MemVal.t, MemVal.S_bounded_int.t CSYMEX.Value.t) Soteria__Sym_states__Tree_block.tree, [> `OutOfBounds ], syn list) SM.Result.t
val put_raw_tree : MemVal.S_bounded_int.t CSYMEX.Value.t -> Tree.t -> (unit, [> `OutOfBounds ], syn list) SM.Result.t
val alloc : MemVal.t -> sint -> t
val to_syn : t -> syn list
val consume_bound : CSYMEX.Value.Expr.t -> t option -> (t option, 'a) CSYMEX.Consumer.t
val produce_bound : Expr.t -> t option -> t option CSYMEX.Producer.t
val produce_mem_val : Expr.t -> Expr.t -> MemVal.syn -> t option -> t option CSYMEX.Producer.t
val consume_mem_val : Expr.t -> Expr.t -> MemVal.syn -> t option -> (t option, syn list) CSYMEX.Consumer.t
val consume : syn -> t option -> (t option, syn list) CSYMEX.Consumer.t
val produce : syn -> t option -> t option CSYMEX.Producer.t