JSIL_PostParser (gillian-js.Js2jsil_lib.JSIL

val heap_asrt_name : string

val pre_scope_prefix : string

val post_scope_prefix : string

val reserved_methods : (string, string) Stdlib.Hashtbl.t

val reserved_properties : (string, string * string * string) Stdlib.Hashtbl.t

val counter : int Stdlib.ref

val pvar_counter : int Stdlib.ref

val fresh_bi_lvar : unit -> string

val populate : unit -> unit

val post_parse_lcmd : 
  (Gillian.Gil_syntax.Annot.Basic.t * string option * Jsil_syntax.LabCmd.t) ->
  (Gillian.Gil_syntax.Annot.Basic.t * string option * Jsil_syntax.LabCmd.t)
    list

val post_parse_eproc : Jsil_syntax.EProc.t -> Jsil_syntax.EProc.t

val post_parse_eprog : Jsil_syntax.EProg.t -> Jsil_syntax.EProg.t

val expr_from_fid : string -> Gillian.Gil_syntax.Expr.t

val make_sc : string list -> Gillian.Gil_syntax.Expr.t list

val asrts_js_val : Gillian.Gil_syntax.Expr.t -> Jsil_syntax.Asrt.t list

val var_assertion : 
  string ->
  string ->
  Gillian.Gil_syntax.Expr.t ->
  Jsil_syntax.Asrt.t

val make_this_assertion : unit -> Jsil_syntax.Asrt.t

val scope_info_to_assertion : 
  Jsil_syntax.EProg.t ->
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  string ->
  Gillian.Utils.Containers.SS.t ->
  Jsil_syntax.Asrt.t

val create_pre_scope_pred : 
  Jsil_syntax.EProg.t ->
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  string ->
  Gillian.Utils.Containers.SS.t ->
  Jsil_syntax.Pred.t

val create_function_predicate : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  string ->
  string list ->
  Jsil_syntax.Pred.t

val create_post_scope_pred : 
  Jsil_syntax.EProg.t ->
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  string ->
  Gillian.Utils.Containers.SS.t ->
  Jsil_syntax.Pred.t

val bi_post_parse_cmd : 
  (Gillian.Gil_syntax.Annot.Basic.t * string option * Jsil_syntax.LabCmd.t) ->
  (Gillian.Gil_syntax.Annot.Basic.t * string option * Jsil_syntax.LabCmd.t)
    list

val bi_post_parse_eproc : 
  Jsil_syntax.EProg.t ->
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  Jsil_syntax.EProc.t ->
  Jsil_syntax.EProc.t

val create_new_bispec : 
  Jsil_syntax.EProg.t ->
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  Jsil_syntax.EProc.t ->
  unit

val bi_post_parse_eprog : 
  Jsil_syntax.EProg.t ->
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  Jsil_syntax.EProg.t