class identifier :
  ?loc:Loc.position ->
  string -> object method loc : Loc.position method name : string end
class ['a] node_located :
  ?loc:Loc.position ->
  'a -> object method loc : Loc.position method node : 'a end
class ptype :
  ?loc:Loc.position ->
  Jc_ast.ptype_node ->
  object method loc : Loc.position method node : Jc_ast.ptype_node end
class pexpr :
  ?loc:Loc.position ->
  Jc_ast.pexpr_node ->
  object method loc : Loc.position method node : Jc_ast.pexpr_node end
class pexpr_with :
  ?loc:Loc.position ->
  ?node:Jc_ast.pexpr_node ->
  < loc : Loc.position; node : Jc_ast.pexpr_node; .. > -> pexpr
class nexpr :
  ?loc:Loc.position ->
  ?logic_label:Jc_env.logic_label ->
  Jc_ast.nexpr_node ->
  object
    val mutable llab : Jc_env.logic_label option
    method loc : Loc.position
    method logic_label : Jc_env.logic_label option
    method node : Jc_ast.nexpr_node
    method set_logic_label : Jc_env.logic_label option -> unit
  end
class pattern :
  ?loc:Loc.position ->
  typ:Jc_env.jc_type ->
  Jc_ast.pattern_node ->
  object
    method loc : Loc.position
    method node : Jc_ast.pattern_node
    method typ : Jc_env.jc_type
  end
class term :
  ?loc:Loc.position ->
  typ:Jc_env.jc_type ->
  ?name_label:string ->
  ?region:Jc_env.region ->
  Jc_ast.term_node ->
  object
    val mutable r : Jc_env.region
    method loc : Loc.position
    method name_label : string
    method node : Jc_ast.term_node
    method region : Jc_env.region
    method set_region : Jc_env.region -> unit
    method typ : Jc_env.jc_type
  end
class term_with :
  ?loc:Loc.position ->
  ?typ:Jc_env.jc_type ->
  ?name_label:string ->
  ?region:Jc_env.region ->
  ?node:Jc_ast.term_node ->
  < loc : Loc.position; name_label : string; node : Jc_ast.term_node;
    region : Jc_env.region; typ : Jc_env.jc_type; .. > ->
  term
class term_var :
  ?loc:Loc.position -> ?name_label:string -> Jc_env.var_info -> term
class expr :
  ?loc:Loc.position ->
  typ:Jc_env.jc_type ->
  ?name_label:string ->
  ?region:Jc_env.region ->
  ?original_type:Jc_env.jc_type ->
  Jc_ast.expr_node ->
  object
    val mutable r : Jc_env.region
    method loc : Loc.position
    method name_label : string
    method node : Jc_ast.expr_node
    method original_type : Jc_env.jc_type
    method region : Jc_env.region
    method set_region : Jc_env.region -> unit
    method typ : Jc_env.jc_type
  end
class expr_with :
  ?loc:Loc.position ->
  ?typ:Jc_env.jc_type ->
  ?name_label:string ->
  ?region:Jc_env.region ->
  ?node:Jc_ast.expr_node ->
  ?original_type:Jc_env.jc_type ->
  < loc : Loc.position; name_label : string; node : Jc_ast.expr_node;
    original_type : Jc_env.jc_type; region : Jc_env.region;
    typ : Jc_env.jc_type; .. > ->
  expr
class assertion :
  ?name_label:string ->
  ?loc:Loc.position ->
  Jc_ast.assertion_node ->
  object
    method loc : Loc.position
    method name_label : string
    method node : Jc_ast.assertion_node
  end
class assertion_with :
  ?loc:Loc.position ->
  ?name_label:string ->
  ?node:Jc_ast.assertion_node ->
  < loc : Loc.position; name_label : string; node : Jc_ast.assertion_node;
    .. > ->
  assertion
class ['a] ptag :
  ?loc:Loc.position ->
  'a Jc_ast.ptag_node ->
  object method loc : Loc.position method node : 'a Jc_ast.ptag_node end
class tag :
  ?loc:Loc.position ->
  Jc_ast.tag_node ->
  object method loc : Loc.position method node : Jc_ast.tag_node end
class ['a] decl :
  ?loc:Loc.position ->
  'a Jc_ast.decl_node ->
  object method loc : Loc.position method node : 'a Jc_ast.decl_node end
module PExpr :
  sig
    val mkconst : const:Jc_ast.const -> ?loc:Loc.position -> unit -> pexpr
    val mkvoid : ?loc:Loc.position -> unit -> pexpr
    val mknull : ?loc:Loc.position -> unit -> pexpr
    val mkboolean : value:bool -> ?loc:Loc.position -> unit -> pexpr
    val mkint :
      ?value:int -> ?valuestr:string -> ?loc:Loc.position -> unit -> pexpr
    val mkbinary :
      expr1:Jc_ast.pexpr ->
      op:Jc_ast.bin_op ->
      expr2:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkand :
      ?expr1:Jc_ast.pexpr ->
      ?expr2:Jc_ast.pexpr ->
      ?list:Jc_ast.pexpr list -> ?loc:Loc.position -> unit -> Jc_ast.pexpr
    val mkor :
      ?expr1:Jc_ast.pexpr ->
      ?expr2:Jc_ast.pexpr ->
      ?list:Jc_ast.pexpr list -> ?loc:Loc.position -> unit -> Jc_ast.pexpr
    val mkadd :
      ?expr1:Jc_ast.pexpr ->
      ?expr2:Jc_ast.pexpr ->
      ?list:Jc_ast.pexpr list -> ?loc:Loc.position -> unit -> Jc_ast.pexpr
    val mklabel :
      label:string -> expr:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkvar : name:string -> ?loc:Loc.position -> unit -> pexpr
    val mkderef :
      expr:Jc_ast.pexpr -> field:string -> ?loc:Loc.position -> unit -> pexpr
    val mkunary :
      expr:Jc_ast.pexpr ->
      op:Jc_ast.pexpr_unary_op -> ?loc:Loc.position -> unit -> pexpr
    val mkapp :
      fun_name:string ->
      ?labels:Jc_env.logic_label list ->
      ?args:Jc_ast.pexpr list -> ?loc:Loc.position -> unit -> pexpr
    val mkassign :
      location:Jc_ast.pexpr ->
      value:Jc_ast.pexpr ->
      ?field:string ->
      ?op:Jc_ast.bin_op -> ?loc:Loc.position -> unit -> pexpr
    val mkinstanceof :
      expr:Jc_ast.pexpr -> typ:string -> ?loc:Loc.position -> unit -> pexpr
    val mkcast :
      expr:Jc_ast.pexpr -> typ:string -> ?loc:Loc.position -> unit -> pexpr
    val mkquantifier :
      quantifier:Jc_ast.quantifier ->
      typ:Jc_ast.ptype ->
      vars:string list ->
      body:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkforall :
      typ:Jc_ast.ptype ->
      vars:string list ->
      body:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkat :
      expr:Jc_ast.pexpr ->
      label:Jc_env.logic_label -> ?loc:Loc.position -> unit -> pexpr
    val mkoffset_max :
      expr:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkif :
      condition:Jc_ast.pexpr ->
      expr_then:Jc_ast.pexpr ->
      ?expr_else:pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkblock :
      exprs:Jc_ast.pexpr list -> ?loc:Loc.position -> unit -> pexpr
    val mklet :
      ?typ:Jc_ast.ptype ->
      var:string ->
      ?init:Jc_ast.pexpr ->
      body:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mklet_nodecl :
      ?typ:Jc_ast.ptype ->
      var:string ->
      ?init:Jc_ast.pexpr ->
      body:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkrange :
      ?left:Jc_ast.pexpr ->
      ?right:Jc_ast.pexpr ->
      ?locations:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkalloc :
      ?count:pexpr -> typ:string -> ?loc:Loc.position -> unit -> pexpr
    val mkassert : expr:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkwhile :
      ?condition:pexpr ->
      ?invariant:(string list * Jc_ast.pexpr) list ->
      ?variant:Jc_ast.pexpr ->
      body:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkfor :
      ?inits:Jc_ast.pexpr list ->
      ?condition:pexpr ->
      ?updates:Jc_ast.pexpr list ->
      ?invariant:pexpr ->
      ?variant:Jc_ast.pexpr ->
      body:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkreturn : ?expr:pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkbreak : ?label:string -> ?loc:Loc.position -> unit -> pexpr
    val mktry :
      expr:Jc_ast.pexpr ->
      ?catches:(Jc_ast.identifier * string * Jc_ast.pexpr) list ->
      ?finally:pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkthrow :
      exn:Jc_ast.identifier ->
      ?argument:pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkswitch :
      expr:Jc_ast.pexpr ->
      ?cases:(Jc_ast.pexpr option list * Jc_ast.pexpr) list ->
      ?loc:Loc.position -> unit -> pexpr
    val mkcatch :
      exn:'a ->
      ?name:string ->
      ?body:pexpr -> ?loc:Loc.position -> unit -> 'a * string * pexpr
    val mkshift :
      expr:Jc_ast.pexpr ->
      offset:Jc_ast.pexpr ->
      ?list:Jc_ast.pexpr list -> ?loc:Loc.position -> unit -> Jc_ast.pexpr
    val mknot : expr:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkeq :
      expr1:Jc_ast.pexpr ->
      expr2:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkimplies :
      expr1:Jc_ast.pexpr ->
      expr2:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkiff :
      expr1:Jc_ast.pexpr ->
      expr2:Jc_ast.pexpr -> ?loc:Loc.position -> unit -> pexpr
    val mkincr_heap :
      expr:Jc_ast.pexpr ->
      field:string ->
      ?op:Jc_ast.pexpr_unary_op -> ?loc:Loc.position -> unit -> pexpr
    val mkcontract :
      requires:Jc_ast.pexpr