Ctree_block (soteria-c.Soteria_c_lib.Ctree

module Ctype = Cerb_frontend.Ctype

module MemVal : sig ... end

include sig ... end

module Expr : sig ... end

type nonrec sint =
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t

type nonrec (!'a, !'sint) tree = {

node : 'a Soteria__Sym_states__Tree_block.node;
range : 'sint * 'sint;
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 = {

root : Tree.t;
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 =

| MemVal of {
1. offset : Expr.t;
2. len : Expr.t;
3. v : MemVal.syn;
}
| 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 Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  len:'b Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  MemVal.syn list ->
  syn list

val lift_miss : 
  offset:'a Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  len:'b Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  (Cerb_location.t ->
    (('c, 'd, MemVal.syn list) Soteria.Symex.Compo_res.t * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  Cerb_location.t ->
  (('c, 'd, syn list) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val lift_miss_c : 
  offset:'a Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  len:'b Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  ('c, MemVal.syn list) Soteria_c_lib__Csymex.CSYMEX.Consumer.t ->
  ('c, syn list) Soteria_c_lib__Csymex.CSYMEX.Consumer.t

val of_opt : 
  ?mk_fixes:
    (unit ->
      Cerb_location.t ->
      ('a list * Cerb_location.t)
        Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  'b option ->
  Cerb_location.t ->
  (('b, 'c, 'a) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val to_opt : t -> t option

val with_bound_check : 
  ?mk_fixes:
    (unit ->
      Cerb_location.t ->
      (syn list list * Cerb_location.t)
        Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  sint ->
  (Tree.t ->
    Cerb_location.t ->
    (('a * Tree.t, [> `OutOfBounds ] as 'b, syn list) Soteria.Symex.Compo_res.t
     * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  ('a, 'b, syn list) SM.Result.t

val assert_exclusively_owned : 
  t option ->
  Cerb_location.t ->
  ((unit, 'a, syn list) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val get_raw_tree_owned : 
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  ((MemVal.t,
     MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t)
     Soteria__Sym_states__Tree_block.tree,
    [> `OutOfBounds ],
    syn list)
    SM.Result.t

val put_raw_tree : 
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  Tree.t ->
  (unit, [> `OutOfBounds ], syn list) SM.Result.t

val to_syn : t -> syn list

val consume_bound : 
  Soteria.Bv_values.Bv_solver.Z3_solver.Value.Expr.t ->
  t option ->
  (t option, 'a) Soteria_c_lib__Csymex.CSYMEX.Consumer.t

val produce_bound : 
  Expr.t ->
  t option ->
  t option Soteria_c_lib__Csymex.CSYMEX.Producer.t

val produce_mem_val : 
  Expr.t ->
  Expr.t ->
  MemVal.syn ->
  t option ->
  t option Soteria_c_lib__Csymex.CSYMEX.Producer.t

val consume_mem_val : 
  Expr.t ->
  Expr.t ->
  MemVal.syn ->
  t option ->
  (t option, syn list) Soteria_c_lib__Csymex.CSYMEX.Consumer.t

val consume : 
  syn ->
  t option ->
  (t option, syn list) Soteria_c_lib__Csymex.CSYMEX.Consumer.t

val produce : 
  syn ->
  t option ->
  t option Soteria_c_lib__Csymex.CSYMEX.Producer.t

val log_fixes : syn list list -> syn list list

val range_of_low_and_type : 
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  Soteria_c_lib.Layout.CF.Ctype.ctype ->
  Cerb_location.t ->
  ((MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
    * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t)
   * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val sval_leaf : 
  range:('a * 'a) ->
  value:Soteria_c_lib.Typed.T.cval Typed.t ->
  ty:Ctype.ctype ->
  (MemVal.t, 'a) Soteria__Sym_states__Tree_block.tree

val zeros : 
  range:('a * 'a) ->
  (MemVal.t, 'a) Soteria__Sym_states__Tree_block.tree

val uninit : 
  range:('a * 'a) ->
  (MemVal.t, 'a) Soteria__Sym_states__Tree_block.tree

val mk_fix_typed : 
  'a Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  Soteria_c_lib.Layout.CF.Ctype.ctype ->
  unit ->
  Cerb_location.t ->
  (syn list list * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val mk_fix_any : 
  'a Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  'b Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  unit ->
  syn list list

val mk_fix_any_s : 
  'a Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  'b Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  unit ->
  syn list list Csymex.t

val decode : 
  ty:Ctype.ctype ->
  ofs:'a Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  MemVal.t MemVal.TB.node ->
  (Soteria_c_lib.Typed.T.cval Typed.t,
    [> `UninitializedMemoryAccess ],
    syn list)
    Csymex.Result.t

val load : 
  Soteria_c_lib.Typed.T.sint Typed.t ->
  Ctype.ctype ->
  (Soteria_c_lib.Typed.T.cval Typed.t,
    [> `OutOfBounds | `UninitializedMemoryAccess ],
    syn list)
    SM.Result.t

val store : 
  Soteria_c_lib.Typed.T.sint Typed.t ->
  Ctype.ctype ->
  Soteria_c_lib.Typed.T.cval Typed.t ->
  (unit, [> `OutOfBounds ], syn list) SM.Result.t

val zero_range : 
  Soteria_c_lib.Typed.T.sint Typed.t ->
  Soteria_c_lib.Typed.T.sint Typed.t ->
  (unit, [> `OutOfBounds ], syn list) SM.Result.t

val deinit : 
  Soteria_c_lib.Typed.T.sint Typed.t ->
  Soteria_c_lib.Typed.T.sint Typed.t ->
  (unit, [> `OutOfBounds ], syn list) SM.Result.t

val alloc : zeroed:bool -> sint -> t