Module External.M

JSIL external procedure calls

Parameters

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

Signature

val execute_printf : 'a -> State.t -> 'b -> int -> Gillian.Gil_syntax.Var.t -> Val.t list -> 'c -> (State.t * 'b * int * int) list
val execute : ('a, 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

General External Procedure Treatment

  • parameter prog

    GIL program

  • parameter state

    Current state

  • parameter cs

    Current call stack

  • parameter i

    Current index

  • parameter x

    Variable that stores the result

  • parameter pid

    Procedure identifier

  • parameter v_args

    Parameters

  • parameter j

    Optional error index

  • returns

    Resulting configuration