sig
  type prop_id
  val property_of_id : Wp.WpPropId.prop_id -> Property.t
  val source_of_id : Wp.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 : Wp.WpPropId.prop_id -> Wp.WpPropId.prop_id -> int
  val tactical : gid:string -> Wp.WpPropId.prop_id
  val is_check : Wp.WpPropId.prop_id -> bool
  val is_tactic : Wp.WpPropId.prop_id -> bool
  val is_assigns : Wp.WpPropId.prop_id -> bool
  val is_requires : Property.t -> bool
  val is_loop_preservation : Wp.WpPropId.prop_id -> Cil_types.stmt option
  val select_default : Wp.WpPropId.prop_id -> bool
  val select_by_name : string list -> Wp.WpPropId.prop_id -> bool
  val select_call_pre :
    Cil_types.stmt -> Property.t option -> Wp.WpPropId.prop_id -> bool
  val prop_id_keys : Wp.WpPropId.prop_id -> string list * string list
  val get_propid : Wp.WpPropId.prop_id -> string
  val get_legacy : Wp.WpPropId.prop_id -> string
  val pp_propid : Stdlib.Format.formatter -> Wp.WpPropId.prop_id -> unit
  type prop_kind =
      PKTactic
    | PKCheck
    | PKProp
    | PKEstablished
    | PKPreserved
    | PKPropLoop
    | PKVarDecr
    | PKVarPos
    | PKAFctOut
    | PKAFctExit
    | PKPre of Cil_types.kernel_function * Cil_types.stmt * Property.t
  val pretty : Stdlib.Format.formatter -> Wp.WpPropId.prop_id -> unit
  val pretty_context :
    Description.kf -> Stdlib.Format.formatter -> Wp.WpPropId.prop_id -> unit
  val pretty_local : Stdlib.Format.formatter -> Wp.WpPropId.prop_id -> unit
  val label_of_prop_id : Wp.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_code_annot_ids :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id list
  val mk_assert_id :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
  val mk_loop_inv_id :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    established:bool -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
  val mk_inv_hyp_id :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
  val mk_var_decr_id :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
  val mk_var_pos_id :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
  val mk_loop_from_id :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.code_annotation -> Cil_types.from -> Wp.WpPropId.prop_id
  val mk_bhv_from_id :
    Cil_types.kernel_function ->
    Cil_types.kinstr ->
    string list ->
    Cil_types.funbehavior -> Cil_types.from -> Wp.WpPropId.prop_id
  val mk_fct_from_id :
    Cil_types.kernel_function ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind -> Cil_types.from -> Wp.WpPropId.prop_id
  val mk_disj_bhv_id :
    Cil_types.kernel_function * Cil_types.kinstr * string list * string list ->
    Wp.WpPropId.prop_id
  val mk_compl_bhv_id :
    Cil_types.kernel_function * Cil_types.kinstr * string list * string list ->
    Wp.WpPropId.prop_id
  val mk_decrease_id :
    Cil_types.kernel_function * Cil_types.kinstr * Cil_types.variant ->
    Wp.WpPropId.prop_id
  val mk_lemma_id : Wp.LogicUsage.logic_lemma -> Wp.WpPropId.prop_id
  val mk_stmt_assigns_id :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    string list ->
    Cil_types.funbehavior ->
    Cil_types.from list -> Wp.WpPropId.prop_id option
  val mk_loop_assigns_id :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.code_annotation ->
    Cil_types.from list -> Wp.WpPropId.prop_id option
  val mk_fct_assigns_id :
    Cil_types.kernel_function ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind ->
    Cil_types.from list -> Wp.WpPropId.prop_id option
  val mk_pre_id :
    Cil_types.kernel_function ->
    Cil_types.kinstr ->
    Cil_types.funbehavior ->
    Cil_types.identified_predicate -> Wp.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 ->
    Wp.WpPropId.prop_id
  val mk_fct_post_id :
    Cil_types.kernel_function ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind * Cil_types.identified_predicate ->
    Wp.WpPropId.prop_id
  val mk_call_pre_id :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Property.t -> Property.t -> Wp.WpPropId.prop_id
  val mk_property : Property.t -> Wp.WpPropId.prop_id
  val mk_check : Property.t -> Wp.WpPropId.prop_id
  type a_kind = LoopAssigns | StmtAssigns
  type assigns_desc = private {
    a_label : Wp.Clabels.c_label;
    a_stmt : Cil_types.stmt option;
    a_kind : Wp.WpPropId.a_kind;
    a_assigns : Cil_types.assigns;
  }
  val pp_assigns_desc :
    Stdlib.Format.formatter -> Wp.WpPropId.assigns_desc -> unit
  type effect_source = FromCode | FromCall | FromReturn
  type assigns_info = Wp.WpPropId.prop_id * Wp.WpPropId.assigns_desc
  val assigns_info_id : Wp.WpPropId.assigns_info -> Wp.WpPropId.prop_id
  type assigns_full_info = private
      AssignsLocations of Wp.WpPropId.assigns_info
    | AssignsAny of Wp.WpPropId.assigns_desc
    | NoAssignsInfo
  val empty_assigns_info : Wp.WpPropId.assigns_full_info
  val mk_assigns_info :
    Wp.WpPropId.prop_id ->
    Wp.WpPropId.assigns_desc -> Wp.WpPropId.assigns_full_info
  val mk_stmt_any_assigns_info :
    Cil_types.stmt -> Wp.WpPropId.assigns_full_info
  val mk_kf_any_assigns_info : unit -> Wp.WpPropId.assigns_full_info
  val mk_loop_any_assigns_info :
    Cil_types.stmt -> Wp.WpPropId.assigns_full_info
  val pp_assign_info :
    string ->
    Stdlib.Format.formatter -> Wp.WpPropId.assigns_full_info -> unit
  val merge_assign_info :
    Wp.WpPropId.assigns_full_info ->
    Wp.WpPropId.assigns_full_info -> Wp.WpPropId.assigns_full_info
  val mk_loop_assigns_desc :
    Cil_types.stmt -> Cil_types.from list -> Wp.WpPropId.assigns_desc
  val mk_stmt_assigns_desc :
    Cil_types.stmt -> Cil_types.from list -> Wp.WpPropId.assigns_desc
  val mk_asm_assigns_desc : Cil_types.stmt -> Wp.WpPropId.assigns_desc
  val mk_kf_assigns_desc : Cil_types.from list -> Wp.WpPropId.assigns_desc
  val mk_init_assigns : Wp.WpPropId.assigns_desc
  val is_call_assigns : Wp.WpPropId.assigns_desc -> bool
  type axiom_info = Wp.WpPropId.prop_id * Wp.LogicUsage.logic_lemma
  val mk_axiom_info : Wp.LogicUsage.logic_lemma -> Wp.WpPropId.axiom_info
  val pp_axiom_info :
    Stdlib.Format.formatter -> Wp.WpPropId.axiom_info -> unit
  type pred_info = Wp.WpPropId.prop_id * Cil_types.predicate
  val mk_pred_info :
    Wp.WpPropId.prop_id -> Cil_types.predicate -> Wp.WpPropId.pred_info
  val pred_info_id : Wp.WpPropId.pred_info -> Wp.WpPropId.prop_id
  val pp_pred_of_pred_info :
    Stdlib.Format.formatter -> Wp.WpPropId.pred_info -> unit
  val pp_pred_info : Stdlib.Format.formatter -> Wp.WpPropId.pred_info -> unit
  val mk_part : Wp.WpPropId.prop_id -> int * int -> Wp.WpPropId.prop_id
  val kind_of_id : Wp.WpPropId.prop_id -> Wp.WpPropId.prop_kind
  val parts_of_id : Wp.WpPropId.prop_id -> (int * int) option
  val subproofs : Wp.WpPropId.prop_id -> int
  val subproof_idx : Wp.WpPropId.prop_id -> int
  val get_induction : Wp.WpPropId.prop_id -> Cil_types.stmt option
end