JS2JSIL_Helpers (gillian-js.Js2jsil_lib.JS2JSIL

val small_tbl_size : int

val medium_tbl_size : int

val line_numbers_extension : string

type js_symbolic_constructs_type = {

js_assume : string;
js_assert : string;
js_symb : string;
js_symb_number : string;
js_symb_string : string;
js_symb_bool : string;

}

val js_symbolic_constructs : js_symbolic_constructs_type

val js2jsil_imports : string list

val js2jsil_imports_cosette : string list

val js2jsil_logic_imports : string list

val js2jsil_imports_bi : string list

val reserved_biannots : string list

val setupHeapName : string

val _callPropName : string

val _constructPropName : string

val _scopePropName : string

val _classPropName : string

val _extensiblePropName : string

val _internalProtoFieldName : string

val _erFlagPropName : string

val locGlobName : string

val locObjPrototype : string

val locFunObjPrototype : string

val locArrPrototype : string

val locTErrPrototype : string

val locSErrPrototype : string

val locRErrPrototype : string

val locErrPrototype : string

val toBooleanName : string

val getValueName : string

val isReservedName : string

val putValueName : string

val createDefaultObjectName : string

val toObjectName : string

val toStringName : string

val toStringComputedName : string

val deletePropertyName : string

val syntaxErrorName : string

val typeErrorName : string

val referenceErrorName : string

val createFunctionObjectName : string

val isCallableName : string

val checkObjectCoercibleName : string

val jsTypeOfName : string

val toNumberName : string

val toPrimitiveName : string

val toInt32Name : string

val toUInt32Name : string

val abstractComparisonName : string

val hasPropertyName : string

val abstractEqualityComparisonName : string

val strictEqualityComparisonName : string

val defineOwnPropertyName : string

val checkAssignmentErrorsName : string

val checkParametersName : string

val getEnumFieldsName : string

val createArgsName : string

val dynamicScoper : string

val isNativeErrorName : string

val deleteObjAndMetadata : string

val deleteErrorObjects : string

val var_this : string

val var_scope : string

val var_scope_final : string

val var_se : string

val var_te : string

val var_re : string

val var_args : string

val var_er : string

val var_er_metadata : string

val var_sc_first : string

val js2jsil_spec_vars : string list

val reserved_vars : string list

val main_fid : string

val macro_GPVF_name : string

val macro_GPVU_name : string

val pi_predicate_name : string

val lit_num : float -> Gillian.Gil_syntax.Expr.t

Various abbreviations

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

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

val lit_typ : Gillian.Gil_syntax.Type.t -> Gillian.Gil_syntax.Expr.t

val lit_refv : Gillian.Gil_syntax.Expr.t

val lit_refo : Gillian.Gil_syntax.Expr.t

val rtype : Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t

val base : Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t

val field : Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t

val fresh_sth : string -> (unit -> string) * (unit -> unit)

* Fresh identifiers

val fresh_var : unit -> string

val reset_var : unit -> unit

val fresh_scope_chain_var : unit -> string

val reset_scope_chain_var : unit -> unit

val fresh_found_var : unit -> string

val reset_found_var : unit -> unit

val fresh_fun_var : unit -> string

val reset_fun_var : unit -> unit

val fresh_obj_var : unit -> string

val reset_obj_var : unit -> unit

val fresh_er_var : unit -> string

val reset_er_var : unit -> unit

val fresh_err_var : unit -> string

val reset_err_var : unit -> unit

val fresh_this_var : unit -> string

val reset_this_var : unit -> unit

val fresh_case_var : unit -> string

val reset_case_var : unit -> unit

val fresh_desc_var : unit -> string

val reset_desc_var : unit -> unit

val fresh_body_var : unit -> string

val reset_body_var : unit -> unit

val fresh_fscope_var : unit -> string

val reset_fscope_var : unit -> unit

val fresh_xfoundb_var : unit -> string

val reset_xfoundb_var : unit -> unit

val fresh_label : unit -> string

val reset_label : unit -> unit

val fresh_next_label : unit -> string

val reset_next_label : unit -> unit

val fresh_then_label : unit -> string

val reset_then_label : unit -> unit

val fresh_else_label : unit -> string

val reset_else_label : unit -> unit

val fresh_endif_label : unit -> string

val reset_endif_label : unit -> unit

val fresh_end_label : unit -> string

val reset_end_label : unit -> unit

val fresh_end_switch_label : unit -> string

val reset_end_switch_label : unit -> unit

val fresh_end_case_label : unit -> string

val reset_end_case_label : unit -> unit

val fresh_default_label : unit -> string

val reset_default_label : unit -> unit

val fresh_b_cases_label : unit -> string

val reset_b_cases_label : unit -> unit

val fresh_logical_variable : unit -> string

val reset_logical_variable : unit -> unit

val fresh_break_label : unit -> string

val reset_break_label : unit -> unit

val fresh_loop_head_label : unit -> string

val reset_loop_head_label : unit -> unit

val fresh_loop_cont_label : unit -> string

val reset_loop_cont_label : unit -> unit

val fresh_loop_guard_label : unit -> string

val reset_loop_guard_label : unit -> unit

val fresh_loop_body_label : unit -> string

val reset_loop_body_label : unit -> unit

val fresh_loop_end_label : unit -> string

val reset_loop_end_label : unit -> unit

val fresh_loop_identifier : unit -> string

val reset_loop_identifier : unit -> unit

val fresh_tcf_finally_label : unit -> string

val reset_tcf_finally_label : unit -> unit

val fresh_tcf_end_label : unit -> string

val reset_tcf_end_label : unit -> unit

val fresh_tcf_err_try_label : unit -> string

val reset_tcf_err_try_label : unit -> unit

val fresh_tcf_err_catch_label : unit -> string

val reset_tcf_err_catch_label : unit -> unit

val fresh_tcf_ret : unit -> string

val reset_tcf_ret : unit -> unit

val fresh_loop_vars : unit -> string * string * string * string * string

val number_of_tcfs : int Stdlib.ref

val fresh_tcf_vars : 
  unit ->
  string * string * string * string * (unit -> string) * string

val fresh_name : string -> string

val fresh_anonymous : unit -> string

val fresh_catch_anonymous : unit -> string

val fresh_named : string -> string

val fresh_anonymous_eval : unit -> string

val fresh_catch_anonymous_eval : unit -> string

val fresh_named_eval : string -> string

val is_get_value_var : Gillian.Gil_syntax.Expr.t -> string option

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

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

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

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

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

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

val fresh_err_label : unit -> string

val reset_err_label : unit -> unit

val fresh_ret_label : unit -> string

val reset_ret_label : unit -> unit

type loop_list_type = (string option * string * string option * bool) list

type translation_context = {

tr_fid : string;
tr_er_fid : string;
tr_sc_var : string;
tr_vis_list : string list;
tr_loop_list : loop_list_type;
tr_loops : string list;
tr_previous : Gillian.Gil_syntax.Expr.t option;
tr_js_lab : string option;
tr_ret_lab : string;
tr_err_lab : string;
tr_use_cc : bool;
tr_strictness : bool;

}

val make_translation_ctx : 
  ?loop_list:loop_list_type ->
  ?loops:string list ->
  ?previous:Gillian.Gil_syntax.Expr.t option ->
  ?js_lab:string option ->
  string ->
  string list ->
  string ->
  bool ->
  translation_context

val update_tr_ctx : 
  ?ret_lab:string ->
  ?err:string ->
  ?loop_list:loop_list_type ->
  ?loops:string list ->
  ?previous:Gillian.Gil_syntax.Expr.t option ->
  ?lab:string option ->
  ?vis_list:string list ->
  ?er_fid:string ->
  ?sc_var:string ->
  ?use_cc:bool ->
  ?strictness:bool ->
  translation_context ->
  translation_context

val reset_generators : unit -> unit