type native_type =
  Jc_env.native_type =
    Tunit
  | Tboolean
  | Tinteger
  | Treal
  | Tstring
type inv_sem = Jc_env.inv_sem = InvNone | InvOwnership | InvArguments
type separation_sem = Jc_env.separation_sem = SepNone | SepRegions
type annotation_sem =
  Jc_env.annotation_sem =
    AnnotNone
  | AnnotInvariants
  | AnnotWeakPre
  | AnnotStrongPre
type abstract_domain =
  Jc_env.abstract_domain =
    AbsNone
  | AbsBox
  | AbsOct
  | AbsPol
type int_model = Jc_env.int_model = IMbounded | IMmodulo
type jc_type =
  Jc_env.jc_type =
    JCTnative of native_type
  | JCTlogic of string
  | JCTenum of enum_info
  | JCTpointer of tag_or_variant * Num.num option * Num.num option
  | JCTnull
  | JCTany
  | JCTtype_var of Jc_type_var.t
and tag_or_variant =
  Jc_env.tag_or_variant =
    JCtag of struct_info * jc_type list
  | JCvariant of variant_info
  | JCunion of variant_info
and enum_info =
  Jc_env.enum_info = {
  jc_enum_info_name : string;
  jc_enum_info_min : Num.num;
  jc_enum_info_max : Num.num;
}
and struct_info =
  Jc_env.struct_info = {
  jc_struct_info_params : Jc_type_var.t list;
  jc_struct_info_name : string;
  mutable jc_struct_info_parent : (struct_info * jc_type list) option;
  mutable jc_struct_info_root : struct_info;
  mutable jc_struct_info_fields : field_info list;
  mutable jc_struct_info_variant : variant_info option;
}
and variant_info =
  Jc_env.variant_info = {
  jc_variant_info_name : string;
  mutable jc_variant_info_roots : struct_info list;
  jc_variant_info_is_union : bool;
}
and field_info =
  Jc_env.field_info = {
  jc_field_info_tag : int;
  jc_field_info_name : string;
  jc_field_info_final_name : string;
  jc_field_info_type : jc_type;
  jc_field_info_struct : struct_info;
  jc_field_info_root : struct_info;
  jc_field_info_rep : bool;
}
type field_or_variant_info =
  Jc_env.field_or_variant_info =
    FVfield of field_info
  | FVvariant of variant_info
type region =
  Jc_env.region = {
  mutable jc_reg_variable : bool;
  jc_reg_id : int;
  jc_reg_name : string;
  jc_reg_final_name : string;
  jc_reg_type : jc_type;
}
type var_info =
  Jc_env.var_info = {
  jc_var_info_tag : int;
  jc_var_info_name : string;
  mutable jc_var_info_final_name : string;
  mutable jc_var_info_type : jc_type;
  mutable jc_var_info_region : region;
  mutable jc_var_info_formal : bool;
  mutable jc_var_info_assigned : bool;
  jc_var_info_static : bool;
}
type exception_info =
  Jc_env.exception_info = {
  jc_exception_info_tag : int;
  jc_exception_info_name : string;
  jc_exception_info_type : jc_type option;
}
type label_info =
  Jc_env.label_info = {
  label_info_name : string;
  label_info_final_name : string;
  mutable times_used : int;
}
type logic_label =
  Jc_env.logic_label =
    LabelName of label_info
  | LabelHere
  | LabelPost
  | LabelPre
  | LabelOld