Module Astral_internal.StackHeapModel

module Location : sig ... end
module Footprint : sig ... end
module Value : sig ... end
module Stack : sig ... end
module Heap : sig ... end
type t = private {
  1. stack : Stack.t;
  2. heap : Heap.t;
  3. footprints : Footprint.t SL.Map.t;
  4. heaps : Heap.t SL.Map.t;
}
val empty : t
val init : ?footprints:Footprint.t SL.Map.t -> ?heaps:Heap.t SL.Map.t -> Stack.t -> Heap.t -> t
val eval : t -> SL.Term.t -> Location.t
val filter_vars : (SL.Variable.t -> bool) -> t -> t
val succ_field : t -> MemoryModel.Field.t -> Location.t -> Location.t
val domain : t -> Footprint.t
val to_smtlib : t -> string
val has_path : ?field:MemoryModel.Field.t -> t -> src:Location.t -> dst:Location.t -> bool
val get_path : ?field:MemoryModel.Field.t -> t -> src:Location.t -> dst:Location.t -> Location.t list

Compute path from src to dst (excluded) via field. If field is not specified, consider all edges.

val has_nested_path : t -> src:Location.t -> dst:Location.t -> sink:Location.t -> field1:MemoryModel.Field.t -> field2:MemoryModel.Field.t -> bool
val get_nested_path : t -> src:Location.t -> dst:Location.t -> sink:Location.t -> field1:MemoryModel.Field.t -> field2:MemoryModel.Field.t -> Location.t list list
val output_graph : string -> t -> unit
include Datatype_sig.PRINTABLE with type t := t
include Datatype_sig.SHOW with type t := t
val show : t -> string

String representation of type t

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

Output to formatter

val print : ?prefix:string -> t -> unit

Output to stdout.

val show_option : t option -> string
val print_option : ?prefix:string -> t option -> unit
val dump : string -> t -> unit

Dump to file given by filename

Lists of printable values

val show_list : ?separator:string -> t list -> string
val pp_list : Stdlib.Format.formatter -> t list -> unit
val print_list : ?separator:string -> ?prefix:string -> t list -> unit