Make_Symbolic (gillian.Bulk.Outcome.Make

Parameters

module SMemory : Engine.SMemory.S

module PC : sig ... end

module ExternalP : Engine.External.T(PC.Annot).S

Signature

module Val : sig ... end

module ESubst : sig ... end

module Store : sig ... end

module State : sig ... end

module ParserAndCompiler : sig ... end

module External
  (Val : Gillian.General.Val.S)
  (ESubst : sig ... end)
  (Store : sig ... end)
  (State : sig ... end)
  (Call_stack : sig ... end) : 
  sig ... end

type t =
  Make(Gillian.Symbolic.Values)(Gillian.Symbolic.Subst)(Engine.SStore)(Engine.SState.Make(SMemory))(PC)(ExternalP).t =

| ParseAndCompileError of ParserAndCompiler.err
| FailedExec of string
| FinishedExec of (State.t, Val.t, (Val.t, State.err_t) Gillian.General.Exec_err.t) Engine.Exec_res.t list

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

val pp_what_branch_did : 
  Stdlib.Format.formatter ->
  (State.t, Val.t, (Val.t, State.err_t) Gillian.General.Exec_err.t)
    Engine.Exec_res.t ->
  unit