gillian » Gillian » Command_line » Make » External

Parameter Make.External

Parameters

moduleVal : General.Val.S

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

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

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

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

Signature

val execute :
  (PC.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