Module Js2jsil_lib.JS2JSIL_Compiler

module Preprocess_GCmd : sig ... end
module SSubst = Gillian.Symbolic.Subst
val if_verification : 'a -> 'a -> 'a
val print_position : Stdlib.out_channel -> Stdlib.Lexing.lexbuf -> unit
val power_list : 'a list -> int -> 'a list
val number_of_switches : int Stdlib.ref
val fresh_switch_labels : unit -> string * string * string * (unit -> string)
val add_initial_label : ('a * 'b option * Jsil_syntax.LabCmd.t) list -> 'b -> 'a -> ('a * 'b option * Jsil_syntax.LabCmd.t) list
val prefix_lcmds : Jsil_syntax.LCmd.t list -> (Jsil_syntax.Asrt.t * string list) option -> (Gillian.Gil_syntax.Annot.Basic.t * string option * Jsil_syntax.LabCmd.t) list -> (Gillian.Gil_syntax.Annot.Basic.t * string option * Jsil_syntax.LabCmd.t) list
val get_break_lab : ('a * 'b * string option * bool) list -> string option -> 'b
val get_continue_lab : ('a option * 'b * string option * bool) list -> string option -> 'a
val filter_cur_jumps : (string option * string * string) list -> string option -> bool -> string list * (string option * string * string) list
val add_none_labs : 'a list -> ('b option * 'a) list
val add_skip_if_empty : ('a * 'b option * Jsil_syntax.LabCmd.t) list -> Gillian.Gil_syntax.Expr.t -> 'a -> ('a * 'b option * Jsil_syntax.LabCmd.t) list * Gillian.Gil_syntax.Expr.t
val make_var_ass_se : unit -> Jsil_syntax.LabCmd.t
val make_var_ass_te : unit -> Jsil_syntax.LabCmd.t
val make_var_ass_re : unit -> Jsil_syntax.LabCmd.t
val add_final_var : ('a * 'b option * Jsil_syntax.LabCmd.t) list -> Gillian.Gil_syntax.Expr.t -> 'a -> ('a * 'b option * Jsil_syntax.LabCmd.t) list * string
val make_unresolvable_ref_test : Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t
val make_get_value_call : Jsil_syntax.LabCmd.Expr.t -> string -> string * Jsil_syntax.LabCmd.t * string list
val make_to_number_call : Gillian.Gil_syntax.Expr.t -> string -> string -> string * Jsil_syntax.LabCmd.t
val make_to_boolean_call : Gillian.Gil_syntax.Expr.t -> string -> string -> string * Jsil_syntax.LabCmd.t
val make_to_primitive_call : Gillian.Gil_syntax.Expr.t -> string -> string -> string * Jsil_syntax.LabCmd.t
val make_to_string_call : Gillian.Gil_syntax.Expr.t -> string -> string -> string * Jsil_syntax.LabCmd.t
val make_to_string_computed_call : Gillian.Gil_syntax.Expr.t -> string -> string -> string * Jsil_syntax.LabCmd.t
val make_to_i32_call : Gillian.Gil_syntax.Expr.t -> string -> string -> string * Jsil_syntax.LabCmd.t
val make_put_value_call : Jsil_syntax.LabCmd.Expr.t -> string -> string -> string * Jsil_syntax.LabCmd.t
val make_dop_call : string -> Jsil_syntax.LabCmd.Expr.t -> string -> bool -> string -> string * Jsil_syntax.LabCmd.t
val make_cae_call : Jsil_syntax.LabCmd.Expr.t -> string -> string * Jsil_syntax.LabCmd.t
val make_empty_ass : unit -> string * Jsil_syntax.LabCmd.t
val make_create_function_object_call : string -> string -> string list -> string * Jsil_syntax.LabCmd.t
val translate_named_function_literal : bool -> string -> string -> string -> string list -> int -> ('a option * Jsil_syntax.LabCmd.t) list * Gillian.Gil_syntax.Expr.t * 'b list
val translate_inc_dec : Jsil_syntax.LabCmd.Expr.t -> bool -> string -> (string option * Jsil_syntax.LabCmd.t) list * string list * string * string
val translate_multiplicative_binop : Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> string -> string -> JS_Parser.Syntax.arith_op -> string -> ('a option * Jsil_syntax.LabCmd.t) list * string list * string
val translate_binop_plus : Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> string -> string -> string -> (string option * Jsil_syntax.LabCmd.t) list * string list * string
val translate_binop_comparison : 'a -> 'b -> string -> string -> bool -> bool -> bool -> string -> (string option * Jsil_syntax.LabCmd.t) list * string list * string
val translate_bitwise_shift : 'a -> 'b -> string -> string -> string -> string -> Gillian.Gil_syntax.BinOp.t -> string -> ('c option * Jsil_syntax.LabCmd.t) list * string list * string
val translate_binop_equality : 'a -> 'b -> string -> string -> bool -> bool -> string -> ('c option * Jsil_syntax.LabCmd.t) list * string list * string
val translate_bitwise_bin_op : Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> string -> string -> JS_Parser.Syntax.arith_op -> string -> ('a option * Jsil_syntax.LabCmd.t) list * string list * string
val make_check_empty_test : Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> (string option * Jsil_syntax.LabCmd.t) list * string
val make_loop_end : string -> string -> string list -> string -> bool -> (string option * Jsil_syntax.LabCmd.t) list * string
val is_get_value_call : Jsil_syntax.LabCmd.t -> bool
val is_put_value_call : Jsil_syntax.LabCmd.t -> bool
val is_hasProperty_call : Jsil_syntax.LabCmd.t -> bool
val get_args : Jsil_syntax.LabCmd.t -> Jsil_syntax.LabCmd.Expr.t list option
val annotate_cmd_top_level : 'a -> ('b * Jsil_syntax.LabCmd.t) -> 'a * 'b * Jsil_syntax.LabCmd.t
val annotate_cmds_top_level : 'a -> ('b * Jsil_syntax.LabCmd.t) list -> ('a * 'b * Jsil_syntax.LabCmd.t) list
val translate_statement : JS2JSIL_Helpers.translation_context -> JS_Parser.Syntax.exp -> (Gillian.Gil_syntax.Annot.Basic.t * string option * Jsil_syntax.LabCmd.t) list * Jsil_syntax.LabCmd.Expr.t * string list * string list * (string option * string * string) list * (string option * string * string) list
val make_final_cmd : string list -> 'a -> string -> Gillian.Gil_syntax.Location.t -> Gillian.Gil_syntax.Annot.Basic.t * 'a option * Jsil_syntax.LabCmd.t
val translate_fun_decls : bool -> string -> int -> JS_Parser.Syntax.exp -> ('a option * Jsil_syntax.LabCmd.t) list
val generate_main : JS_Parser.Syntax.exp -> bool -> Jsil_syntax.Spec.t option -> Jsil_syntax.EProc.t
val generate_proc_eval : string -> ?use_cc:bool -> JS_Parser.Syntax.exp -> bool -> string list -> Jsil_syntax.EProc.t
val generate_proc : ?use_cc:bool -> JS_Parser.Syntax.exp -> string -> string list -> bool -> string list -> Jsil_syntax.Spec.t option -> Jsil_syntax.EProc.t
val js2jsil_eval : (Jsil_syntax.EProc.Annot.t, int) Gillian.Gil_syntax.Prog.t -> string -> bool -> JS_Parser.Syntax.exp -> string
val js2jsil_function_constructor_prop : (Jsil_syntax.EProc.Annot.t, int) GProg.t -> 'a -> string list -> bool -> JS_Parser.Syntax.exp -> (Jsil_syntax.EProc.Annot.t, int) Gillian.Gil_syntax.Proc.t
val compute_imports : bool -> string list