gillian » Gillian » General » External » T » S

Module type T.S

Parameters

moduleVal : Val.S

moduleESubst : ESubst.S with type vt = Val.t and type t = Val.et

moduleStore : Store.S with type vt = Val.t

moduleState :
  State.S
    with type vt = Val.t
     and type st = ESubst.t
     and type store_t = Store.t

moduleCall_stack : Call_stack.S with type vt = Val.t and type store_t = Store.t

Signature

val execute :
  (Annot.t, int) 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