JS2JSIL_Preprocessing (gillian-js.Js2jsil_lib.JS2JSIL

module Flag = Gillian.Gil_syntax.Flag

exception CannotHappen

exception No_Codename

exception EarlyError of string

val string_of_vtf_tbl : Jslogic.JSLogicCommon.var_to_fid_tbl_type -> string

val string_of_cc_tbl : Jslogic.JSLogicCommon.cc_tbl_type -> string

val update_fun_tbl : 
  Jslogic.JSLogicCommon.pre_fun_tbl_type ->
  string ->
  string list ->
  JS_Parser.Syntax.exp option ->
  bool ->
  JS_Parser.Syntax.annotation list ->
  Jslogic.JSLogicCommon.var_to_fid_tbl_type ->
  string list ->
  unit

val update_cc_tbl : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  string ->
  string ->
  string list ->
  (string, string) Stdlib.Hashtbl.t

val update_cc_tbl_single_var_er : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  string ->
  string ->
  string ->
  (string, string) Stdlib.Hashtbl.t

val get_vis_list_index : 'a list -> 'a -> int

val update_annotation : 
  JS_Parser.Syntax.annotation list ->
  JS_Parser.Syntax.annotation_type ->
  string ->
  JS_Parser.Syntax.annotation list

val is_logic_cmd_annot : JS_Parser.Syntax.annotation -> bool

val is_spec_annot : JS_Parser.Syntax.annotation -> bool

val get_top_level_annot : 
  JS_Parser.Syntax.exp ->
  JS_Parser.Syntax.annotation list

val sanitise : string -> string

val update_codename_annotation : 
  JS_Parser.Syntax.annotation list ->
  (unit -> string) ->
  JS_Parser.Syntax.annotation list * string

val get_codename : JS_Parser.Syntax.exp -> string

val add_codenames : JS_Parser.Syntax.exp -> JS_Parser.Syntax.exp * string list

val closure_clarification : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.pre_fun_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  string ->
  string list ->
  JS_Parser.Syntax.exp ->
  'a list

val propagate_annotations : 
  JS_Parser.Syntax.exp ->
  JS_Parser.Syntax.exp * (bool * JS_Parser.Syntax.annotation list)

val test_expr_eval_arguments_assignment : JS_Parser.Syntax.exp -> bool

val test_early_errors : bool -> JS_Parser.Syntax.exp -> unit

val get_predicate_defs_from_annots : 
  JS_Parser.Syntax.annotation list ->
  Jslogic.JSPred.t list

val get_only_specs_from_annots : 
  JS_Parser.Syntax.annotation list ->
  Jslogic.JSSpec.t list

val parse_annots_formulae : 
  JS_Parser.Syntax.annotation list ->
  Jslogic.JSLCmd.t list

val translate_lannots_in_exp : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  Jslogic.JSLogicCommon.pre_fun_tbl_type ->
  string ->
  string ->
  bool ->
  JS_Parser.Syntax.exp ->
  Jsil_syntax.LCmd.t list
  * Jsil_syntax.LCmd.t list
  * (string * (string * Gillian.Gil_syntax.Expr.t) list) option

val translate_invariant_in_exp : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  Jslogic.JSLogicCommon.pre_fun_tbl_type ->
  string ->
  string ->
  JS_Parser.Syntax.exp ->
  (Jsil_syntax.Asrt.t * string list) option

val translate_single_func_specs : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  Jslogic.JSLogicCommon.pre_fun_tbl_type ->
  string ->
  string list ->
  JS_Parser.Syntax.annotation list ->
  JS_Parser.Syntax.annotation_type ->
  JS_Parser.Syntax.annotation_type ->
  JS_Parser.Syntax.annotation_type ->
  Jsil_syntax.Spec.t option

val translate_specs : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  Jslogic.JSLogicCommon.pre_fun_tbl_type ->
  Jslogic.JSLogicCommon.fun_tbl_type ->
  unit

* Populates the new fun_tbl given the old fun_tbl * by compiling the specs in the old fun_tbl

val get_predicate_definitions : JS_Parser.Syntax.exp -> Jslogic.JSPred.t list

val translate_only_specs : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  (string,
    string
    * string list
    * 'a option
    * bool
    * ('b list * string list * ('c, 'd) Stdlib.Hashtbl.t))
    Stdlib.Hashtbl.t ->
  (string, string * string list * 'e option * bool * Jsil_syntax.Spec.t option)
    Stdlib.Hashtbl.t ->
  (string, string list) Stdlib.Hashtbl.t ->
  Jslogic.JSSpec.t list ->
  (string, Jsil_syntax.Spec.t) Stdlib.Hashtbl.t

val get_imports : JS_Parser.Syntax.annotation list -> (string * bool) list

val preprocess : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.fun_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  JS_Parser.Syntax.exp ->
  JS_Parser.Syntax.exp
  * (string, Jsil_syntax.Spec.t) Stdlib.Hashtbl.t
  * (string, Jsil_syntax.Pred.t) Stdlib.Hashtbl.t
  * string list
  * (string * bool) list

val get_them_functions : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.pre_fun_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  string ->
  string list ->
  JS_Parser.Syntax.exp ->
  'a list

val preprocess_eval : 
  Jslogic.JSLogicCommon.cc_tbl_type ->
  Jslogic.JSLogicCommon.vis_tbl_type ->
  bool ->
  JS_Parser.Syntax.exp ->
  string ->
  string list ->
  JS_Parser.Syntax.exp
  * string
  * string list
  * (string,
      string
      * string list
      * JS_Parser.Syntax.exp option
      * bool
      * Jsil_syntax.Spec.t option)
      Stdlib.Hashtbl.t