ExternalP (gillian.Bulk.Outcome.Make

Parameters

module Val : Gillian.General.Val.S

module ESubst : Gillian.General.ESubst.S with type vt = Val.t and type t = Val.et

module Store : Gillian.General.Store.S with type vt = Val.t

module State : 
  Gillian.General.State.S
    with type vt = Val.t
     and type st = ESubst.t
     and type store_t = Store.t

module Call_stack : Gillian.General.Call_stack.S with type vt = Val.t and type store_t = Store.t

Signature

val execute : 
  (PC.Annot.t, int) Gillian.Gil_syntax.Prog.t ->
  State.t ->
  Call_stack.t ->
  int ->
  string ->
  string ->
  Val.t list ->
  int option ->
  (State.t * Call_stack.t * int * int) list