val ( $ ) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
val error : Loc.position -> ('a, Format.formatter, unit, 'b) format4 -> 'a
val label_var :
  ?label_in_name:bool ->
  ?label_assoc:(Jc_env.logic_label * Jc_env.logic_label) list ->
  Jc_env.logic_label -> string -> string
val new_label_name : unit -> string
val operator_of_native :
  Jc_env.native_type -> [> Jc_ast.native_operator_type ]
val operator_of_type : Jc_env.jc_type -> [> Jc_ast.operator_type ]
val integer_type : Jc_env.jc_type
val boolean_type : Jc_env.jc_type
val real_type : Jc_env.jc_type
val unit_type : Jc_env.jc_type
val string_type : Jc_env.jc_type
val any_type : Jc_env.jc_type
val string_of_native : Jc_env.native_type -> string
val print_type : Format.formatter -> Jc_env.jc_type -> unit
val struct_of_union : Jc_env.struct_info -> bool
val field_of_union : Jc_env.field_info -> bool
val union_of_field : Jc_env.field_info -> Jc_env.variant_info
val integral_union : Jc_env.variant_info -> bool
val zero : Num.num
val num_of_constant : 'a -> Jc_ast.const -> Num.num
val const : Jc_ast.const -> Jc_env.jc_type * Jc_env.region * Jc_ast.const
val var :
  ?unique:bool ->
  ?static:bool -> ?formal:bool -> Jc_env.jc_type -> string -> Jc_env.var_info
val copyvar : Jc_env.var_info -> Jc_env.var_info
val tmp_var_name : unit -> string
val newvar : Jc_env.jc_type -> Jc_env.var_info
val newrefvar : Jc_env.jc_type -> Jc_env.var_info
val exception_info : Jc_env.jc_type option -> string -> Jc_env.exception_info
val make_fun_info : string -> Jc_env.jc_type -> Jc_fenv.fun_info
val make_rel : string -> Jc_fenv.logic_info
val make_logic_fun : string -> Jc_env.jc_type -> Jc_fenv.logic_info
val location_set_region : Jc_ast.tlocation_set -> Jc_env.region
val field_sinfo : Jc_env.field_info -> Jc_env.struct_info
val field_bounds : Jc_env.field_info -> Num.num * Num.num
val root_name : Jc_env.struct_info -> string
val field_root_name : Jc_env.field_info -> string
val struct_variant : Jc_env.struct_info -> Jc_env.variant_info
val tag_or_variant_variant : Jc_env.tag_or_variant -> Jc_env.variant_info
val tag_or_variant_name : Jc_env.tag_or_variant -> string
val true_assertion : Jc_ast.assertion
val any_string : Jc_fenv.logic_info
val real_of_integer : Jc_fenv.logic_info
val real_of_integer_ : Jc_fenv.fun_info
val full_separated : Jc_fenv.logic_info
val default_behavior : Jc_ast.behavior
val empty_fun_effect : Jc_fenv.fun_effect
val empty_effects : Jc_fenv.effect
val raw_term_equal : Jc_ast.term -> Jc_ast.term -> bool
val raw_term_compare : Jc_ast.term -> Jc_ast.term -> int
val raw_assertion_equal : Jc_ast.assertion -> Jc_ast.assertion -> bool
val make_and : Jc_ast.assertion list -> Jc_ast.assertion
val skip_term_shifts : Jc_ast.term -> Jc_ast.term
val skip_shifts : Jc_ast.expr -> Jc_ast.expr
val skip_tloc_range : Jc_ast.tlocation_set -> Jc_ast.tlocation_set
val is_true : Jc_ast.assertion -> bool
val select_option : 'a option -> 'a -> 'a
val apply_option : ('a -> 'b) -> 'a option -> 'b option
val is_constant_assertion : Jc_ast.assertion -> bool
val contains_normal_behavior : Jc_ast.fun_spec -> bool
val contains_exceptional_behavior : Jc_ast.fun_spec -> bool
val is_purely_exceptional_fun : Jc_ast.fun_spec -> bool
val pattern_vars :
  Jc_env.var_info Jc_envset.StringMap.t ->
  Jc_ast.pattern -> Jc_env.var_info Jc_envset.StringMap.t
val string_of_op :
  [< `Badd
   | `Barith_shift_right
   | `Bbw_and
   | `Bbw_or
   | `Bbw_xor
   | `Bconcat
   | `Bdiv
   | `Beq
   | `Bge
   | `Bgt
   | `Biff
   | `Bimplies
   | `Bland
   | `Ble
   | `Blogical_shift_right
   | `Blor
   | `Blt
   | `Bmod
   | `Bmul
   | `Bneq
   | `Bshift_left
   | `Bsub
   | `Ubw_not
   | `Uminus
   | `Unot ] ->
  string
val string_of_op_type : [< Jc_ast.operator_type ] -> string
val builtin_logic_symbols :
  (Jc_env.jc_type option * string * string * Jc_env.jc_type list) list