module Lib :
  sig
    module Sset :
      sig
        type elt = string
        type t = Jc.Lib.Sset.t
        val empty : t
        val is_empty : t -> bool
        val mem : elt -> t -> bool
        val add : elt -> t -> t
        val singleton : elt -> t
        val remove : elt -> t -> t
        val union : t -> t -> t
        val inter : t -> t -> t
        val diff : t -> t -> t
        val compare : t -> t -> int
        val equal : t -> t -> bool
        val subset : t -> t -> bool
        val iter : (elt -> unit) -> t -> unit
        val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
        val for_all : (elt -> bool) -> t -> bool
        val exists : (elt -> bool) -> t -> bool
        val filter : (elt -> bool) -> t -> t
        val partition : (elt -> bool) -> t -> t * t
        val cardinal : t -> int
        val elements : t -> elt list
        val min_elt : t -> elt
        val max_elt : t -> elt
        val choose : t -> elt
        val split : elt -> t -> t * bool * t
      end
    val mkdir_p : string -> unit
    val file : dir:string -> file:string -> string
    val file_subdir : dir:string -> file:string -> string
    val file_copy_if_different : string -> string -> unit
  end
module Rc :
  sig
    type rc_value =
      Jc.Rc.rc_value =
        RCint of int
      | RCbool of bool
      | RCfloat of float
      | RCstring of string
      | RCident of string
      | RCkind of Output.kind
    val from_file : string -> (string * (string * rc_value) list) list
  end
module Loc :
  sig
    val report_line : Format.formatter -> Lexing.position -> unit
    type position = Lexing.position * Lexing.position
    exception Located of position * exn
    val string : position -> string
    val parse : string -> position
    val dummy_position : position
    type floc = string * int * int * int
    val dummy_floc : floc
    val extract : position -> floc
    val gen_report_line : Format.formatter -> floc -> unit
    val gen_report_position : Format.formatter -> position -> unit
    val report_position : Format.formatter -> position -> unit
    val report_obligation_position : Format.formatter -> floc -> unit
    val join : 'a * 'b -> 'a * 'b -> 'a * 'b
    val current_offset : int ref
    val reloc : Lexing.position -> Lexing.position
    val add_ident : string -> floc -> unit
    val ident : string -> floc
  end
