type effect =
  Jc_fenv.effect = {
  jc_effect_alloc_table : Jc_region.StringRegionSet.t;
  jc_effect_tag_table : Jc_envset.LogicLabelSet.t Jc_envset.VariantMap.t;
  jc_effect_memories :
    Jc_envset.LogicLabelSet.t Jc_region.FieldOrVariantRegionMap.t;
  jc_effect_globals : Jc_envset.VarSet.t;
  jc_effect_mutable : Jc_envset.StringSet.t;
  jc_effect_committed : Jc_envset.StringSet.t;
}
type fun_effect =
  Jc_fenv.fun_effect = {
  jc_reads : effect;
  jc_writes : effect;
  jc_raises : Jc_envset.ExceptionSet.t;
}
type logic_info =
  Jc_fenv.logic_info = {
  jc_logic_info_tag : int;
  jc_logic_info_name : string;
  mutable jc_logic_info_final_name : string;
  mutable jc_logic_info_result_type : Jc_env.jc_type option;
  mutable jc_logic_info_result_region : Jc_env.region;
  mutable jc_logic_info_parameters : Jc_env.var_info list;
  mutable jc_logic_info_param_regions : Jc_env.region list;
  mutable jc_logic_info_effects : effect;
  mutable jc_logic_info_calls : logic_info list;
  mutable jc_logic_info_is_recursive : bool;
  mutable jc_logic_info_labels : Jc_env.logic_label list;
}
type fun_info =
  Jc_fenv.fun_info = {
  jc_fun_info_tag : int;
  jc_fun_info_name : string;
  mutable jc_fun_info_final_name : string;
  jc_fun_info_result : Jc_env.var_info;
  jc_fun_info_return_region : Jc_env.region;
  mutable jc_fun_info_parameters : Jc_env.var_info list;
  mutable jc_fun_info_param_regions : Jc_env.region list;
  mutable jc_fun_info_calls : fun_info list;
  mutable jc_fun_info_is_recursive : bool;
  mutable jc_fun_info_logic_apps : logic_info list;
  mutable jc_fun_info_effects : fun_effect;
}