sig   type prop_id   val property_of_id : WpPropId.prop_id -> Property.t   val source_of_id : WpPropId.prop_id -> Lexing.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 is_check : 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 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 pp_propid : Format.formatter -> WpPropId.prop_id -> unit   type prop_kind =       PKCheck     | PKProp     | PKEstablished     | PKPreserved     | PKPropLoop     | PKVarDecr     | PKVarPos     | PKAFctOut     | PKAFctExit     | PKPre of Cil_types.kernel_function * Cil_types.stmt * Property.t   val pretty : Format.formatter -> WpPropId.prop_id -> unit   val pretty_context :     Description.kf -> Format.formatter -> WpPropId.prop_id -> unit   val pretty_local : 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.identified_term Cil_types.from -> int   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_establish_id :     Cil_types.kernel_function ->     Cil_types.stmt -> Cil_types.code_annotation -> WpPropId.prop_id   val mk_preserve_id :     Cil_types.kernel_function ->     Cil_types.stmt -> 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.identified_term 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.identified_term Cil_types.from -> WpPropId.prop_id   val mk_fct_from_id :     Cil_types.kernel_function ->     Cil_types.funbehavior ->     Cil_types.termination_kind ->     Cil_types.identified_term 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.term 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.identified_term 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.identified_term 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.identified_term 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 : Cil_types.logic_label;     a_stmt : Cil_types.stmt option;     a_kind : WpPropId.a_kind;     a_assigns : Cil_types.identified_term Cil_types.assigns;   }   val pp_assigns_desc : 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 -> 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.identified_term Cil_types.from list -> WpPropId.assigns_desc   val mk_stmt_assigns_desc :     Cil_types.stmt ->     Cil_types.identified_term 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.identified_term 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 : 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 : Format.formatter -> WpPropId.pred_info -> unit   val pp_pred_info : Format.formatter -> WpPropId.pred_info -> unit   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