sig
  type prop_id
  val property_of_id : WpPropId.prop_id -> Property.t
  val doomed_if_valid : WpPropId.prop_id -> Property.t list
  val unreachable_if_valid : WpPropId.prop_id -> Property.other_loc
  val source_of_id : WpPropId.prop_id -> Filepath.position
  module PropId :
    sig
      type t = prop_id
      val ty : t Type.t
      val name : string
      val descr : t Descr.t
      val packed_descr : Structural_descr.pack
      val reprs : t list
      val equal : t -> t -> bool
      val compare : t -> t -> int
      val hash : t -> int
      val pretty_code : Format.formatter -> t -> unit
      val internal_pretty_code :
        Type.precedence -> Format.formatter -> t -> unit
      val pretty : Format.formatter -> t -> unit
      val varname : t -> string
      val mem_project : (Project_skeleton.t -> bool) -> t -> bool
      val copy : t -> t
    end
  val compare_prop_id : WpPropId.prop_id -> WpPropId.prop_id -> int
  val tactical : gid:string -> WpPropId.prop_id
  val is_check : WpPropId.prop_id -> bool
  val is_tactic : WpPropId.prop_id -> bool
  val is_assigns : WpPropId.prop_id -> bool
  val is_requires : Property.t -> bool
  val is_loop_preservation : WpPropId.prop_id -> Cil_types.stmt option
  val is_smoke_test : WpPropId.prop_id -> bool
  val select_default : WpPropId.prop_id -> bool
  val select_by_name : string list -> WpPropId.prop_id -> bool
  val select_call_pre :
    Cil_types.stmt -> Property.t option -> WpPropId.prop_id -> bool
  val prop_id_keys : WpPropId.prop_id -> string list * string list
  val get_propid : WpPropId.prop_id -> string
  val get_legacy : WpPropId.prop_id -> string
  val pp_propid : Stdlib.Format.formatter -> WpPropId.prop_id -> unit
  val user_bhv_names : Property.identified_property -> string list
  val user_prop_names : Property.identified_property -> string list
  val are_selected_names : string list -> string list -> bool
  type prop_kind =
      PKTactic
    | PKCheck
    | PKProp
    | PKEstablished
    | PKPreserved
    | PKPropLoop
    | PKVarDecr
    | PKVarPos
    | PKAFctOut
    | PKAFctExit
    | PKSmoke
    | PKPre of Cil_types.kernel_function * Cil_types.stmt * Property.t
  val pretty : Stdlib.Format.formatter -> WpPropId.prop_id -> unit
  val pretty_context :
    Description.kf -> Stdlib.Format.formatter -> WpPropId.prop_id -> unit
  val pretty_local : Stdlib.Format.formatter -> WpPropId.prop_id -> unit
  val label_of_prop_id : WpPropId.prop_id -> string
  val string_of_termination_kind : Cil_types.termination_kind -> string
  val num_of_bhv_from : Cil_types.funbehavior -> Cil_types.from -> int
  val mk_smoke :
    Cil_types.kernel_function ->
    id:string ->
    ?doomed:Property.t list ->
    ?unreachable:Cil_types.stmt -> unit -> WpPropId.prop_id
  val mk_code_annot_ids :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation -> WpPropId.prop_id list
  val mk_assert_id :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation -> WpPropId.prop_id
  val mk_loop_inv_id :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    established:bool -> Cil_types.code_annotation -> WpPropId.prop_id
  val mk_inv_hyp_id :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation -> WpPropId.prop_id
  val mk_var_decr_id :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation -> WpPropId.prop_id
  val mk_var_pos_id :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation -> WpPropId.prop_id
  val mk_loop_from_id :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.code_annotation -> Cil_types.from -> WpPropId.prop_id
  val mk_bhv_from_id :
    Cil_types.kernel_function ->
    Cil_types.kinstr ->
    string list ->
    Cil_types.funbehavior -> Cil_types.from -> WpPropId.prop_id
  val mk_fct_from_id :
    Cil_types.kernel_function ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind -> Cil_types.from -> WpPropId.prop_id
  val mk_disj_bhv_id :
    Cil_types.kernel_function * Cil_types.kinstr * string list * string list ->
    WpPropId.prop_id
  val mk_compl_bhv_id :
    Cil_types.kernel_function * Cil_types.kinstr * string list * string list ->
    WpPropId.prop_id
  val mk_decrease_id :
    Cil_types.kernel_function * Cil_types.kinstr * Cil_types.variant ->
    WpPropId.prop_id
  val mk_lemma_id : LogicUsage.logic_lemma -> WpPropId.prop_id
  val mk_stmt_assigns_id :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    string list ->
    Cil_types.funbehavior -> Cil_types.from list -> WpPropId.prop_id option
  val mk_loop_assigns_id :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.code_annotation ->
    Cil_types.from list -> WpPropId.prop_id option
  val mk_fct_assigns_id :
    Cil_types.kernel_function ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind ->
    Cil_types.from list -> WpPropId.prop_id option
  val mk_pre_id :
    Cil_types.kernel_function ->
    Cil_types.kinstr ->
    Cil_types.funbehavior ->
    Cil_types.identified_predicate -> WpPropId.prop_id
  val mk_stmt_post_id :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind * Cil_types.identified_predicate ->
    WpPropId.prop_id
  val mk_fct_post_id :
    Cil_types.kernel_function ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind * Cil_types.identified_predicate ->
    WpPropId.prop_id
  val mk_call_pre_id :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Property.t -> Property.t -> WpPropId.prop_id
  val mk_property : Property.t -> WpPropId.prop_id
  val mk_check : Property.t -> WpPropId.prop_id
  type a_kind = LoopAssigns | StmtAssigns
  type assigns_desc = private {
    a_label : Clabels.c_label;
    a_stmt : Cil_types.stmt option;
    a_kind : WpPropId.a_kind;
    a_assigns : Cil_types.assigns;
  }
  val pp_assigns_desc :
    Stdlib.Format.formatter -> WpPropId.assigns_desc -> unit
  type effect_source = FromCode | FromCall | FromReturn
  type assigns_info = WpPropId.prop_id * WpPropId.assigns_desc
  val assigns_info_id : WpPropId.assigns_info -> WpPropId.prop_id
  type assigns_full_info = private
      AssignsLocations of WpPropId.assigns_info
    | AssignsAny of WpPropId.assigns_desc
    | NoAssignsInfo
  val empty_assigns_info : WpPropId.assigns_full_info
  val mk_assigns_info :
    WpPropId.prop_id -> WpPropId.assigns_desc -> WpPropId.assigns_full_info
  val mk_stmt_any_assigns_info : Cil_types.stmt -> WpPropId.assigns_full_info
  val mk_kf_any_assigns_info : unit -> WpPropId.assigns_full_info
  val mk_loop_any_assigns_info : Cil_types.stmt -> WpPropId.assigns_full_info
  val pp_assign_info :
    string -> Stdlib.Format.formatter -> WpPropId.assigns_full_info -> unit
  val merge_assign_info :
    WpPropId.assigns_full_info ->
    WpPropId.assigns_full_info -> WpPropId.assigns_full_info
  val mk_loop_assigns_desc :
    Cil_types.stmt -> Cil_types.from list -> WpPropId.assigns_desc
  val mk_stmt_assigns_desc :
    Cil_types.stmt -> Cil_types.from list -> WpPropId.assigns_desc
  val mk_asm_assigns_desc : Cil_types.stmt -> WpPropId.assigns_desc
  val mk_kf_assigns_desc : Cil_types.from list -> WpPropId.assigns_desc
  val mk_init_assigns : WpPropId.assigns_desc
  val is_call_assigns : WpPropId.assigns_desc -> bool
  type axiom_info = WpPropId.prop_id * LogicUsage.logic_lemma
  val mk_axiom_info : LogicUsage.logic_lemma -> WpPropId.axiom_info
  val pp_axiom_info : Stdlib.Format.formatter -> WpPropId.axiom_info -> unit
  type pred_info = WpPropId.prop_id * Cil_types.predicate
  val mk_pred_info :
    WpPropId.prop_id -> Cil_types.predicate -> WpPropId.pred_info
  val pred_info_id : WpPropId.pred_info -> WpPropId.prop_id
  val pp_pred_of_pred_info :
    Stdlib.Format.formatter -> WpPropId.pred_info -> unit
  val pp_pred_info : Stdlib.Format.formatter -> WpPropId.pred_info -> unit
  val split_bag :
    (WpPropId.prop_id -> '-> unit) -> WpPropId.prop_id -> 'Bag.t -> unit
  val split_map :
    (WpPropId.prop_id -> '-> 'b) -> WpPropId.prop_id -> 'a list -> 'b list
  val mk_part : WpPropId.prop_id -> int * int -> WpPropId.prop_id
  val kind_of_id : WpPropId.prop_id -> WpPropId.prop_kind
  val parts_of_id : WpPropId.prop_id -> (int * int) option
  val subproofs : WpPropId.prop_id -> int
  val subproof_idx : WpPropId.prop_id -> int
  val get_induction : WpPropId.prop_id -> Cil_types.stmt option
end