Module Js2jsil_lib.JSIL2GIL

module Gil = Gillian.Gil_syntax
module GAsrt = Gil.Asrt
module GSLCmd = Gil.SLCmd
module GLCmd = Gil.LCmd
module GSpec = Gil.Spec
module GLemma = Gil.Lemma
module GPred = Gil.Pred
module GMacro = Gil.Macro
module GProc = Gil.Proc
module GProg = Gil.Prog
module GBiSpec = Gil.BiSpec
module GCmd = Gil.Cmd
module Expr = Gil.Expr
module Annot = Gil.Annot
val fresh_sth : string -> (unit -> string) * (unit -> unit)

* Fresh identifiers

val fresh_then : unit -> string
val reset_then : unit -> unit
val fresh_else : unit -> string
val reset_else : unit -> unit
val fresh_var : unit -> string
val reset_var : unit -> unit
val resource_error : Gillian.Gil_syntax.Expr.t list -> 'a GCmd.t
val reset_generators : unit -> unit
val jsil2gil_expr : Expr.t -> Expr.t
val jsil2gil_asrt : Jsil_syntax.Asrt.t -> GAsrt.t
val jsil2gil_slcmd : Jsil_syntax.SLCmd.t -> GSLCmd.t
val jsil2gil_lcmd : Jsil_syntax.LCmd.t -> GLCmd.t
val jsil2gil_sspec : Jsil_syntax.Spec.st -> GSpec.st
val jsil2gil_spec : Jsil_syntax.Spec.t -> GSpec.t
val jsil2gil_lemma : Jsil_syntax.Lemma.t -> GLemma.t
val jsil2gil_pred : Jsil_syntax.Pred.t -> GPred.t
val jsil2gil_macro : Jsil_syntax.Macro.t -> GMacro.t
val jsil2gil_bispec : Jsil_syntax.BiSpec.t -> GBiSpec.t
val jsil2core : string option -> Jsil_syntax.LabCmd.t -> (string option * string GCmd.t) list
val jsil2core_proc : Jsil_syntax.EProc.t -> (Jsil_syntax.EProc.Annot.t, string) GProc.t
val translate_tbl : (string, 'a) Stdlib.Hashtbl.t -> ('a -> 'b) -> (string, 'b) Stdlib.Hashtbl.t
val jsil2core_prog : Jsil_syntax.EProg.t -> (Annot.Basic.t, string) GProg.t