module Pp :
  sig
    val print_option :
      (Format.formatter -> 'a -> unit) ->
      Format.formatter -> 'a option -> unit
    val print_option_or_default :
      string ->
      (Format.formatter -> 'a -> unit) ->
      Format.formatter -> 'a option -> unit
    val print_list :
      (Format.formatter -> unit -> unit) ->
      (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
    val print_list_or_default :
      string ->
      (Format.formatter -> unit -> unit) ->
      (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
    val print_list_par :
      (Format.formatter -> unit -> 'a) ->
      (Format.formatter -> 'b -> unit) -> Format.formatter -> 'b list -> unit
    val print_list_delim :
      (Format.formatter -> unit -> unit) ->
      (Format.formatter -> unit -> unit) ->
      (Format.formatter -> unit -> unit) ->
      (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
    val space : Format.formatter -> unit -> unit
    val alt : Format.formatter -> unit -> unit
    val newline : Format.formatter -> unit -> unit
    val comma : Format.formatter -> unit -> unit
    val semi : Format.formatter -> unit -> unit
    val underscore : Format.formatter -> unit -> unit
    val arrow : Format.formatter -> unit -> unit
    val lbrace : Format.formatter -> unit -> unit
    val rbrace : Format.formatter -> unit -> unit
    val nothing : Format.formatter -> unit -> unit
    val string : Format.formatter -> string -> unit
    val constant_string : string -> Format.formatter -> unit -> unit
    val hov : int -> Format.formatter -> ('a -> unit) -> 'a -> unit
    val open_formatter : ?margin:int -> out_channel -> Format.formatter
    val close_formatter : Format.formatter -> unit
    val open_file_and_formatter :
      ?margin:int -> string -> out_channel * Format.formatter
    val close_file_and_formatter : out_channel * Format.formatter -> unit
    val print_in_file_no_close :
      ?margin:int -> (Format.formatter -> unit) -> string -> out_channel
    val print_in_file :
      ?margin:int -> (Format.formatter -> unit) -> string -> unit
  end
module Option_misc :
  sig
    val map : ('a -> 'b) -> 'a option -> 'b option
    val iter : ('a -> unit) -> 'a option -> unit
    val fold : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
    val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b option -> 'a
  end
module Jc_type_var :
  sig
    type t = Jc.Jc_type_var.t
    val fresh : string -> t
    val find : t -> t list -> 'a list -> 'a
    val uid : t -> int
    val name : t -> string
    val uname : t -> string
  end
module Output :
  sig
    type constant =
      Jc.Output.constant =
        Prim_void
      | Prim_int of string
      | Prim_real of string
      | Prim_bool of bool
    type logic_type =
      Jc.Output.logic_type = {
      logic_type_name : string;
      logic_type_args : logic_type list;
    }
    val fprintf_logic_type : Format.formatter -> logic_type -> unit
    type term =
      Jc.Output.term =
        LConst of constant
      | LApp of string * term list
      | LVar of string
      | LVarAtLabel of string * string
      | Tnamed of string * term
      | TIf of term * term * term
    val fprintf_term : Format.formatter -> term -> unit
    type assertion =
      Jc.Output.assertion =
        LTrue
      | LFalse
      | LAnd of assertion * assertion
      | LOr of assertion * assertion
      | LIff of assertion * assertion
      | LNot of assertion
      | LImpl of assertion * assertion
      | LIf of term * assertion * assertion
      | LLet of string * term * assertion
      | LForall of string * logic_type * assertion
      | LExists of string * logic_type * assertion
      | LPred of string * term list
      | LNamed of string * assertion
    val make_or : assertion -> assertion -> assertion
    val make_and : assertion -> assertion -> assertion
    val make_or_list : assertion list -> assertion
    val make_and_list : assertion list -> assertion
    val make_impl : assertion -> assertion -> assertion
    val make_equiv : assertion -> assertion -> assertion
    val fprintf_assertion : Format.formatter -> assertion -> unit
    type why_type =
      Jc.Output.why_type =
        Prod_type of string * why_type * why_type
      | Base_type of logic_type
      | Ref_type of why_type
      | Annot_type of assertion * why_type * string list * string list *
          assertion * (string * assertion) list
    val int_type : why_type
    val bool_type : why_type
    val unit_type : why_type
    val base_type : string -> why_type
    type variant = term * string option
    type opaque = bool
    type expr =
      Jc.Output.expr =
        Cte of constant
      | Var of string
      | And of expr * expr
      | Or of expr * expr
      | Not of expr
      | Void
      | Deref of string
      | If of expr * expr * expr
      | While of expr * assertion * variant option * expr list
      | Block of expr list
      | Assign of string * expr
      | Let of string * expr * expr
      | Let_ref of string * expr * expr
      | App of expr * expr
      | Raise of string * expr option
      | Try of expr * string * string option * expr
      | Fun of (string * why_type) list * assertion * expr * assertion *
          (string * assertion) list
      | Triple of opaque * assertion * expr * assertion *
          (string * assertion) list
      | Assert of assertion * expr
      | Label of string * expr
      | BlackBox of why_type
      | Absurd
      | Loc of Lexing.position * expr
    val fprintf_expr : Format.formatter -> expr -> unit
    val make_or_expr : expr -> expr -> expr
    val make_and_expr : expr -> expr -> expr
    val make_app : string -> expr list -> expr
    val make_app_e : expr -> expr list -> expr
    val make_label : string -> expr -> expr
    val make_while : expr -> assertion -> variant option -> expr -> expr
    val make_pre : assertion -> expr -> expr
    val append : expr -> expr -> expr
    type why_decl =
      Jc.Output.why_decl =
        Param of bool * string * why_type
      | Def of string * expr
      | Logic of bool * string * (string * logic_type) list * logic_type
      | Axiom of string * assertion
      | Goal of string * assertion
      | Predicate of bool * string * (string * logic_type) list * assertion
      | Function of bool * string * (string * logic_type) list * logic_type *
          term
      | Type of string * string list
      | Exception of string * logic_type option
    val fprintf_why_decl : Format.formatter -> why_decl -> unit
    val fprintf_why_decls : Format.formatter -> why_decl list -> unit
    type kind =
      Jc.Output.kind =
        ArithOverflow
      | DownCast
      | IndexBounds
      | PointerDeref
      | UserCall
      | DivByZero
      | AllocSize
      | Pack
      | Unpack
    val locs_table :
      (string, kind option * string option * string option * Loc.position)
      Hashtbl.t
    val reg_loc :
      string ->
      ?id:string ->
      ?kind:kind -> ?name:string -> ?formula:string -> Loc.position -> string
    val print_locs : Format.formatter -> unit
  end
module Jc_version :
  sig val version : string val date : string val libdir : string end
module Jc_common_options :
  sig
    val debug : bool ref
    val verbose : bool ref
    val werror : bool ref
    val inv_sem : Jc_env.inv_sem