Frame_range (soteria-c.Soteria_c_lib.Ctree_block.Tree.Frame

Parameters

module M : sig ... end

Signature

val (let*) : ('a, 'b, 'c) M.t -> ('a -> ('d, 'b, 'c) M.t) -> ('d, 'b, 'c) M.t

val (let+) : ('a, 'b, 'c) M.t -> ('a -> 'd) -> ('d, 'b, 'c) M.t

val (let*^) : 
  (Cerb_location.t ->
    ('a * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  ('a -> ('b, 'c, 'd) M.t) ->
  ('b, 'c, 'd) M.t

val (let+^) : 
  (Cerb_location.t ->
    ('a * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  ('a -> 'b) ->
  ('b, 'c, 'd) M.t

val frame_range : 
  t ->
  replace_node:(t -> (t, 'b, 'c) M.t) ->
  rebuild_parent:
    ((MemVal.t, sint) tree ->
      left:t ->
      right:t ->
      Cerb_location.t ->
      ((MemVal.t, sint) tree * Cerb_location.t)
        Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  Range.t ->
  (t * t, 'b, 'c) M.t