type constant =
  Output.constant =
    Prim_void
  | Prim_int of string
  | Prim_real of string
  | Prim_bool of bool
type logic_type =
  Output.logic_type = {
  logic_type_name : string;
  logic_type_args : logic_type list;
}
val fprintf_logic_type : Format.formatter -> logic_type -> unit
type term =
  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 =
  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 =
  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 =
  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 =
  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 =
  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