type jc_decl =
  Jc_output.jc_decl =
    JCfun_def of Jc_env.jc_type * string * Jc_env.var_info list *
      Jc_ast.fun_spec * Jc_ast.expr option
  | JCenum_type_def of string * Num.num * Num.num
  | JCvariant_type_def of string * string list
  | JCunion_type_def of string * string list
  | JCstruct_def of string * string option * Jc_env.field_info list *
      (string * Jc_env.var_info * Jc_ast.assertion) list
  | JCrec_struct_defs of jc_decl list
  | JCrec_fun_defs of jc_decl list
  | JCvar_def of Jc_env.jc_type * string * Jc_ast.expr option
  | JClemma_def of string * bool * Jc_env.logic_label list * Jc_ast.assertion
  | JClogic_fun_def of Jc_env.jc_type option * string *
      Jc_env.logic_label list * Jc_env.var_info list *
      Jc_ast.term_or_assertion
  | JCexception_def of string * Jc_env.exception_info
  | JCglobinv_def of string * Jc_ast.assertion
  | JClogic_const_def of Jc_env.jc_type * string * Jc_ast.term option
  | JClogic_type_def of string
  | JCinvariant_policy of Jc_env.inv_sem
  | JCseparation_policy of Jc_env.separation_sem
  | JCannotation_policy of Jc_env.annotation_sem
  | JCabstract_domain of Jc_env.abstract_domain
  | JCint_model of Jc_env.int_model
val bin_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 ] *
  'a -> string
val unary_op : [< `Ubw_not | `Uminus | `Unot ] * 'a -> string
val real_conversion : Format.formatter -> Jc_ast.real_conversion -> unit
val pattern : Format.formatter -> Jc_ast.pattern -> unit
val term : Format.formatter -> Jc_constructors.term_with -> unit
val quantifier : Format.formatter -> Jc_ast.quantifier -> unit
val assertion : Format.formatter -> Jc_constructors.assertion_with -> unit
val location_set : Format.formatter -> Jc_ast.tlocation_set -> unit
val location : Format.formatter -> Jc_ast.tlocation -> unit
val behavior : Format.formatter -> 'a * string * Jc_ast.behavior -> unit
val print_spec : Format.formatter -> Jc_ast.fun_spec -> unit
val call_bin_op : 'a -> 'b
val expr : Format.formatter -> Jc_constructors.expr_with -> unit
val case :
  Format.formatter ->
  Jc_constructors.expr_with option list * Jc_constructors.expr_with list ->
  unit
val handler :
  Format.formatter ->
  Jc_env.exception_info * Jc_env.var_info option * Jc_ast.expr -> unit
val statements : Format.formatter -> Jc_constructors.expr_with list -> unit
val block : Format.formatter -> Jc_constructors.expr_with list -> unit
val param : Format.formatter -> Jc_env.var_info -> unit
val field : Format.formatter -> Jc_env.field_info -> unit
val invariant :
  Format.formatter ->
  string * Jc_env.var_info * Jc_constructors.assertion_with -> unit
val term_or_assertion : Format.formatter -> Jc_ast.term_or_assertion -> unit
val print_super : Format.formatter -> string option -> unit
val string_of_invariant_policy : Jc_env.inv_sem -> string
val string_of_separation_policy : Jc_env.separation_sem -> string
val string_of_annotation_policy : Jc_env.annotation_sem -> string
val string_of_abstract_domain : Jc_env.abstract_domain -> string
val string_of_int_model : Jc_env.int_model -> string
val print_decl : Format.formatter -> jc_decl -> unit
val print_decls : Format.formatter -> jc_decl list -> unit