diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 2be8813645a9ca63fd7b2c7403205f869ed79f77..532097186425bb770369cd7a91451ad21948a687 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -412,6 +412,141 @@ let rec has_status = function
(* -------------------------------------------------------------------------- *)
(* --- Datatype --- *)
(* -------------------------------------------------------------------------- *)
+let pp_active fmt active =
+ let sep = ref false in
+ let print_one a =
+ Format.fprintf fmt "%s%s" (if !sep then ", " else "") a;
+ sep:=true
+ in
+ Datatype.String.Set.iter print_one active
+
+let rec pretty_ip fmt = function
+ | IPPredicate {ip_kind; ip_pred} ->
+ Format.fprintf fmt "%a@ %a"
+ pretty_predicate_kind ip_kind
+ Cil_printer.pp_identified_predicate ip_pred
+ | IPExtended {ie_ext} -> Cil_printer.pp_extended fmt ie_ext
+ | IPAxiom {il_name} -> Format.fprintf fmt "axiom@ %s" il_name
+ | IPAxiomatic {iax_name} -> Format.fprintf fmt "axiomatic@ %s" iax_name
+ | IPLemma {il_name} -> Format.fprintf fmt "lemma@ %s" il_name
+ | IPTypeInvariant {iti_name; iti_type} ->
+ Format.fprintf fmt "invariant@ %s for type %a" iti_name
+ Cil_printer.pp_typ iti_type
+ | IPGlobalInvariant {igi_name} ->
+ Format.fprintf fmt "global invariant@ %s" igi_name
+ | IPBehavior {ib_bhv; ib_kinstr; ib_active} ->
+ if Cil.is_default_behavior ib_bhv then
+ Format.pp_print_string fmt "default behavior"
+ else
+ Format.fprintf fmt "behavior %s" ib_bhv.b_name;
+ (match ib_kinstr with
+ | Kstmt s -> Format.fprintf fmt " for statement %d" s.sid
+ | Kglobal -> ());
+ pp_active fmt ib_active
+ | IPCodeAnnot {ica_ca} -> Cil_printer.pp_code_annotation fmt ica_ca
+ | IPComplete {ic_active; ic_bhvs} ->
+ Format.fprintf fmt "complete@ %a"
+ (Pretty_utils.pp_iter ~sep:","
+ Datatype.String.Set.iter
+ (fun fmt s -> Format.fprintf fmt "@ %s" s))
+ ic_bhvs;
+ pp_active fmt ic_active
+ | IPDisjoint {ic_active; ic_bhvs} ->
+ Format.fprintf fmt "disjoint@ %a"
+ (Pretty_utils.pp_iter ~sep:","
+ Datatype.String.Set.iter
+ (fun fmt s -> Format.fprintf fmt "@ %s" s))
+ ic_bhvs;
+ pp_active fmt ic_active
+ | IPAllocation {ial_allocs=(f,a)} ->
+ Cil_printer.pp_allocation fmt (FreeAlloc(f,a))
+ | IPAssigns {ias_froms} -> Cil_printer.pp_assigns fmt (Writes ias_froms)
+ | IPFrom {if_from} -> Cil_printer.pp_from fmt if_from
+ | IPDecrease {id_ca=None; id_variant=v} -> Cil_printer.pp_decreases fmt v
+ | IPDecrease {id_variant=v} -> Cil_printer.pp_variant fmt v
+ | IPReachable {ir_kf=None; ir_kinstr=Kstmt _} -> assert false
+ | IPReachable {ir_kf=None; ir_kinstr=Kglobal} ->
+ Format.fprintf fmt "reachability of entry point"
+ | IPReachable {ir_kf=Some kf; ir_kinstr=Kglobal} ->
+ Format.fprintf fmt "reachability of function %a" Kf.pretty kf
+ | IPReachable {ir_kf=Some kf; ir_kinstr=Kstmt stmt; ir_program_point=ba} ->
+ Format.fprintf fmt "reachability %s stmt %a in %a"
+ (match ba with Before -> "of" | After -> "post")
+ Cil_datatype.Location.pretty_line (Cil_datatype.Stmt.loc stmt)
+ Kf.pretty kf
+ | IPPropertyInstance {ii_kf; ii_stmt; ii_ip} ->
+ Format.fprintf fmt "status of '%a'%t %a"
+ pretty_ip ii_ip
+ (fun fmt -> match get_kf ii_ip with
+ | Some kf -> Format.fprintf fmt " of %a" Kernel_function.pretty kf
+ | None -> ())
+ pretty_instance_location (ii_kf, ii_stmt)
+ | IPOther {io_name} -> Format.pp_print_string fmt io_name
+
+let rec hash_ip =
+ let hash_bhv_loop = function
+ | Id_contract (a,b) -> (0, Hashtbl.hash (a,b.b_name))
+ | Id_loop ca -> (1, ca.annot_id)
+ in
+ function
+ | IPPredicate {ip_pred=x} -> Hashtbl.hash (1, x.ip_id)
+ | IPAxiom {il_name=x} -> Hashtbl.hash (2, (x:string))
+ | IPAxiomatic {iax_name=x} -> Hashtbl.hash (3, (x:string))
+ | IPLemma {il_name=x} -> Hashtbl.hash (4, (x:string))
+ | IPCodeAnnot {ica_ca=ca} -> Hashtbl.hash (5, ca.annot_id)
+ | IPComplete {ic_kf=f; ic_kinstr=ki; ic_bhvs=y; ic_active=x} ->
+ (* complete list is more likely to discriminate than active list. *)
+ Hashtbl.hash
+ (6, Kf.hash f, Kinstr.hash ki,
+ Datatype.String.Set.hash y, Datatype.String.Set.hash x)
+ | IPDisjoint {ic_kf=f; ic_kinstr=ki; ic_bhvs=y; ic_active=x} ->
+ Hashtbl.hash
+ (7, Kf.hash f, Kinstr.hash ki,
+ Datatype.String.Set.hash y, Datatype.String.Set.hash x)
+ | IPAssigns {ias_kf=f; ias_kinstr=ki; ias_bhv=b} ->
+ Hashtbl.hash (8, Kf.hash f, Kinstr.hash ki, hash_bhv_loop b)
+ | IPFrom {if_kf=kf; if_kinstr=ki; if_bhv=b; if_from=(t, _)} ->
+ Hashtbl.hash
+ (9, Kf.hash kf, Kinstr.hash ki,
+ hash_bhv_loop b, Identified_term.hash t)
+ | IPDecrease {id_kf=kf; id_kinstr=ki} ->
+ (* At most one loop variant per statement anyway, no
+ need to discriminate against the code annotation itself *)
+ Hashtbl.hash (10, Kf.hash kf, Kinstr.hash ki)
+ | IPBehavior {ib_kf=kf; ib_kinstr=s; ib_active=a; ib_bhv=b} ->
+ Hashtbl.hash
+ (11, Kf.hash kf, Kinstr.hash s,
+ (b.b_name:string), (a:Datatype.String.Set.t))
+ | IPReachable {ir_kf=kf; ir_kinstr=ki; ir_program_point=ba} ->
+ Hashtbl.hash(12, Option.fold ~some:Kf.hash ~none:0 kf,
+ Kinstr.hash ki, Hashtbl.hash ba)
+ | IPAllocation {ial_kf=f; ial_kinstr=ki; ial_bhv=b} ->
+ Hashtbl.hash (13, Kf.hash f, Kinstr.hash ki, hash_bhv_loop b)
+ | IPPropertyInstance {ii_kf=kf_caller; ii_stmt=stmt; ii_ip=ip} ->
+ Hashtbl.hash (14, Kf.hash kf_caller,
+ Stmt.hash stmt, hash_ip ip)
+ | IPOther {io_name=s} -> Hashtbl.hash (15, (s:string))
+ | IPTypeInvariant {iti_name=s} -> Hashtbl.hash (16, (s:string))
+ | IPGlobalInvariant {igi_name=s} -> Hashtbl.hash (17, (s:string))
+ | IPExtended {ie_ext={ext_id}} -> Hashtbl.hash (18, ext_id)
+
+let reprs = [
+ IPAxiom {
+ il_name="";il_labels=[];il_args=[];
+ il_pred=Logic_const.(toplevel_predicate ptrue);
+ il_attrs=[];
+ il_loc=Location.unknown
+ }]
+
+let compare_behavior_or_loop b1 b2 =
+ match b1, b2 with
+ | Id_contract (a1,b1), Id_contract (a2,b2) ->
+ let n = Datatype.String.compare b1.b_name b2.b_name in
+ if n = 0 then Datatype.String.Set.compare a1 a2 else n
+ | Id_loop ca1, Id_loop ca2 ->
+ Datatype.Int.compare ca1.annot_id ca2.annot_id
+ | Id_contract _, Id_loop _ -> -1
+ | Id_loop _, Id_contract _ -> 1
include Datatype.Make_with_collections
(struct
@@ -420,133 +555,14 @@ include Datatype.Make_with_collections
type t = identified_property
let name = "Property.t"
- let reprs = [
- IPAxiom {
- il_name="";il_labels=[];il_args=[];
- il_pred=Logic_const.(toplevel_predicate ptrue);
- il_attrs=[];
- il_loc=Location.unknown
- }]
+
+ let reprs = reprs
let mem_project = Datatype.never_any_project
- let pp_active fmt active =
- let sep = ref false in
- let print_one a =
- Format.fprintf fmt "%s%s" (if !sep then ", " else "") a;
- sep:=true
- in
- Datatype.String.Set.iter print_one active
-
- let rec pretty fmt = function
- | IPPredicate {ip_kind; ip_pred} ->
- Format.fprintf fmt "%a@ %a"
- pretty_predicate_kind ip_kind
- Cil_printer.pp_identified_predicate ip_pred
- | IPExtended {ie_ext} -> Cil_printer.pp_extended fmt ie_ext
- | IPAxiom {il_name} -> Format.fprintf fmt "axiom@ %s" il_name
- | IPAxiomatic {iax_name} -> Format.fprintf fmt "axiomatic@ %s" iax_name
- | IPLemma {il_name} -> Format.fprintf fmt "lemma@ %s" il_name
- | IPTypeInvariant {iti_name; iti_type} ->
- Format.fprintf fmt "invariant@ %s for type %a" iti_name
- Cil_printer.pp_typ iti_type
- | IPGlobalInvariant {igi_name} ->
- Format.fprintf fmt "global invariant@ %s" igi_name
- | IPBehavior {ib_bhv; ib_kinstr; ib_active} ->
- if Cil.is_default_behavior ib_bhv then
- Format.pp_print_string fmt "default behavior"
- else
- Format.fprintf fmt "behavior %s" ib_bhv.b_name;
- (match ib_kinstr with
- | Kstmt s -> Format.fprintf fmt " for statement %d" s.sid
- | Kglobal -> ());
- pp_active fmt ib_active
- | IPCodeAnnot {ica_ca} -> Cil_printer.pp_code_annotation fmt ica_ca
- | IPComplete {ic_active; ic_bhvs} ->
- Format.fprintf fmt "complete@ %a"
- (Pretty_utils.pp_iter ~sep:","
- Datatype.String.Set.iter
- (fun fmt s -> Format.fprintf fmt "@ %s" s))
- ic_bhvs;
- pp_active fmt ic_active
- | IPDisjoint {ic_active; ic_bhvs} ->
- Format.fprintf fmt "disjoint@ %a"
- (Pretty_utils.pp_iter ~sep:","
- Datatype.String.Set.iter
- (fun fmt s -> Format.fprintf fmt "@ %s" s))
- ic_bhvs;
- pp_active fmt ic_active
- | IPAllocation {ial_allocs=(f,a)} ->
- Cil_printer.pp_allocation fmt (FreeAlloc(f,a))
- | IPAssigns {ias_froms} -> Cil_printer.pp_assigns fmt (Writes ias_froms)
- | IPFrom {if_from} -> Cil_printer.pp_from fmt if_from
- | IPDecrease {id_ca=None; id_variant=v} -> Cil_printer.pp_decreases fmt v
- | IPDecrease {id_variant=v} -> Cil_printer.pp_variant fmt v
- | IPReachable {ir_kf=None; ir_kinstr=Kstmt _} -> assert false
- | IPReachable {ir_kf=None; ir_kinstr=Kglobal} ->
- Format.fprintf fmt "reachability of entry point"
- | IPReachable {ir_kf=Some kf; ir_kinstr=Kglobal} ->
- Format.fprintf fmt "reachability of function %a" Kf.pretty kf
- | IPReachable {ir_kf=Some kf; ir_kinstr=Kstmt stmt; ir_program_point=ba} ->
- Format.fprintf fmt "reachability %s stmt %a in %a"
- (match ba with Before -> "of" | After -> "post")
- Cil_datatype.Location.pretty_line (Cil_datatype.Stmt.loc stmt)
- Kf.pretty kf
- | IPPropertyInstance {ii_kf; ii_stmt; ii_ip} ->
- Format.fprintf fmt "status of '%a'%t %a"
- pretty ii_ip
- (fun fmt -> match get_kf ii_ip with
- | Some kf -> Format.fprintf fmt " of %a" Kernel_function.pretty kf
- | None -> ())
- pretty_instance_location (ii_kf, ii_stmt)
- | IPOther {io_name} -> Format.pp_print_string fmt io_name
-
- let rec hash =
- let hash_bhv_loop = function
- | Id_contract (a,b) -> (0, Hashtbl.hash (a,b.b_name))
- | Id_loop ca -> (1, ca.annot_id)
- in
- function
- | IPPredicate {ip_pred=x} -> Hashtbl.hash (1, x.ip_id)
- | IPAxiom {il_name=x} -> Hashtbl.hash (2, (x:string))
- | IPAxiomatic {iax_name=x} -> Hashtbl.hash (3, (x:string))
- | IPLemma {il_name=x} -> Hashtbl.hash (4, (x:string))
- | IPCodeAnnot {ica_ca=ca} -> Hashtbl.hash (5, ca.annot_id)
- | IPComplete {ic_kf=f; ic_kinstr=ki; ic_bhvs=y; ic_active=x} ->
- (* complete list is more likely to discriminate than active list. *)
- Hashtbl.hash
- (6, Kf.hash f, Kinstr.hash ki,
- Datatype.String.Set.hash y, Datatype.String.Set.hash x)
- | IPDisjoint {ic_kf=f; ic_kinstr=ki; ic_bhvs=y; ic_active=x} ->
- Hashtbl.hash
- (7, Kf.hash f, Kinstr.hash ki,
- Datatype.String.Set.hash y, Datatype.String.Set.hash x)
- | IPAssigns {ias_kf=f; ias_kinstr=ki; ias_bhv=b} ->
- Hashtbl.hash (8, Kf.hash f, Kinstr.hash ki, hash_bhv_loop b)
- | IPFrom {if_kf=kf; if_kinstr=ki; if_bhv=b; if_from=(t, _)} ->
- Hashtbl.hash
- (9, Kf.hash kf, Kinstr.hash ki,
- hash_bhv_loop b, Identified_term.hash t)
- | IPDecrease {id_kf=kf; id_kinstr=ki} ->
- (* At most one loop variant per statement anyway, no
- need to discriminate against the code annotation itself *)
- Hashtbl.hash (10, Kf.hash kf, Kinstr.hash ki)
- | IPBehavior {ib_kf=kf; ib_kinstr=s; ib_active=a; ib_bhv=b} ->
- Hashtbl.hash
- (11, Kf.hash kf, Kinstr.hash s,
- (b.b_name:string), (a:Datatype.String.Set.t))
- | IPReachable {ir_kf=kf; ir_kinstr=ki; ir_program_point=ba} ->
- Hashtbl.hash(12, Option.fold ~some:Kf.hash ~none:0 kf,
- Kinstr.hash ki, Hashtbl.hash ba)
- | IPAllocation {ial_kf=f; ial_kinstr=ki; ial_bhv=b} ->
- Hashtbl.hash (13, Kf.hash f, Kinstr.hash ki, hash_bhv_loop b)
- | IPPropertyInstance {ii_kf=kf_caller; ii_stmt=stmt; ii_ip=ip} ->
- Hashtbl.hash (14, Kf.hash kf_caller,
- Stmt.hash stmt, hash ip)
- | IPOther {io_name=s} -> Hashtbl.hash (15, (s:string))
- | IPTypeInvariant {iti_name=s} -> Hashtbl.hash (16, (s:string))
- | IPGlobalInvariant {igi_name=s} -> Hashtbl.hash (17, (s:string))
- | IPExtended {ie_ext={ext_id}} -> Hashtbl.hash (18, ext_id)
+ let pretty = pretty_ip
+
+ let hash = hash_ip
let rec equal p1 p2 =
let eq_bhv (f1,ki1,b1) (f2,ki2,b2) =
@@ -577,7 +593,8 @@ include Datatype.Make_with_collections
IPComplete {ic_kf=f2;ic_kinstr=ki2;ic_active=a2;ic_bhvs=x2}
| IPDisjoint {ic_kf=f1;ic_kinstr=ki1;ic_active=a1;ic_bhvs=x1},
IPDisjoint {ic_kf=f2;ic_kinstr=ki2;ic_active=a2;ic_bhvs=x2} ->
- Kf.equal f1 f2 && Kinstr.equal ki1 ki2 && a1 = a2 && Datatype.String.Set.equal x1 x2
+ Kf.equal f1 f2 && Kinstr.equal ki1 ki2 && a1 = a2
+ && Datatype.String.Set.equal x1 x2
| IPAllocation {ial_kf=f1;ial_kinstr=ki1;ial_bhv=b1},
IPAllocation {ial_kf=f2;ial_kinstr=ki2;ial_bhv=b2}
| IPAssigns {ias_kf=f1;ias_kinstr=ki1;ias_bhv=b1},
@@ -617,14 +634,7 @@ include Datatype.Make_with_collections
if n = 0 then
let n = Kinstr.compare ki1 ki2 in
if n = 0 then
- match b1, b2 with
- | Id_contract (a1,b1), Id_contract (a2,b2) ->
- let n = Datatype.String.compare b1.b_name b2.b_name in
- if n = 0 then Datatype.String.Set.compare a1 a2 else n
- | Id_loop ca1, Id_loop ca2 ->
- Datatype.Int.compare ca1.annot_id ca2.annot_id
- | Id_contract _, Id_loop _ -> -1
- | Id_loop _, Id_contract _ -> 1
+ compare_behavior_or_loop b1 b2
else n
else n
in
@@ -718,6 +728,129 @@ include Datatype.Make_with_collections
end)
+module Ordered_by_function = Datatype.Make_with_collections(
+ struct
+ include Datatype.Serializable_undefined
+ type t = identified_property
+ let name = "Property.Ordered_by_function"
+ let reprs = reprs
+ let hash = hash_ip
+ let pretty = pretty_ip
+
+ (* be sure to keep cmp_same_kind synchronized with this function. *)
+ let cmp_kind p1 p2 =
+ let nb = function
+ | IPAxiomatic _ -> 1
+ | IPAxiom _ -> 2
+ | IPLemma _ -> 3
+ | IPTypeInvariant _ -> 4
+ | IPGlobalInvariant _ -> 5
+ | IPPropertyInstance _ -> 6
+ | IPBehavior _ -> 7
+ | IPPredicate { ip_kind = PKRequires _ } -> 8
+ | IPPredicate { ip_kind = PKAssumes _ } -> 9
+ | IPPredicate { ip_kind = PKEnsures _ } -> 10
+ | IPCodeAnnot { ica_ca = { annot_content = AAssert _ }} -> 11
+ | IPCodeAnnot { ica_ca = { annot_content = AInvariant _ }} -> 12
+ | IPCodeAnnot { ica_ca = { annot_content = APragma _ }} -> 13
+ | IPAssigns _ -> 14
+ | IPFrom _ -> 15
+ | IPAllocation _ -> 16
+ | IPPredicate { ip_kind = PKTerminates } -> 17
+ | IPDecrease _ -> 18
+ | IPReachable _ -> 18
+ | IPComplete _ -> 19
+ | IPDisjoint _ -> 20
+ | IPExtended _ -> 21
+ | IPOther _ -> 22
+ | IPCodeAnnot ca ->
+ Kernel.fatal "Unexpected code annot %a in identified property"
+ Cil_printer.pp_code_annotation ca.ica_ca
+ in
+ Datatype.Int.compare (nb p1) (nb p2)
+
+ let rec cmp_same_kind p1 p2 =
+ match (p1,p2) with
+ | IPAxiomatic { iax_name = n1 }, IPAxiomatic { iax_name = n2 }
+ | IPAxiom { il_name = n1 }, IPAxiom { il_name = n2 }
+ | IPLemma { il_name = n1 }, IPAxiom { il_name = n2 }
+ | IPTypeInvariant { iti_name = n1 }, IPTypeInvariant { iti_name = n2 }
+ | IPGlobalInvariant { igi_name = n1 },
+ IPGlobalInvariant { igi_name = n2 }
+ ->
+ String.compare n1 n2
+ | IPPropertyInstance { ii_ip = p1 }, IPPropertyInstance { ii_ip = p2 }
+ ->
+ let res = cmp_kind p1 p2 in
+ if res <> 0 then res else cmp_same_kind p1 p2
+ | IPBehavior { ib_active = a1; ib_bhv = b1 },
+ IPBehavior { ib_active = a2; ib_bhv = b2 } ->
+ compare_behavior_or_loop (Id_contract(a1,b1)) (Id_contract(a2,b2))
+ | IPPredicate { ip_pred = i1 }, IPPredicate { ip_pred = i2 } ->
+ Datatype.Int.compare i1.ip_id i2.ip_id
+ | IPCodeAnnot { ica_ca = a1 }, IPCodeAnnot { ica_ca = a2 } ->
+ Datatype.Int.compare a1.annot_id a2.annot_id
+ | IPAssigns { ias_bhv = b1 }, IPAssigns { ias_bhv = b2 }
+ | IPAllocation { ial_bhv = b1 }, IPAllocation { ial_bhv = b2 } ->
+ compare_behavior_or_loop b1 b2
+ | IPFrom { if_bhv = b1; if_from = (f1,_) },
+ IPFrom { if_bhv = b2; if_from = (f2,_) } ->
+ let res = compare_behavior_or_loop b1 b2 in
+ if res <> 0 then res
+ else Datatype.Int.compare f1.it_id f2.it_id
+ (* at most one decrease per statement *)
+ | IPDecrease _, IPDecrease _ -> 0
+ | IPReachable { ir_program_point = Before },
+ IPReachable { ir_program_point = After } -> -1
+ | IPReachable { ir_program_point = After },
+ IPReachable { ir_program_point = Before } -> 1
+ | IPReachable _, IPReachable _ -> 0
+
+ | IPComplete { ic_active = b1; ic_bhvs = s1 },
+ IPComplete { ic_active = b2; ic_bhvs = s2 }
+ | IPDisjoint { ic_active = b1; ic_bhvs = s1 },
+ IPDisjoint { ic_active = b2; ic_bhvs = s2 } ->
+ let res = Datatype.String.Set.compare b1 b2 in
+ if res <> 0 then res
+ else Datatype.String.Set.compare s1 s2
+ | IPExtended { ie_ext = e1 }, IPExtended { ie_ext = e2 } ->
+ Datatype.Int.compare e1.ext_id e2.ext_id
+ | IPOther { io_name = n1; io_loc = l1 },
+ IPOther { io_name = n2; io_loc = l2 } ->
+ let res = other_loc_compare l1 l2 in
+ if res <> 0 then res
+ else String.compare n1 n2
+ | _ ->
+ Kernel.fatal
+ "Property.cmp_same_kind called with 2 arguments of different kind"
+
+ let compare p1 p2 =
+ let kf1 = get_kf p1 and kf2 = get_kf p2 in
+ let cmp_kf kf1 kf2 =
+ String.compare
+ (Kernel_function.get_name kf1) (Kernel_function.get_name kf2)
+ in
+ let res = Option.compare cmp_kf kf1 kf2 in
+ if res <> 0 then res
+ else begin
+ let ki1 = get_kinstr p1 and ki2 = get_kinstr p2 in
+ let res =
+ match ki1, ki2 with
+ | Kglobal, Kglobal -> 0
+ | Kstmt _, Kglobal -> 1
+ | Kglobal, Kstmt _ -> -1
+ | Kstmt s1, Kstmt s2 -> Datatype.Int.compare s1.sid s2.sid
+ in
+ if res <> 0 then res
+ else begin
+ let res = cmp_kind p1 p2 in
+ if res <> 0 then res
+ else cmp_same_kind p1 p2
+ end
+ end
+ let equal = Datatype.from_compare
+ end)
+
let rec short_pretty fmt p = match p with
| IPPredicate {ip_pred} ->
(match (Logic_const.pred_of_id_pred ip_pred).pred_name with
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 6ad7e28371f3d73dfba4d67ff5a61f5dd1d98164..ab15f381a1b032e7a41c83ed3ffad3891ab39261 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -214,6 +214,18 @@ and identified_property = private
include Datatype.S_with_collections with type t = identified_property
+(** Datatype with alternative ordering, where properties are ordered according
+ the following criteria:
+ 1. Kf name (global properties ranked first)
+ 2. Kinstr
+ 3. kind of property
+ 4. id of the property
+
+ @since Frama-C+dev
+*)
+module Ordered_by_function:
+ Datatype.S_with_collections with type t = identified_property
+
val short_pretty: Format.formatter -> t -> unit
(** output a meaningful name for the property (e.g. the name of the
corresponding identified predicate when available)