Tree_borrow (soteria-rust.Soteria_rust_lib.Tree

type tag

and access =

and state =

and protector =

and t

and tb_state

val fresh_tag : unit -> tag

val zero : tag

val pp : Stdlib.Format.formatter -> t -> unit

val pp_tag : Stdlib.Format.formatter -> tag -> unit

val pp_state : Stdlib.Format.formatter -> state -> unit

val pp_tb_state : Stdlib.Format.formatter -> tb_state -> unit

val init : state:state -> unit -> t * tag

val ub_state : t

val add_child : 
  parent:tag ->
  ?protector:protector ->
  state:state ->
  t ->
  t * tag

val unprotect : tag -> t -> t

val strong_protector_exists : t -> bool

val empty_state : tb_state

val set_protector : protected:bool -> tag -> t -> tb_state -> tb_state

val access : 
  tag ->
  access ->
  t ->
  tb_state ->
  (tb_state, [> `AliasingError ], 'm) Rustsymex.Result.t

access root accessed e state: Update all nodes in the mapping state for the tree rooted at root with an event e, that happened at accessed.

val merge : tb_state -> tb_state -> tb_state