From c28182fbe37bcc7dc2676adc820ea7e151a5e266 Mon Sep 17 00:00:00 2001
From: Virgile Robles <virgile.robles@protonmail.ch>
Date: Wed, 17 Jul 2019 14:30:17 +0200
Subject: [PATCH] [property] All identified_* from tuple to record
---
src/kernel_services/ast_data/property.ml | 1335 +++++++++--------
src/kernel_services/ast_data/property.mli | 141 +-
.../ast_data/property_status.ml | 107 +-
.../ast_data/statuses_by_call.ml | 2 +-
.../ast_printing/description.ml | 187 +--
.../ast_printing/printer_tag.ml | 4 +-
src/plugins/gui/design.ml | 106 +-
src/plugins/gui/pretty_source.ml | 13 +-
src/plugins/gui/property_navigator.ml | 67 +-
src/plugins/report/classify.ml | 48 +-
src/plugins/scope/dpds_gui.ml | 6 +-
src/plugins/value/gui_files/gui_eval.ml | 9 +-
src/plugins/value/gui_files/register_gui.ml | 21 +-
src/plugins/value/utils/red_statuses.ml | 3 +-
src/plugins/value/utils/value_results.ml | 8 +-
src/plugins/wp/Generator.ml | 48 +-
src/plugins/wp/GuiNavigator.ml | 6 +-
src/plugins/wp/GuiSource.ml | 2 +-
src/plugins/wp/LogicUsage.ml | 6 +-
src/plugins/wp/wpAnnot.ml | 47 +-
src/plugins/wp/wpPropId.ml | 113 +-
21 files changed, 1231 insertions(+), 1048 deletions(-)
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index ffd1ed30d7e..62b20fdd550 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -31,35 +31,55 @@ type behavior_or_loop =
Id_contract of Datatype.String.Set.t * funbehavior
| Id_loop of code_annotation
-type identified_complete =
- kernel_function * kinstr * Datatype.String.Set.t * string list
-type identified_disjoint = identified_complete
-type identified_code_annotation =
- kernel_function * stmt * code_annotation
-
-type identified_allocation =
- kernel_function
- * kinstr
- * behavior_or_loop
- * (identified_term list * identified_term list)
-
-type identified_assigns =
- kernel_function
- * kinstr
- * behavior_or_loop
- * from list
-
-type identified_from =
- kernel_function
- * kinstr
- * behavior_or_loop
- * from
-
-type identified_decrease =
- kernel_function * kinstr * code_annotation option * variant
-
-type identified_behavior =
- kernel_function * kinstr * Datatype.String.Set.t * funbehavior
+type identified_code_annotation = {
+ ica_kf : kernel_function;
+ ica_stmt : stmt;
+ ica_ca : code_annotation
+}
+
+type identified_assigns = {
+ ias_kf : kernel_function;
+ ias_kinstr : kinstr;
+ ias_bhv : behavior_or_loop;
+ ias_froms : from list
+}
+
+type identified_allocation = {
+ ial_kf : kernel_function;
+ ial_kinstr : kinstr;
+ ial_bhv : behavior_or_loop;
+ ial_allocs : identified_term list * identified_term list
+}
+
+type identified_from = {
+ if_kf : kernel_function;
+ if_kinstr : kinstr;
+ if_bhv : behavior_or_loop;
+ if_from : from
+}
+
+type identified_decrease = {
+ id_kf : kernel_function;
+ id_kinstr : kinstr;
+ id_ca : code_annotation option;
+ id_variant : variant
+}
+
+type identified_behavior = {
+ ib_kf : kernel_function;
+ ib_kinstr : kinstr;
+ ib_active : Datatype.String.Set.t;
+ ib_bhv : funbehavior
+}
+
+type identified_complete = {
+ ic_kf : kernel_function;
+ ic_kinstr : kinstr;
+ ic_active : Datatype.String.Set.t;
+ ic_bhvs : string list
+}
+
+type identified_disjoint = identified_complete
type predicate_kind =
| PKRequires of funbehavior
@@ -67,67 +87,75 @@ type predicate_kind =
| PKEnsures of funbehavior * termination_kind
| PKTerminates
-let pretty_predicate_kind fmt = function
- | PKRequires _ -> Format.pp_print_string fmt "requires"
- | PKAssumes _ -> Format.pp_print_string fmt "assumes"
- | PKEnsures(_, tk) ->
- Format.pp_print_string fmt
- (match tk with
- | Normal -> "ensures"
- | Exits -> "exits"
- | Breaks -> "breaks"
- | Continues -> "continues"
- | Returns -> "returns")
- | PKTerminates -> Format.pp_print_string fmt "terminates"
-
-type identified_predicate =
- predicate_kind * kernel_function * kinstr * Cil_types.identified_predicate
+type identified_predicate = {
+ ip_kind : predicate_kind;
+ ip_kf : kernel_function;
+ ip_kinstr : kinstr;
+ ip_pred : Cil_types.identified_predicate
+}
type program_point = Before | After
-type identified_reachable = kernel_function option * kinstr * program_point
-
-type identified_type_invariant = string * typ * predicate * location
-
-type identified_global_invariant = string * predicate * location
+type identified_reachable = {
+ ir_kf : kernel_function option;
+ ir_kinstr : kinstr;
+ ir_program_point : program_point
+}
type other_loc =
| OLContract of kernel_function
| OLStmt of kernel_function * stmt
| OLGlob of location
-let other_loc_equal le1 le2 =
- match le1, le2 with
- | OLContract kf1, OLContract kf2 -> Kernel_function.equal kf1 kf2
- | OLStmt (_,s1), OLStmt (_,s2) -> Cil_datatype.Stmt.equal s1 s2
- | OLGlob loc1, OLGlob loc2 -> Cil_datatype.Location.equal loc1 loc2
- | (OLContract _ | OLStmt _ | OLGlob _ ), _ -> false
-
-let other_loc_compare le1 le2 =
- match le1, le2 with
- | OLContract kf1, OLContract kf2 -> Kernel_function.compare kf1 kf2
- | OLContract _, _ -> 1 | _, OLContract _ -> -1
- | OLStmt (_,s1), OLStmt (_,s2) -> Cil_datatype.Stmt.compare s1 s2
- | OLStmt _, _ -> 1 | _, OLStmt _ -> -1
- | OLGlob loc1, OLGlob loc2 -> Cil_datatype.Location.compare loc1 loc2
-
type extended_loc =
| ELContract of kernel_function
| ELStmt of kernel_function * stmt
| ELGlob
-type identified_extended = extended_loc * Cil_types.acsl_extension
+type identified_extended = {
+ ie_loc : extended_loc;
+ ie_ext : Cil_types.acsl_extension
+}
-and identified_axiomatic = string * identified_property list
+and identified_axiomatic = {
+ iax_name : string;
+ iax_props : identified_property list
+}
-and identified_lemma =
- string * logic_label list * string list * predicate * location
+and identified_lemma = {
+ il_name : string;
+ il_labels : logic_label list;
+ il_args : string list;
+ il_pred : predicate;
+ il_loc : location
+}
and identified_axiom = identified_lemma
-and identified_instance =
- kernel_function * stmt * Cil_types.identified_predicate option
- * identified_property
+and identified_instance = {
+ ii_kf : kernel_function;
+ ii_stmt : stmt;
+ ii_pred : Cil_types.identified_predicate option;
+ ii_ip : identified_property
+}
+
+and identified_type_invariant = {
+ iti_name : string;
+ iti_type : typ;
+ iti_pred : predicate;
+ iti_loc : location
+}
+
+and identified_global_invariant = {
+ igi_name : string;
+ igi_pred : predicate;
+ igi_loc : location
+}
+
+and identified_other = {
+ io_name : string;
+ io_loc : other_loc
+}
and identified_property =
| IPPredicate of identified_predicate
@@ -147,7 +175,35 @@ and identified_property =
| IPPropertyInstance of identified_instance
| IPTypeInvariant of identified_type_invariant
| IPGlobalInvariant of identified_global_invariant
- | IPOther of string * other_loc
+ | IPOther of identified_other
+
+let pretty_predicate_kind fmt = function
+ | PKRequires _ -> Format.pp_print_string fmt "requires"
+ | PKAssumes _ -> Format.pp_print_string fmt "assumes"
+ | PKEnsures(_, tk) ->
+ Format.pp_print_string fmt
+ (match tk with
+ | Normal -> "ensures"
+ | Exits -> "exits"
+ | Breaks -> "breaks"
+ | Continues -> "continues"
+ | Returns -> "returns")
+ | PKTerminates -> Format.pp_print_string fmt "terminates"
+
+let other_loc_equal le1 le2 =
+ match le1, le2 with
+ | OLContract kf1, OLContract kf2 -> Kernel_function.equal kf1 kf2
+ | OLStmt (_,s1), OLStmt (_,s2) -> Cil_datatype.Stmt.equal s1 s2
+ | OLGlob loc1, OLGlob loc2 -> Cil_datatype.Location.equal loc1 loc2
+ | (OLContract _ | OLStmt _ | OLGlob _ ), _ -> false
+
+let other_loc_compare le1 le2 =
+ match le1, le2 with
+ | OLContract kf1, OLContract kf2 -> Kernel_function.compare kf1 kf2
+ | OLContract _, _ -> 1 | _, OLContract _ -> -1
+ | OLStmt (_,s1), OLStmt (_,s2) -> Cil_datatype.Stmt.compare s1 s2
+ | OLStmt _, _ -> 1 | _, OLStmt _ -> -1
+ | OLGlob loc1, OLGlob loc2 -> Cil_datatype.Location.compare loc1 loc2
(* -------------------------------------------------------------------------- *)
(* --- Getters --- *)
@@ -170,22 +226,22 @@ let o_loc_of_stmt kf = function
| Kstmt s -> OLStmt (kf,s)
let get_kinstr = function
- | IPPredicate (_,_,ki,_)
- | IPBehavior(_, ki,_,_)
- | IPComplete (_,ki,_,_)
- | IPDisjoint(_,ki,_,_)
- | IPAllocation (_,ki,_,_)
- | IPAssigns (_,ki,_,_)
- | IPFrom(_,ki,_,_)
- | IPReachable (_, ki, _)
- | IPDecrease (_,ki,_,_) -> ki
+ | IPPredicate {ip_kinstr=ki}
+ | IPBehavior {ib_kinstr=ki}
+ | IPComplete {ic_kinstr=ki}
+ | IPDisjoint {ic_kinstr=ki}
+ | IPAllocation {ial_kinstr=ki}
+ | IPAssigns {ias_kinstr=ki}
+ | IPFrom {if_kinstr=ki}
+ | IPReachable {ir_kinstr=ki}
+ | IPDecrease {id_kinstr=ki} -> ki
| IPAxiom _
| IPAxiomatic _
| IPLemma _ -> Kglobal
- | IPOther(_,loc_e) -> ki_of_o_loc loc_e
- | IPExtended (loc_e, _) -> ki_of_e_loc loc_e
- | IPCodeAnnot (_,s,_)
- | IPPropertyInstance (_, s, _, _) -> Kstmt s
+ | IPOther {io_loc} -> ki_of_o_loc io_loc
+ | IPExtended {ie_loc} -> ki_of_e_loc ie_loc
+ | IPCodeAnnot {ica_stmt=stmt}
+ | IPPropertyInstance {ii_stmt=stmt} -> Kstmt stmt
| IPTypeInvariant _ | IPGlobalInvariant _ -> Kglobal
let kf_of_loc_e = function
@@ -197,22 +253,22 @@ let kf_of_loc_o = function
| OLGlob _ -> None
let get_kf = function
- | IPPredicate (_,kf,_,_)
- | IPBehavior(kf,_,_,_)
- | IPCodeAnnot (kf,_,_)
- | IPComplete (kf,_,_,_)
- | IPDisjoint(kf,_,_,_)
- | IPAllocation(kf,_,_,_)
- | IPAssigns(kf,_,_,_)
- | IPFrom(kf,_,_,_)
- | IPDecrease (kf,_,_,_)
- | IPPropertyInstance (kf, _, _, _) -> Some kf
+ | IPPredicate {ip_kf=kf}
+ | IPBehavior {ib_kf=kf}
+ | IPCodeAnnot {ica_kf=kf}
+ | IPComplete {ic_kf=kf}
+ | IPDisjoint {ic_kf=kf}
+ | IPAllocation {ial_kf=kf}
+ | IPAssigns {ias_kf=kf}
+ | IPFrom {if_kf=kf}
+ | IPDecrease {id_kf=kf}
+ | IPPropertyInstance {ii_kf=kf} -> Some kf
| IPAxiom _
| IPAxiomatic _
| IPLemma _ -> None
- | IPReachable (kfopt, _, _) -> kfopt
- | IPExtended (loc_e,_) -> kf_of_loc_e loc_e
- | IPOther(_,loc_e) -> kf_of_loc_o loc_e
+ | IPReachable {ir_kf} -> ir_kf
+ | IPExtended {ie_loc} -> kf_of_loc_e ie_loc
+ | IPOther {io_loc} -> kf_of_loc_o io_loc
| IPTypeInvariant _ | IPGlobalInvariant _ -> None
let loc_of_kf_ki kf = function
@@ -225,38 +281,38 @@ let loc_of_loc_o = function
| OLGlob loc -> loc
let rec location = function
- | IPPredicate (_,_,_,ip) -> ip.ip_content.pred_loc
- | IPBehavior(kf,ki, _,_)
- | IPComplete (kf,ki,_,_)
- | IPDisjoint(kf,ki,_,_)
- | IPReachable(Some kf, ki, _) -> loc_of_kf_ki kf ki
- | IPReachable(None, Kstmt s, _)
- | IPPropertyInstance (_, s, _, _) -> Cil_datatype.Stmt.loc s
- | IPCodeAnnot (_,s,ca) -> (
+ | IPPredicate {ip_pred} -> ip_pred.ip_content.pred_loc
+ | IPBehavior {ib_kf=kf; ib_kinstr=ki}
+ | IPComplete {ic_kf=kf; ic_kinstr=ki}
+ | IPDisjoint {ic_kf=kf; ic_kinstr=ki}
+ | IPReachable {ir_kf=Some kf; ir_kinstr=ki} -> loc_of_kf_ki kf ki
+ | IPReachable {ir_kf=None; ir_kinstr=Kstmt s}
+ | IPPropertyInstance {ii_stmt=s} -> Cil_datatype.Stmt.loc s
+ | IPCodeAnnot {ica_stmt=s; ica_ca=ca} -> (
match Cil_datatype.Code_annotation.loc ca with
| None -> Cil_datatype.Stmt.loc s
| Some loc -> loc)
- | IPReachable(None, Kglobal, _) -> Cil_datatype.Location.unknown
- | IPAssigns(kf,ki,_,a) ->
+ | IPReachable {ir_kf=None; ir_kinstr=Kglobal} -> Cil_datatype.Location.unknown
+ | IPAssigns {ias_kf=kf; ias_kinstr=ki; ias_froms=a} ->
(match a with
| [] -> loc_of_kf_ki kf ki
| (t,_) :: _ -> t.it_content.term_loc)
- | IPAllocation(kf,ki,_,fa) ->
+ | IPAllocation {ial_kf=kf; ial_kinstr=ki; ial_allocs=fa} ->
(match fa with
| [],[] -> loc_of_kf_ki kf ki
| (t :: _),_
| _,(t :: _) -> t.it_content.term_loc)
- | IPFrom(_,_,_,(t,_)) -> t.it_content.term_loc
- | IPDecrease (_,_,_,(t,_)) -> t.term_loc
- | IPAxiom (_,_,_,_,loc) -> loc
- | IPAxiomatic (_,l) ->
- (match l with
+ | IPFrom {if_from=(t, _)} -> t.it_content.term_loc
+ | IPDecrease {id_variant=(t, _)} -> t.term_loc
+ | IPAxiom {il_loc} -> il_loc
+ | IPAxiomatic {iax_props} ->
+ (match iax_props with
| [] -> Cil_datatype.Location.unknown
| p :: _ -> location p)
- | IPLemma (_,_,_,_,loc) -> loc
- | IPExtended(_,{ext_loc}) -> ext_loc
- | IPOther(_,loc_e) -> loc_of_loc_o loc_e
- | IPTypeInvariant(_,_,_,loc) | IPGlobalInvariant(_,_,loc) -> loc
+ | IPLemma {il_loc} -> il_loc
+ | IPExtended {ie_ext={ext_loc}} -> ext_loc
+ | IPOther {io_loc} -> loc_of_loc_o io_loc
+ | IPTypeInvariant {iti_loc=loc} | IPGlobalInvariant {igi_loc=loc} -> loc
let source ip =
let loc = location ip in
@@ -277,21 +333,21 @@ let get_pk_behavior = function
| PKTerminates -> None
let get_behavior = function
- | IPPredicate (pk,_,_,_) -> get_pk_behavior pk
- | IPBehavior(_, _, _, b) -> Some b
- | IPAllocation(_,_,Id_contract (_,b),_)
- | IPAssigns(_,_,Id_contract (_,b),_)
- | IPFrom(_,_,Id_contract (_,b),_) -> Some b
- | IPAllocation(_,_,Id_loop _,_)
- | IPAssigns(_,_,Id_loop _,_)
- | IPFrom(_,_,Id_loop _,_)
+ | IPPredicate {ip_kind} -> get_pk_behavior ip_kind
+ | IPBehavior {ib_bhv=b}
+ | IPAllocation {ial_bhv=Id_contract (_, b)}
+ | IPAssigns {ias_bhv=Id_contract (_, b)}
+ | IPFrom {if_bhv=Id_contract (_, b)} -> Some b
+ | IPAllocation {ial_bhv=Id_loop _}
+ | IPAssigns {ias_bhv=Id_loop _}
+ | IPFrom {if_bhv=Id_loop _}
| IPAxiom _
| IPAxiomatic _
| IPExtended _
| IPLemma _
- | IPCodeAnnot (_,_,_)
- | IPComplete (_,_,_,_)
- | IPDisjoint(_,_,_,_)
+ | IPCodeAnnot _
+ | IPComplete _
+ | IPDisjoint _
| IPDecrease _
| IPReachable _
| IPPropertyInstance _
@@ -318,10 +374,10 @@ let has_status_pkind = function
-> true
let rec has_status = function
- | IPPredicate(pkind, _, _, _) -> has_status_pkind pkind
- | IPExtended(_,e) -> has_status_ext e
- | IPCodeAnnot(_,_, { annot_content = ca }) -> has_status_ca ca
- | IPPropertyInstance(_,_,_,ip) -> has_status ip
+ | IPPredicate {ip_kind} -> has_status_pkind ip_kind
+ | IPExtended {ie_ext} -> has_status_ext ie_ext
+ | IPCodeAnnot {ica_ca={annot_content}} -> has_status_ca annot_content
+ | IPPropertyInstance {ii_ip} -> has_status ii_ip
| IPOther _ | IPReachable _
| IPAxiom _ | IPAxiomatic _ | IPBehavior _
| IPDisjoint _ | IPComplete _
@@ -341,7 +397,8 @@ include Datatype.Make_with_collections
type t = identified_property
let name = "Property.t"
- let reprs = [ IPAxiom ("",[],[],Logic_const.ptrue,Location.unknown) ]
+ let reprs = [IPAxiom {il_name="";il_labels=[];il_args=[];
+ il_pred=Logic_const.ptrue;il_loc=Location.unknown}]
let mem_project = Datatype.never_any_project
let pp_active fmt active =
@@ -353,195 +410,207 @@ include Datatype.Make_with_collections
Datatype.String.Set.iter print_one active
let rec pretty fmt = function
- | IPPredicate (kind,_,_,p) ->
+ | IPPredicate {ip_kind; ip_pred} ->
Format.fprintf fmt "%a@ %a"
- pretty_predicate_kind kind Cil_printer.pp_identified_predicate p
- | IPExtended (_,e) -> Cil_printer.pp_extended fmt e
- | IPAxiom (s,_,_,_,_) -> Format.fprintf fmt "axiom@ %s" s
- | IPAxiomatic(s, _) -> Format.fprintf fmt "axiomatic@ %s" s
- | IPLemma (s,_,_,_,_) -> Format.fprintf fmt "lemma@ %s" s
- | IPTypeInvariant(s,ty,_,_) ->
- Format.fprintf fmt "invariant@ %s for type %a" s Cil_printer.pp_typ ty
- | IPGlobalInvariant(s,_,_) ->
- Format.fprintf fmt "global invariant@ %s" s
- | IPBehavior(_kf, ki, active, b) ->
- if Cil.is_default_behavior b then
- Format.pp_print_string fmt "default behavior"
- else
- Format.fprintf fmt "behavior %s" b.b_name;
- (match ki with
- | Kstmt s -> Format.fprintf fmt " for statement %d" s.sid
- | Kglobal -> ());
- pp_active fmt active
- | IPCodeAnnot(_, _, a) -> Cil_printer.pp_code_annotation fmt a
- | IPComplete(_, _, active, l) ->
- Format.fprintf fmt "complete@ %a"
- (Pretty_utils.pp_list ~sep:","
- (fun fmt s -> Format.fprintf fmt "@ %s" s))
- l;
- pp_active fmt active
- | IPDisjoint(_, _, active, l) ->
- Format.fprintf fmt "disjoint@ %a"
- (Pretty_utils.pp_list ~sep:","
- (fun fmt s -> Format.fprintf fmt " %s" s))
- l;
- pp_active fmt active
- | IPAllocation(_, _, _, (f,a)) ->
- Cil_printer.pp_allocation fmt (FreeAlloc(f,a))
- | IPAssigns(_, _, _, l) -> Cil_printer.pp_assigns fmt (Writes l)
- | IPFrom (_,_,_, f) -> Cil_printer.pp_from fmt f
- | IPDecrease(_, _, None,v) -> Cil_printer.pp_decreases fmt v
- | IPDecrease(_, _, _,v) -> Cil_printer.pp_variant fmt v
- | IPReachable(None, Kstmt _, _) -> assert false
- | IPReachable(None, Kglobal, _) ->
- Format.fprintf fmt "reachability of entry point"
- | IPReachable(Some kf, Kglobal, _) ->
- Format.fprintf fmt "reachability of function %a" Kf.pretty kf
- | IPReachable(Some kf, Kstmt stmt, 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 (kf, ki, _, ip) ->
- Format.fprintf fmt "status of '%a'%t %a"
- pretty ip
- (fun fmt -> match get_kf ip with
- | Some kf -> Format.fprintf fmt " of %a" Kernel_function.pretty kf
- | None -> ())
- pretty_instance_location (kf, ki)
- | IPOther(s,_) -> Format.pp_print_string fmt s
+ 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_list ~sep:","
+ (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_list ~sep:","
+ (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
+ 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 (_,_,_,x) -> Hashtbl.hash (1, x.ip_id)
- | IPAxiom (x,_,_,_,_) -> Hashtbl.hash (2, (x:string))
- | IPAxiomatic (x,_) -> Hashtbl.hash (3, (x:string))
- | IPLemma (x,_,_,_,_) -> Hashtbl.hash (4, (x:string))
- | IPCodeAnnot(_,_, ca) -> Hashtbl.hash (5, ca.annot_id)
- | IPComplete(f, ki, x, y) ->
+ 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
+ Hashtbl.hash
(6, Kf.hash f, Kinstr.hash ki,
(y:string list), (x:Datatype.String.Set.t))
- | IPDisjoint(f, ki, x, y) ->
- Hashtbl.hash
+ | IPDisjoint {ic_kf=f; ic_kinstr=ki; ic_bhvs=y; ic_active=x} ->
+ Hashtbl.hash
(7, Kf.hash f, Kinstr.hash ki,
(y: string list), (x:Datatype.String.Set.t))
- | IPAssigns(f, ki, b, _l) ->
- Hashtbl.hash (8, Kf.hash f, Kinstr.hash ki, hash_bhv_loop b)
- | IPFrom(kf,ki,b,(t,_)) ->
+ | 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(kf, ki, _ca, _v) ->
- (* 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(kf, s, a, b) ->
- Hashtbl.hash
+ | 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(kf, ki, ba) ->
- Hashtbl.hash(12, Extlib.may_map Kf.hash ~dft:0 kf,
+ | IPReachable {ir_kf=kf; ir_kinstr=ki; ir_program_point=ba} ->
+ Hashtbl.hash(12, Extlib.may_map Kf.hash ~dft:0 kf,
Kinstr.hash ki, Hashtbl.hash ba)
- | IPAllocation(f, ki, b, _fa) ->
- Hashtbl.hash (13, Kf.hash f, Kinstr.hash ki, hash_bhv_loop b)
- | IPPropertyInstance (kf_caller, stmt, _, ip) ->
- Hashtbl.hash (14, Kf.hash kf_caller,
- Stmt.hash stmt, hash ip)
- | IPOther(s,_) -> Hashtbl.hash (15, (s:string))
- | IPTypeInvariant(s,_,_,_) -> Hashtbl.hash (16, (s:string))
- | IPGlobalInvariant(s,_,_) -> Hashtbl.hash (17, (s:string))
- | IPExtended (_,{ext_id}) -> Hashtbl.hash (18, ext_id)
+ | 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 rec equal p1 p2 =
- let eq_bhv (f1,ki1,b1) (f2,ki2,b2) =
- Kf.equal f1 f2 && Kinstr.equal ki1 ki2
- &&
- (match b1, b2 with
- | Id_loop ca1, Id_loop ca2 ->
- ca1.annot_id = ca2.annot_id
- | Id_contract (a1,b1), Id_contract (a2,b2) ->
- Datatype.String.Set.equal a1 a2 &&
- Datatype.String.equal b1.b_name b2.b_name
- | Id_loop _, Id_contract _
- | Id_contract _, Id_loop _ -> false)
- in
- match p1, p2 with
- | IPPredicate (_,_,_,s1), IPPredicate (_,_,_,s2) -> s1.ip_id = s2.ip_id
- | IPExtended (_,{ext_id=i1}), IPExtended (_,{ext_id=i2}) ->
- Datatype.Int.equal i1 i2
- | IPAxiom (s1,_,_,_,_), IPAxiom (s2,_,_,_,_)
- | IPAxiomatic(s1, _), IPAxiomatic(s2, _)
- | IPTypeInvariant(s1,_,_,_), IPTypeInvariant(s2,_,_,_)
- | IPGlobalInvariant(s1,_,_), IPGlobalInvariant(s2,_,_)
- | IPLemma (s1,_,_,_,_), IPLemma (s2,_,_,_,_) ->
- Datatype.String.equal s1 s2
- | IPCodeAnnot(_,_,ca1), IPCodeAnnot(_,_,ca2) ->
+ let eq_bhv (f1,ki1,b1) (f2,ki2,b2) =
+ Kf.equal f1 f2 && Kinstr.equal ki1 ki2
+ &&
+ (match b1, b2 with
+ | Id_loop ca1, Id_loop ca2 ->
+ ca1.annot_id = ca2.annot_id
+ | Id_contract (a1,b1), Id_contract (a2,b2) ->
+ Datatype.String.Set.equal a1 a2 &&
+ Datatype.String.equal b1.b_name b2.b_name
+ | Id_loop _, Id_contract _
+ | Id_contract _, Id_loop _ -> false)
+ in
+ match p1, p2 with
+ | IPPredicate {ip_pred=s1}, IPPredicate {ip_pred=s2} -> s1.ip_id = s2.ip_id
+ | IPExtended {ie_ext={ext_id=i1}}, IPExtended {ie_ext={ext_id=i2}} ->
+ Datatype.Int.equal i1 i2
+ | IPAxiom {il_name=s1}, IPAxiom {il_name=s2}
+ | IPAxiomatic {iax_name=s1}, IPAxiomatic {iax_name=s2}
+ | IPTypeInvariant {iti_name=s1}, IPTypeInvariant {iti_name=s2}
+ | IPGlobalInvariant {igi_name=s1}, IPGlobalInvariant {igi_name=s2}
+ | IPLemma {il_name=s1}, IPLemma {il_name=s2} ->
+ Datatype.String.equal s1 s2
+ | IPCodeAnnot {ica_ca=ca1}, IPCodeAnnot {ica_ca=ca2} ->
ca1.annot_id = ca2.annot_id
- | IPComplete(f1, ki1, a1, x1), IPComplete(f2, ki2, a2, x2)
- | IPDisjoint(f1, ki1, a1, x1), IPDisjoint(f2, ki2, a2, x2) ->
- Kf.equal f1 f2 && Kinstr.equal ki1 ki2 && a1 = a2 && x1 = x2
- | IPAllocation (f1, ki1, b1, _), IPAllocation (f2, ki2, b2, _) ->
+ | IPComplete {ic_kf=f1;ic_kinstr=ki1;ic_active=a1;ic_bhvs=x1},
+ 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 && 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},
+ IPAssigns {ias_kf=f2;ias_kinstr=ki2;ias_bhv=b2} ->
eq_bhv (f1,ki1,b1) (f2,ki2,b2)
- | IPAssigns (f1, ki1, b1, _), IPAssigns (f2, ki2, b2, _) ->
- eq_bhv (f1,ki1,b1) (f2,ki2,b2)
- | IPFrom (f1,ki1,b1,(t1,_)), IPFrom (f2, ki2,b2,(t2,_)) ->
+ | IPFrom {if_kf=f1;if_kinstr=ki1;if_bhv=b1;if_from=(t1,_)},
+ IPFrom {if_kf=f2;if_kinstr=ki2;if_bhv=b2;if_from=(t2,_)} ->
eq_bhv (f1,ki1,b1) (f2,ki2,b2) && t1.it_id = t2.it_id
- | IPDecrease(f1, ki1, _, _), IPDecrease(f2, ki2, _, _) ->
- Kf.equal f1 f2 && Kinstr.equal ki1 ki2
- | IPReachable(kf1, ki1, ba1), IPReachable(kf2, ki2, ba2) ->
- Extlib.opt_equal Kf.equal kf1 kf2 && Kinstr.equal ki1 ki2 && ba1 = ba2
- | IPBehavior(f1, k1, a1, b1), IPBehavior(f2, k2, a2, b2) ->
- Kf.equal f1 f2
- && Kinstr.equal k1 k2
+ | IPDecrease {id_kf=f1; id_kinstr=ki1},
+ IPDecrease {id_kf=f2; id_kinstr=ki2} ->
+ Kf.equal f1 f2 && Kinstr.equal ki1 ki2
+ | IPReachable {ir_kf=kf1; ir_kinstr=ki1; ir_program_point=ba1},
+ IPReachable {ir_kf=kf2; ir_kinstr=ki2; ir_program_point=ba2} ->
+ Extlib.opt_equal Kf.equal kf1 kf2 && Kinstr.equal ki1 ki2 && ba1 = ba2
+ | IPBehavior {ib_kf=f1; ib_kinstr=k1; ib_active=a1; ib_bhv=b1},
+ IPBehavior {ib_kf=f2; ib_kinstr=k2; ib_active=a2; ib_bhv=b2} ->
+ Kf.equal f1 f2
+ && Kinstr.equal k1 k2
&& Datatype.String.Set.equal a1 a2
- && Datatype.String.equal b1.b_name b2.b_name
- | IPOther(s1,loc_e1), IPOther(s2,loc_e2) ->
- Datatype.String.equal s1 s2
- && other_loc_equal loc_e1 loc_e2
- | IPPropertyInstance (kf1, s1, _, ip1),
- IPPropertyInstance (kf2, s2, _, ip2) ->
- Kernel_function.equal kf1 kf2 &&
- Stmt.equal s1 s2 && equal ip1 ip2
- | (IPPredicate _ | IPAxiom _ | IPExtended _ | IPAxiomatic _ | IPLemma _
- | IPCodeAnnot _ | IPComplete _ | IPDisjoint _ | IPAssigns _
- | IPFrom _ | IPDecrease _ | IPBehavior _ | IPReachable _
- | IPAllocation _ | IPOther _ | IPPropertyInstance _
- | IPTypeInvariant _ | IPGlobalInvariant _), _ -> false
+ && Datatype.String.equal b1.b_name b2.b_name
+ | IPOther {io_name=s1;io_loc=l1}, IPOther {io_name=s2;io_loc=l2} ->
+ Datatype.String.equal s1 s2
+ && other_loc_equal l1 l2
+ | IPPropertyInstance {ii_kf=kf1;ii_stmt=s1;ii_ip=ip1},
+ IPPropertyInstance {ii_kf=kf2;ii_stmt=s2;ii_ip=ip2} ->
+ Kernel_function.equal kf1 kf2 &&
+ Stmt.equal s1 s2 && equal ip1 ip2
+ | (IPPredicate _ | IPAxiom _ | IPExtended _ | IPAxiomatic _ | IPLemma _
+ | IPCodeAnnot _ | IPComplete _ | IPDisjoint _ | IPAssigns _
+ | IPFrom _ | IPDecrease _ | IPBehavior _ | IPReachable _
+ | IPAllocation _ | IPOther _ | IPPropertyInstance _
+ | IPTypeInvariant _ | IPGlobalInvariant _), _ -> false
let rec compare x y =
- let cmp_bhv (f1,ki1,b1) (f2,ki2,b2) =
- let n = Kf.compare f1 f2 in
- 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
+ let cmp_bhv (f1,ki1,b1) (f2,ki2,b2) =
+ let n = Kf.compare f1 f2 in
+ 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
+ Datatype.Int.compare ca1.annot_id ca2.annot_id
| Id_contract _, Id_loop _ -> -1
| Id_loop _, Id_contract _ -> 1
else n
else n
- in
- match x, y with
- | IPPredicate (_,_,_,s1), IPPredicate (_,_,_,s2) ->
+ in
+ match x, y with
+ | IPPredicate {ip_pred=s1}, IPPredicate {ip_pred=s2} ->
Datatype.Int.compare s1.ip_id s2.ip_id
- | IPExtended (_,{ext_id=i1}), IPExtended (_,{ext_id=i2}) ->
+ | IPExtended {ie_ext={ext_id=i1}}, IPExtended {ie_ext={ext_id=i2}} ->
Datatype.Int.compare i1 i2
- | IPCodeAnnot(_,_,ca1), IPCodeAnnot(_,_,ca2) ->
+ | IPCodeAnnot {ica_ca=ca1}, IPCodeAnnot {ica_ca=ca2} ->
Datatype.Int.compare ca1.annot_id ca2.annot_id
- | IPBehavior(f1, k1, a1, b1), IPBehavior(f2, k2, a2, b2) ->
- cmp_bhv (f1, k1, Id_contract (a1,b1)) (f2, k2, Id_contract (a2,b2))
- | IPComplete(f1, ki1, a1, x1), IPComplete(f2, ki2, a2, x2)
- | IPDisjoint(f1, ki1, a1, x1), IPDisjoint(f2, ki2, a2, x2) ->
+ | IPBehavior {ib_kf=f1; ib_kinstr=k1; ib_active=a1; ib_bhv=b1},
+ IPBehavior {ib_kf=f2; ib_kinstr=k2; ib_active=a2; ib_bhv=b2} ->
+ cmp_bhv (f1, k1, Id_contract (a1,b1)) (f2, k2, Id_contract (a2,b2))
+ | IPComplete {ic_kf=f1;ic_kinstr=ki1;ic_active=a1;ic_bhvs=x1},
+ 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} ->
let n = Kf.compare f1 f2 in
if n = 0 then
let n = Kinstr.compare ki1 ki2 in
@@ -552,105 +621,108 @@ include Datatype.Make_with_collections
else n
else n
else n
- | IPAssigns (f1, ki1, b1, _), IPAssigns (f2, ki2, b2, _) ->
+ | IPAssigns {ias_kf=f1;ias_kinstr=ki1;ias_bhv=b1},
+ IPAssigns {ias_kf=f2;ias_kinstr=ki2;ias_bhv=b2} ->
cmp_bhv (f1,ki1,b1) (f2,ki2,b2)
- | IPFrom (f1,ki1,b1,(t1,_)), IPFrom(f2,ki2,b2,(t2,_)) ->
+ | IPFrom {if_kf=f1;if_kinstr=ki1;if_bhv=b1;if_from=(t1,_)},
+ IPFrom {if_kf=f2;if_kinstr=ki2;if_bhv=b2;if_from=(t2,_)} ->
let n = cmp_bhv (f1,ki1,b1) (f2,ki2,b2) in
if n = 0 then Identified_term.compare t1 t2 else n
- | IPDecrease(f1, ki1,_,_), IPDecrease(f2, ki2,_,_) ->
- let n = Kf.compare f1 f2 in
- if n = 0 then Kinstr.compare ki1 ki2 else n
- | IPReachable(kf1, ki1, ba1), IPReachable(kf2, ki2, ba2) ->
- let n = Extlib.opt_compare Kf.compare kf1 kf2 in
- if n = 0 then
- let n = Kinstr.compare ki1 ki2 in
- if n = 0 then Transitioning.Stdlib.compare ba1 ba2 else n
- else
- n
- | IPAxiom (s1,_,_,_,_), IPAxiom (s2,_,_,_,_)
- | IPAxiomatic(s1, _), IPAxiomatic(s2, _)
- | IPTypeInvariant(s1,_,_,_), IPTypeInvariant(s2,_,_,_)
- | IPLemma (s1,_,_,_,_), IPLemma (s2,_,_,_,_) ->
- Datatype.String.compare s1 s2
- | IPOther(s1,le1), IPOther(s2,le2) ->
- let s = Datatype.String.compare s1 s2 in
- if s <> 0 then s else other_loc_compare le1 le2
- | IPAllocation (f1, ki1, b1, _), IPAllocation (f2, ki2, b2, _) ->
- cmp_bhv (f1,ki1,b1) (f2,ki2,b2)
- | IPPropertyInstance (kf1, s1, _, ip1),
- IPPropertyInstance (kf2, s2, _, ip2) ->
- let c = Kernel_function.compare kf1 kf2 in
- if c <> 0 then c else
- let c = Stmt.compare s1 s2 in
- if c <> 0 then c else compare ip1 ip2
- | (IPPredicate _ | IPExtended _ | IPCodeAnnot _ | IPBehavior _ | IPComplete _ |
+ | IPDecrease {id_kf=f1; id_kinstr=ki1},
+ IPDecrease {id_kf=f2; id_kinstr=ki2} ->
+ let n = Kf.compare f1 f2 in
+ if n = 0 then Kinstr.compare ki1 ki2 else n
+ | IPReachable {ir_kf=kf1; ir_kinstr=ki1; ir_program_point=ba1},
+ IPReachable {ir_kf=kf2; ir_kinstr=ki2; ir_program_point=ba2} ->
+ let n = Extlib.opt_compare Kf.compare kf1 kf2 in
+ if n = 0 then
+ let n = Kinstr.compare ki1 ki2 in
+ if n = 0 then Transitioning.Stdlib.compare ba1 ba2 else n
+ else
+ n
+ | IPAxiom {il_name=s1}, IPAxiom {il_name=s2}
+ | IPAxiomatic {iax_name=s1}, IPAxiomatic {iax_name=s2}
+ | IPTypeInvariant {iti_name=s1}, IPTypeInvariant {iti_name=s2}
+ | IPGlobalInvariant {igi_name=s1}, IPGlobalInvariant {igi_name=s2}
+ | IPLemma {il_name=s1}, IPLemma {il_name=s2} ->
+ Datatype.String.compare s1 s2
+ | IPOther {io_name=s1;io_loc=l1}, IPOther {io_name=s2;io_loc=l2} ->
+ let s = Datatype.String.compare s1 s2 in
+ if s <> 0 then s else other_loc_compare l1 l2
+ | IPAllocation {ial_kf=f1;ial_kinstr=ki1;ial_bhv=b1},
+ IPAllocation {ial_kf=f2;ial_kinstr=ki2;ial_bhv=b2} ->
+ cmp_bhv (f1,ki1,b1) (f2,ki2,b2)
+ | IPPropertyInstance {ii_kf=kf1;ii_stmt=s1;ii_ip=ip1},
+ IPPropertyInstance {ii_kf=kf2;ii_stmt=s2;ii_ip=ip2} ->
+ let c = Kernel_function.compare kf1 kf2 in
+ if c <> 0 then c else
+ let c = Stmt.compare s1 s2 in
+ if c <> 0 then c else compare ip1 ip2
+ | (IPPredicate _ | IPExtended _ | IPCodeAnnot _ | IPBehavior _ | IPComplete _ |
IPDisjoint _ | IPAssigns _ | IPFrom _ | IPDecrease _ |
IPReachable _ | IPAxiom _ | IPAxiomatic _ | IPLemma _ |
IPOther _ | IPAllocation _ | IPPropertyInstance _ |
- IPTypeInvariant _ | IPGlobalInvariant _) as x, y ->
+ IPTypeInvariant _ | IPGlobalInvariant _) as x, y ->
let nb = function
| IPPredicate _ -> 1
| IPAssigns _ -> 2
| IPDecrease _ -> 3
| IPAxiom _ -> 4
| IPAxiomatic _ -> 5
- | IPLemma _ -> 6
+ | IPLemma _ -> 6
| IPCodeAnnot _ -> 7
| IPComplete _ -> 8
| IPDisjoint _ -> 9
| IPFrom _ -> 10
- | IPBehavior _ -> 11
- | IPReachable _ -> 12
- | IPAllocation _ -> 13
- | IPOther _ -> 14
- | IPPropertyInstance _ -> 15
- | IPTypeInvariant _ -> 16
- | IPGlobalInvariant _ -> 17
+ | IPBehavior _ -> 11
+ | IPReachable _ -> 12
+ | IPAllocation _ -> 13
+ | IPOther _ -> 14
+ | IPPropertyInstance _ -> 15
+ | IPTypeInvariant _ -> 16
+ | IPGlobalInvariant _ -> 17
| IPExtended _ -> 18
- in
- Datatype.Int.compare (nb x) (nb y)
+ in
+ Datatype.Int.compare (nb x) (nb y)
- end)
+ end)
let rec short_pretty fmt p = match p with
- | IPPredicate (_,_,_,{ ip_content = {pred_name = name :: _ }}) ->
+ | IPPredicate {ip_pred={ip_content={pred_name=name::_}}} ->
Format.pp_print_string fmt name
| IPPredicate _ -> pretty fmt p
- | IPExtended (_,{ext_name}) -> Format.pp_print_string fmt ext_name
- | IPAxiom (name,_,_,_,_) | IPLemma(name,_,_,_,_)
- | IPTypeInvariant(name,_,_,_) -> Format.pp_print_string fmt name
- | IPGlobalInvariant(name,_,_) -> Format.pp_print_string fmt name
- | IPAxiomatic (name,_) -> Format.pp_print_string fmt name
- | IPBehavior(kf,_,_,{b_name = name }) ->
+ | IPExtended {ie_ext={ext_name}} -> Format.pp_print_string fmt ext_name
+ | IPAxiom {il_name=n} | IPLemma {il_name=n}
+ | IPTypeInvariant {iti_name=n} | IPGlobalInvariant {igi_name=n}
+ | IPAxiomatic {iax_name=n} -> Format.pp_print_string fmt n
+ | IPBehavior {ib_kf; ib_bhv={b_name}} ->
Format.fprintf fmt "behavior %s in function %a"
- name Kernel_function.pretty kf
- | IPComplete (kf,_,_,_) ->
+ b_name Kernel_function.pretty ib_kf
+ | IPComplete {ic_kf} ->
Format.fprintf fmt "complete clause in function %a"
- Kernel_function.pretty kf
- | IPDisjoint (kf,_,_,_) ->
+ Kernel_function.pretty ic_kf
+ | IPDisjoint {ic_kf} ->
Format.fprintf fmt "disjoint clause in function %a"
- Kernel_function.pretty kf
- | IPCodeAnnot (_,_,{ annot_content = AAssert (_, _, { pred_name = name :: _ })}) ->
- Format.pp_print_string fmt name
- | IPCodeAnnot(_,_,{annot_content =
- AInvariant (_,_, { pred_name = name :: _ })})->
+ Kernel_function.pretty ic_kf
+ | IPCodeAnnot {ica_ca={annot_content=AAssert (_, _, {pred_name=name::_})}}
+ | IPCodeAnnot {ica_ca={annot_content=AInvariant (_, _, {pred_name=name::_})}} ->
Format.pp_print_string fmt name
| IPCodeAnnot _ -> pretty fmt p
- | IPAllocation (kf,_,_,_) ->
+ | IPAllocation {ial_kf} ->
Format.fprintf fmt "allocates/frees clause in function %a"
- Kernel_function.pretty kf
- | IPAssigns (kf,_,_,_) ->
+ Kernel_function.pretty ial_kf
+ | IPAssigns {ias_kf} ->
Format.fprintf fmt "assigns clause in function %a"
- Kernel_function.pretty kf
- | IPFrom (kf,_,_,(t,_)) ->
+ Kernel_function.pretty ias_kf
+ | IPFrom {if_kf; if_from=(t, _)} ->
Format.fprintf fmt "from clause of term %a in function %a"
- Cil_printer.pp_identified_term t Kernel_function.pretty kf
- | IPDecrease(kf,_,_,_) ->
+ Cil_printer.pp_identified_term t Kernel_function.pretty if_kf
+ | IPDecrease {id_kf} ->
Format.fprintf fmt "decrease clause in function %a"
- Kernel_function.pretty kf
- | IPPropertyInstance (kf, stmt, _, ip) ->
- Format.fprintf fmt "specialization of %a %a" short_pretty ip
- pretty_instance_location (kf, stmt)
+ Kernel_function.pretty id_kf
+ | IPPropertyInstance {ii_kf; ii_stmt; ii_ip} ->
+ Format.fprintf fmt "specialization of %a %a" short_pretty ii_ip
+ pretty_instance_location (ii_kf, ii_stmt)
| IPReachable _ | IPOther _ -> pretty fmt p
let pp_behavior_or_loop_debug fmt = function
@@ -703,110 +775,110 @@ let pp_other_loc fmt = function
let rec pretty_debug fmt = function
- | IPPredicate (pk,kf,ki,ip) ->
+ | IPPredicate {ip_kind;ip_kf;ip_kinstr;ip_pred} ->
Format.fprintf fmt "IPPredicate(%a,%a,%a,%a)"
- pp_predicate_type_debug pk
- Cil_types_debug.pp_kernel_function kf
- Cil_types_debug.pp_kinstr ki
- Cil_types_debug.pp_identified_predicate ip
- | IPExtended (el,ae) ->
+ pp_predicate_type_debug ip_kind
+ Cil_types_debug.pp_kernel_function ip_kf
+ Cil_types_debug.pp_kinstr ip_kinstr
+ Cil_types_debug.pp_identified_predicate ip_pred
+ | IPExtended {ie_ext;ie_loc} ->
Format.fprintf fmt "IPExtended(%a,%a)"
- pp_extended_loc el
- Cil_types_debug.pp_acsl_extension ae
- | IPCodeAnnot (kf, s, ca) ->
+ pp_extended_loc ie_loc
+ Cil_types_debug.pp_acsl_extension ie_ext
+ | IPCodeAnnot {ica_kf; ica_stmt; ica_ca} ->
Format.fprintf fmt "IPCodeAnnot(%a,%a,%a)"
- Cil_types_debug.pp_kernel_function kf
- Cil_types_debug.pp_stmt s
- Cil_types_debug.pp_code_annotation ca
- | IPComplete (kf, ki, a, lb) ->
+ Cil_types_debug.pp_kernel_function ica_kf
+ Cil_types_debug.pp_stmt ica_stmt
+ Cil_types_debug.pp_code_annotation ica_ca
+ | IPComplete {ic_kf; ic_kinstr; ic_active; ic_bhvs} ->
Format.fprintf fmt "IPComplete(%a,%a,%a,%a)"
- Cil_types_debug.pp_kernel_function kf
- Cil_types_debug.pp_kinstr ki
- Datatype.String.Set.pretty a
- (Cil_types_debug.pp_list Cil_types_debug.pp_string) lb
- | IPDisjoint (kf, ki, a, lb) ->
+ Cil_types_debug.pp_kernel_function ic_kf
+ Cil_types_debug.pp_kinstr ic_kinstr
+ Datatype.String.Set.pretty ic_active
+ (Cil_types_debug.pp_list Cil_types_debug.pp_string) ic_bhvs
+ | IPDisjoint {ic_kf; ic_kinstr; ic_active; ic_bhvs} ->
Format.fprintf fmt "IPDisjoint(%a,%a,%a,%a)"
- Cil_types_debug.pp_kernel_function kf
- Cil_types_debug.pp_kinstr ki
- Datatype.String.Set.pretty a
- (Cil_types_debug.pp_list Cil_types_debug.pp_string) lb
- | IPDecrease (kf, ki, oca, variant) ->
+ Cil_types_debug.pp_kernel_function ic_kf
+ Cil_types_debug.pp_kinstr ic_kinstr
+ Datatype.String.Set.pretty ic_active
+ (Cil_types_debug.pp_list Cil_types_debug.pp_string) ic_bhvs
+ | IPDecrease {id_kf; id_kinstr; id_ca; id_variant} ->
Format.fprintf fmt "IPDecrease(%a,%a,%a,%a)"
- Cil_types_debug.pp_kernel_function kf
- Cil_types_debug.pp_kinstr ki
- (Cil_types_debug.pp_option Cil_types_debug.pp_code_annotation) oca
- Cil_types_debug.pp_variant variant
- | IPAxiom (str,log_lbl_list,str_list,pred,loc) ->
+ Cil_types_debug.pp_kernel_function id_kf
+ Cil_types_debug.pp_kinstr id_kinstr
+ (Cil_types_debug.pp_option Cil_types_debug.pp_code_annotation) id_ca
+ Cil_types_debug.pp_variant id_variant
+ | IPAxiom {il_name; il_labels; il_args; il_pred; il_loc} ->
Format.fprintf fmt "IPAxiom(%a,%a,%a,%a,%a)"
- Cil_types_debug.pp_string str
- (Cil_types_debug.pp_list Cil_types_debug.pp_logic_label) log_lbl_list
- (Cil_types_debug.pp_list Cil_types_debug.pp_string) str_list
- Cil_types_debug.pp_predicate pred
- Cil_types_debug.pp_location loc
- | IPAxiomatic(str, ip_list) ->
+ Cil_types_debug.pp_string il_name
+ (Cil_types_debug.pp_list Cil_types_debug.pp_logic_label) il_labels
+ (Cil_types_debug.pp_list Cil_types_debug.pp_string) il_args
+ Cil_types_debug.pp_predicate il_pred
+ Cil_types_debug.pp_location il_loc
+ | IPAxiomatic {iax_name; iax_props} ->
Format.fprintf fmt "IPAxiomatic(%a,%a)"
- Cil_types_debug.pp_string str
- (Cil_types_debug.pp_list pretty_debug) ip_list
- | IPLemma (str,log_lbl_list,str_list,pred,loc) ->
+ Cil_types_debug.pp_string iax_name
+ (Cil_types_debug.pp_list pretty_debug) iax_props
+ | IPLemma {il_name; il_labels; il_args; il_pred; il_loc} ->
Format.fprintf fmt "IPLemma(%a,%a,%a,%a,%a)"
- Cil_types_debug.pp_string str
- (Cil_types_debug.pp_list Cil_types_debug.pp_logic_label) log_lbl_list
- (Cil_types_debug.pp_list Cil_types_debug.pp_string) str_list
- Cil_types_debug.pp_predicate pred
- Cil_types_debug.pp_location loc
- | IPTypeInvariant (str,typ,pred,loc) ->
+ Cil_types_debug.pp_string il_name
+ (Cil_types_debug.pp_list Cil_types_debug.pp_logic_label) il_labels
+ (Cil_types_debug.pp_list Cil_types_debug.pp_string) il_args
+ Cil_types_debug.pp_predicate il_pred
+ Cil_types_debug.pp_location il_loc
+ | IPTypeInvariant {iti_name; iti_type; iti_pred; iti_loc} ->
Format.fprintf fmt "IPTypeInvariant(%a,%a,%a,%a)"
- Cil_types_debug.pp_string str
- Cil_types_debug.pp_typ typ
- Cil_types_debug.pp_predicate pred
- Cil_types_debug.pp_location loc
- | IPGlobalInvariant (str,pred,loc) ->
+ Cil_types_debug.pp_string iti_name
+ Cil_types_debug.pp_typ iti_type
+ Cil_types_debug.pp_predicate iti_pred
+ Cil_types_debug.pp_location iti_loc
+ | IPGlobalInvariant {igi_name; igi_pred; igi_loc} ->
Format.fprintf fmt "IPGlobalInvariant(%a,%a,%a)"
- Cil_types_debug.pp_string str
- Cil_types_debug.pp_predicate pred
- Cil_types_debug.pp_location loc
- | IPAllocation (kf, ki, bol, iterm_pair_list) ->
+ Cil_types_debug.pp_string igi_name
+ Cil_types_debug.pp_predicate igi_pred
+ Cil_types_debug.pp_location igi_loc
+ | IPAllocation {ial_kf; ial_kinstr; ial_bhv; ial_allocs} ->
Format.fprintf fmt "IPAllocation(%a,%a,%a,%a)"
- Cil_types_debug.pp_kernel_function kf
- Cil_types_debug.pp_kinstr ki
- pp_behavior_or_loop_debug bol
+ Cil_types_debug.pp_kernel_function ial_kf
+ Cil_types_debug.pp_kinstr ial_kinstr
+ pp_behavior_or_loop_debug ial_bhv
(Cil_types_debug.pp_pair
(Cil_types_debug.pp_list Cil_types_debug.pp_identified_term)
(Cil_types_debug.pp_list Cil_types_debug.pp_identified_term)
- ) iterm_pair_list
- | IPAssigns (kf, ki, bol, from_list) ->
+ ) ial_allocs
+ | IPAssigns {ias_kf; ias_kinstr; ias_bhv; ias_froms} ->
Format.fprintf fmt "IPAssigns(%a,%a,%a,%a)"
- Cil_types_debug.pp_kernel_function kf
- Cil_types_debug.pp_kinstr ki
- pp_behavior_or_loop_debug bol
- (Cil_types_debug.pp_list Cil_types_debug.pp_from) from_list
- | IPFrom (kf, ki, bol, from) ->
+ Cil_types_debug.pp_kernel_function ias_kf
+ Cil_types_debug.pp_kinstr ias_kinstr
+ pp_behavior_or_loop_debug ias_bhv
+ (Cil_types_debug.pp_list Cil_types_debug.pp_from) ias_froms
+ | IPFrom {if_kf; if_kinstr; if_bhv; if_from} ->
Format.fprintf fmt "IPFrom(%a,%a,%a,%a)"
- Cil_types_debug.pp_kernel_function kf
- Cil_types_debug.pp_kinstr ki
- pp_behavior_or_loop_debug bol
- Cil_types_debug.pp_from from
- | IPReachable (okf, ki, pp) ->
+ Cil_types_debug.pp_kernel_function if_kf
+ Cil_types_debug.pp_kinstr if_kinstr
+ pp_behavior_or_loop_debug if_bhv
+ Cil_types_debug.pp_from if_from
+ | IPReachable {ir_kf; ir_kinstr; ir_program_point} ->
Format.fprintf fmt "IPReachable(%a,%a,%a)"
- (Cil_types_debug.pp_option Cil_types_debug.pp_kernel_function) okf
- Cil_types_debug.pp_kinstr ki
- pp_program_point pp
- | IPBehavior(kf, ki, a, fb) ->
+ (Cil_types_debug.pp_option Cil_types_debug.pp_kernel_function) ir_kf
+ Cil_types_debug.pp_kinstr ir_kinstr
+ pp_program_point ir_program_point
+ | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
Format.fprintf fmt "IPBehavior(%a,%a,%a,%a)"
- Cil_types_debug.pp_kernel_function kf
- Cil_types_debug.pp_kinstr ki
- Datatype.String.Set.pretty a
- Cil_types_debug.pp_funbehavior fb
- | IPPropertyInstance (kf, s, oip, ip) ->
+ Cil_types_debug.pp_kernel_function ib_kf
+ Cil_types_debug.pp_kinstr ib_kinstr
+ Datatype.String.Set.pretty ib_active
+ Cil_types_debug.pp_funbehavior ib_bhv
+ | IPPropertyInstance {ii_kf; ii_stmt; ii_pred; ii_ip} ->
Format.fprintf fmt "IPPropertyInstance(%a,%a,%a,%a)"
- Cil_types_debug.pp_kernel_function kf
- Cil_types_debug.pp_stmt s
- (Cil_types_debug.pp_option Cil_types_debug.pp_identified_predicate) oip
- pretty_debug ip
- | IPOther(s,ol) ->
+ Cil_types_debug.pp_kernel_function ii_kf
+ Cil_types_debug.pp_stmt ii_stmt
+ (Cil_types_debug.pp_option Cil_types_debug.pp_identified_predicate)
+ ii_pred pretty_debug ii_ip
+ | IPOther {io_name; io_loc} ->
Format.fprintf fmt "IPOther(%a,%a)"
- Cil_types_debug.pp_string s
- pp_other_loc ol
+ Cil_types_debug.pp_string io_name
+ pp_other_loc io_loc
(* -------------------------------------------------------------------------- *)
(* --- Legacy Property Names --- *)
@@ -819,17 +891,17 @@ struct
module NamesTbl =
State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
(struct
- let name = "PropertyNames"
- let dependencies = [ ]
- let size = 97
- end)
+ let name = "PropertyNames"
+ let dependencies = [ ]
+ let size = 97
+ end)
module IndexTbl =
State_builder.Hashtbl(Hashtbl)(Datatype.String)
(struct
- let name = "PropertyIndex"
- let dependencies = [ Ast.self; NamesTbl.self; Globals.Functions.self ]
- let size = 97
- end)
+ let name = "PropertyIndex"
+ let dependencies = [ Ast.self; NamesTbl.self; Globals.Functions.self ]
+ let size = 97
+ end)
let self = IndexTbl.self
@@ -837,26 +909,26 @@ struct
let ident_names names =
List.filter (function "" -> true
- | _ as n -> '\"' <> (String.get n 0) ) names
+ | _ as n -> '\"' <> (String.get n 0) ) names
let pp_names fmt l =
let l = ident_names l in
match l with [] -> ()
- | _ -> Format.fprintf fmt "_%a"
- (Pretty_utils.pp_list ~sep:"_" Format.pp_print_string) l
+ | _ -> Format.fprintf fmt "_%a"
+ (Pretty_utils.pp_list ~sep:"_" Format.pp_print_string) l
let pp_code_annot_names fmt ca =
match ca.annot_content with
- | AAssert(for_bhv,_,named_pred) | AInvariant(for_bhv,_,named_pred) ->
- let pp_for_bhv fmt l =
- match l with
- | [] -> ()
- | _ -> Format.fprintf fmt "_for_%a"
- (Pretty_utils.pp_list ~sep:"_" Format.pp_print_string) l
- in
- Format.fprintf fmt "%a%a" pp_names named_pred.pred_name pp_for_bhv for_bhv
- | AVariant(term, _) -> pp_names fmt term.term_name
- | _ -> () (* TODO : add some more names ? *)
+ | AAssert(for_bhv,_,named_pred) | AInvariant(for_bhv,_,named_pred) ->
+ let pp_for_bhv fmt l =
+ match l with
+ | [] -> ()
+ | _ -> Format.fprintf fmt "_for_%a"
+ (Pretty_utils.pp_list ~sep:"_" Format.pp_print_string) l
+ in
+ Format.fprintf fmt "%a%a" pp_names named_pred.pred_name pp_for_bhv for_bhv
+ | AVariant(term, _) -> pp_names fmt term.term_name
+ | _ -> () (* TODO : add some more names ? *)
let behavior_prefix b =
if Cil.is_default_behavior b then ""
@@ -894,76 +966,78 @@ struct
| PKEnsures (b, tk) -> (behavior_prefix b) ^ string_of_termination_kind tk
| PKTerminates -> "term"
in
- (ki_prefix ki) ^ name
+ (ki_prefix ki) ^ name
let active_prefix fmt a =
let print_one a = Format.fprintf fmt "_%s" a in
Datatype.String.Set.iter print_one a
let rec id_prop_txt p = match p with
- | IPPredicate (pk,kf,ki,idp) ->
- Format.asprintf "%s%s%a"
- (kf_prefix kf) (predicate_kind_txt pk ki)
- pp_names idp.ip_content.pred_name
- | IPExtended (le,{ext_name}) ->
+ | IPPredicate {ip_kind=pk;ip_kf=kf;ip_kinstr=ki;ip_pred=idp} ->
+ Format.asprintf "%s%s%a"
+ (kf_prefix kf) (predicate_kind_txt pk ki)
+ pp_names idp.ip_content.pred_name
+ | IPExtended {ie_ext={ext_name};ie_loc=le} ->
Format.asprintf "%sextended%a" (extended_loc_prefix le) pp_names [ext_name]
- | IPCodeAnnot (kf,_, ca) ->
- let name = match ca.annot_content with
- | AAssert (_, Assert, _) -> "assert"
- | AAssert (_, Check, _) -> "check"
- | AInvariant (_,true,_) -> "loop_inv"
- | AInvariant _ -> "inv"
- | APragma _ -> "pragma"
- | AStmtSpec _ -> "contract"
- | AAssigns _ -> "assigns"
- | AVariant _ -> "variant"
- | AAllocation _ -> "allocates"
- | AExtended(_,_,{ext_name}) -> ext_name
- in Format.asprintf "%s%s%a" (kf_prefix kf) name pp_code_annot_names ca
- | IPComplete (kf, ki, a, lb) ->
- Format.asprintf "%s%s%acomplete%a"
- (kf_prefix kf) (ki_prefix ki) active_prefix a pp_names lb
- | IPDisjoint (kf, ki, a, lb) ->
- Format.asprintf "%s%s%adisjoint%a"
- (kf_prefix kf) (ki_prefix ki) active_prefix a pp_names lb
- | IPDecrease (kf,_,None, variant) -> (kf_prefix kf) ^ "decr" ^ (variant_suffix variant)
- | IPDecrease (kf,_,_,variant) -> (kf_prefix kf) ^ "loop_term" ^ (variant_suffix variant)
- | IPAxiom (name,_,_,named_pred,_) ->
- Format.asprintf "axiom_%s%a" name pp_names named_pred.pred_name
- | IPAxiomatic(name, _) -> "axiomatic_" ^ name
- | IPLemma (name,_,_,named_pred,_) ->
- Format.asprintf "lemma_%s%a" name pp_names named_pred.pred_name
- | IPTypeInvariant (name,_,named_pred,_) ->
+ | IPCodeAnnot {ica_kf=kf; ica_ca=ca} ->
+ let name = match ca.annot_content with
+ | AAssert (_, Assert, _) -> "assert"
+ | AAssert (_, Check, _) -> "check"
+ | AInvariant (_,true,_) -> "loop_inv"
+ | AInvariant _ -> "inv"
+ | APragma _ -> "pragma"
+ | AStmtSpec _ -> "contract"
+ | AAssigns _ -> "assigns"
+ | AVariant _ -> "variant"
+ | AAllocation _ -> "allocates"
+ | AExtended(_,_,{ext_name}) -> ext_name
+ in Format.asprintf "%s%s%a" (kf_prefix kf) name pp_code_annot_names ca
+ | IPComplete {ic_kf=kf; ic_kinstr=ki; ic_active=a; ic_bhvs=lb} ->
+ Format.asprintf "%s%s%acomplete%a"
+ (kf_prefix kf) (ki_prefix ki) active_prefix a pp_names lb
+ | IPDisjoint {ic_kf=kf; ic_kinstr=ki; ic_active=a; ic_bhvs=lb} ->
+ Format.asprintf "%s%s%adisjoint%a"
+ (kf_prefix kf) (ki_prefix ki) active_prefix a pp_names lb
+ | IPDecrease {id_kf=kf; id_ca=None; id_variant=variant} ->
+ (kf_prefix kf) ^ "decr" ^ (variant_suffix variant)
+ | IPDecrease {id_kf=kf; id_variant=variant} ->
+ (kf_prefix kf) ^ "loop_term" ^ (variant_suffix variant)
+ | IPAxiom {il_name=name; il_pred} ->
+ Format.asprintf "axiom_%s%a" name pp_names il_pred.pred_name
+ | IPAxiomatic {iax_name} -> "axiomatic_" ^ iax_name
+ | IPLemma {il_name=name; il_pred} ->
+ Format.asprintf "lemma_%s%a" name pp_names il_pred.pred_name
+ | IPTypeInvariant {iti_name; iti_pred} ->
Format.asprintf "type_invariant_%s%a"
- name pp_names named_pred.pred_name
- | IPGlobalInvariant (name,named_pred,_) ->
+ iti_name pp_names iti_pred.pred_name
+ | IPGlobalInvariant {igi_name; igi_pred} ->
Format.asprintf "global_invariant_%s%a"
- name pp_names named_pred.pred_name
- | IPAllocation (kf, ki, (Id_contract (a,b)), _) ->
+ igi_name pp_names igi_pred.pred_name
+ | IPAllocation {ial_kf=kf; ial_kinstr=ki; ial_bhv=Id_contract (a,b)} ->
Format.asprintf "%s%s%a%salloc"
(kf_prefix kf) (ki_prefix ki) active_prefix a (behavior_prefix b)
- | IPAllocation (kf, Kstmt _s, (Id_loop ca), _) ->
+ | IPAllocation {ial_kf=kf; ial_kinstr=Kstmt _; ial_bhv=Id_loop ca} ->
Format.asprintf "%sloop_alloc%a"
(kf_prefix kf) pp_code_annot_names ca
| IPAllocation _ -> assert false
- | IPAssigns (kf, ki, (Id_contract (a,b)), _) ->
+ | IPAssigns {ias_kf=kf; ias_kinstr=ki; ias_bhv=Id_contract (a,b)} ->
Format.asprintf "%s%s%a%sassign"
(kf_prefix kf) (ki_prefix ki) active_prefix a (behavior_prefix b)
- | IPAssigns (kf, Kstmt _s, (Id_loop ca), _) ->
+ | IPAssigns {ias_kf=kf; ias_kinstr=Kstmt _; ias_bhv=Id_loop ca} ->
Format.asprintf "%sloop_assign%a"
(kf_prefix kf) pp_code_annot_names ca
| IPAssigns _ -> assert false
- | IPFrom (_, _, _, (out,_)) ->
- "from_id_"^(string_of_int (out.it_id))
+ | IPFrom {if_from=(out,_)} ->
+ "from_id_"^(string_of_int (out.it_id))
| IPReachable _ -> "reachable_stmt"
- | IPBehavior(kf, ki, a, b) ->
+ | IPBehavior {ib_kf=kf; ib_kinstr=ki; ib_active=a; ib_bhv=b} ->
Format.asprintf "%s%s%a%s"
(kf_prefix kf) (ki_prefix ki) active_prefix a b.b_name
- | IPPropertyInstance (kf, stmt, _, ip) ->
+ | IPPropertyInstance {ii_kf=kf; ii_stmt=stmt; ii_ip=ip} ->
Format.asprintf "specialization_%s_at_%t" (id_prop_txt ip)
(fun fmt ->
Format.fprintf fmt "%a_stmt_%d" Kernel_function.pretty kf stmt.sid)
- | IPOther(s,le) -> other_loc_prefix le ^ s
+ | IPOther {io_name; io_loc} -> other_loc_prefix io_loc ^ io_name
(** function used to normalize basename *)
let normalize_basename s =
@@ -982,15 +1056,15 @@ struct
(** returns the name that should be returned by the function [get_prop_name_id] if the given property has [name] as basename. That name is reserved so that [get_prop_name_id prop] can never return an identical name. *)
let reserve_name_id basename =
let basename = normalize_basename basename in
- try
- let speed_up_start = NamesTbl.find basename in
- (* this basename is already reserved *)
- let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
- in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
- unique_name
- with Not_found -> (* first time that basename is reserved *)
- NamesTbl.add basename 2 ;
- basename
+ try
+ let speed_up_start = NamesTbl.find basename in
+ (* this basename is already reserved *)
+ let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
+ in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
+ unique_name
+ with Not_found -> (* first time that basename is reserved *)
+ NamesTbl.add basename 2 ;
+ basename
(** returns the basename of the property. *)
let get_prop_basename ip = normalize_basename (id_prop_txt ip)
@@ -1002,8 +1076,8 @@ struct
with Not_found -> (* first time we are asking for a name for that [ip] *)
let basename = get_prop_basename ip in
let unique_name = reserve_name_id basename in
- IndexTbl.add ip unique_name ;
- unique_name
+ IndexTbl.add ip unique_name ;
+ unique_name
end
@@ -1043,108 +1117,104 @@ struct
let rec parts_of_property ip : part list =
match ip with
- | IPBehavior(kf,Kglobal,_,bhv) ->
- [ K kf ; B bhv ]
- | IPBehavior(kf,Kstmt s,_,bhv) ->
- [ K kf ; B bhv ; S s ]
+ | IPBehavior {ib_kf; ib_kinstr=Kglobal; ib_bhv} ->
+ [ K ib_kf ; B ib_bhv ]
+ | IPBehavior {ib_kf; ib_kinstr=Kstmt s; ib_bhv} ->
+ [ K ib_kf ; B ib_bhv ; S s]
- | IPPredicate (PKAssumes bhv,kf,_,ip) ->
+ | IPPredicate {ip_kind=PKAssumes bhv; ip_kf=kf; ip_pred=ip} ->
[ K kf ; B bhv ; A "assumes" ; I ip ]
- | IPPredicate (PKRequires bhv,kf,_,ip) ->
+ | IPPredicate {ip_kind=PKRequires bhv; ip_kf=kf; ip_pred=ip} ->
[ K kf ; B bhv ; A "requires" ; I ip ]
- | IPPredicate (PKEnsures(bhv,Normal),kf,_,ip) ->
+ | IPPredicate {ip_kind=PKEnsures (bhv, Normal); ip_kf=kf; ip_pred=ip} ->
[ K kf ; B bhv ; A "ensures" ; I ip ]
- | IPPredicate (PKEnsures(bhv,Exits),kf,_,ip) ->
+ | IPPredicate {ip_kind=PKEnsures (bhv, Exits); ip_kf=kf; ip_pred=ip} ->
[ K kf ; B bhv ; A "exits" ; I ip ]
- | IPPredicate (PKEnsures(bhv,Breaks),kf,_,ip) ->
+ | IPPredicate {ip_kind=PKEnsures (bhv, Breaks); ip_kf=kf; ip_pred=ip} ->
[ K kf ; B bhv ; A "breaks" ; I ip ]
- | IPPredicate (PKEnsures(bhv,Continues),kf,_,ip) ->
+ | IPPredicate {ip_kind=PKEnsures (bhv, Continues); ip_kf=kf; ip_pred=ip} ->
[ K kf ; B bhv ; A "continues" ; I ip ]
- | IPPredicate (PKEnsures(bhv,Returns),kf,_,ip) ->
+ | IPPredicate {ip_kind=PKEnsures (bhv, Returns); ip_kf=kf; ip_pred=ip} ->
[ K kf ; B bhv ; A "returns" ; I ip ]
- | IPPredicate (PKTerminates,kf,_,ip) ->
+ | IPPredicate {ip_kind=PKTerminates; ip_kf=kf; ip_pred=ip} ->
[ K kf ; A "terminates" ; I ip ]
- | IPAllocation(kf,_,Id_contract(_,bhv),_) ->
+ | IPAllocation {ial_kf=kf; ial_bhv=Id_contract (_, bhv)} ->
[ K kf ; B bhv ; A "allocates" ]
- | IPAllocation(kf,_,Id_loop _,_) ->
+ | IPAllocation {ial_kf=kf; ial_bhv=Id_loop _} ->
[ K kf ; A "loop_allocates" ]
- | IPAssigns(kf,_,Id_contract(_,bhv),_) ->
+ | IPAssigns {ias_kf=kf; ias_bhv=Id_contract (_, bhv)} ->
[ K kf ; B bhv ; A "assigns" ]
-
- | IPAssigns(kf,_,Id_loop _,_) ->
+ | IPAssigns {ias_kf=kf; ias_bhv=Id_loop _} ->
[ K kf ; A "loop_assigns" ]
- | IPFrom(kf,_,Id_contract(_,bhv),_) ->
+ | IPFrom {if_kf=kf; if_bhv=Id_contract (_, bhv)} ->
[ K kf ; B bhv ; A "assigns_from" ]
-
- | IPFrom(kf,_,Id_loop _,_) ->
+ | IPFrom {if_kf=kf; if_bhv=Id_loop _} ->
[ K kf ; A "loop_assigns_from" ]
- | IPDecrease (kf,_,None,_) ->
+ | IPDecrease {id_kf=kf; id_ca=None} ->
[ K kf ; A "variant" ]
-
- | IPDecrease (kf,_,Some _,_) ->
+ | IPDecrease {id_kf=kf; id_ca=Some _} ->
[ K kf ; A "loop_variant" ]
- | IPCodeAnnot (kf,stmt, { annot_content = AStmtSpec _ } ) ->
+ | IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca={annot_content=AStmtSpec _}} ->
[ K kf ; A "contract" ; S stmt ]
-
- | IPCodeAnnot (kf,stmt, { annot_content = APragma _ } ) ->
+ | IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca={annot_content=APragma _}} ->
[ K kf ; A "pragma" ; S stmt ]
-
- | IPCodeAnnot (kf,stmt, { annot_content = AExtended(_,_,{ext_name}) } ) ->
+ | IPCodeAnnot {ica_kf=kf; ica_stmt=stmt;
+ ica_ca={annot_content=AExtended (_, _, {ext_name})}} ->
[ K kf ; A ext_name ; S stmt ]
-
- | IPCodeAnnot (kf,_, { annot_content = AAssert(_,Assert,p) } ) ->
+ | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssert (_, Assert,p)}} ->
[K kf ; A "assert" ; P p ]
- | IPCodeAnnot (kf,_, { annot_content = AAssert(_,Check,p) } ) ->
+ | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssert (_, Check,p)}} ->
[K kf ; A "check" ; P p ]
- | IPCodeAnnot (kf,_, { annot_content = AInvariant(_,true,p) } ) ->
+ | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_, true, p)}} ->
[K kf ; A "loop_invariant" ; P p ]
- | IPCodeAnnot (kf,_, { annot_content = AInvariant(_,false,p) } ) ->
+ | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_, false, p)}} ->
[K kf ; A "invariant" ; P p ]
- | IPCodeAnnot (kf,_, { annot_content = AVariant(e,_) } ) ->
+ | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AVariant (e, _)}} ->
[K kf ; A "loop_variant" ; T e ]
- | IPCodeAnnot (kf,_, { annot_content = AAssigns _ } ) ->
+ | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssigns _}} ->
[K kf ; A "loop_assigns" ]
- | IPCodeAnnot (kf,_, { annot_content = AAllocation _ } ) ->
+ | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAllocation _}} ->
[K kf ; A "loop_allocates" ]
- | IPComplete (kf,_,_,cs) ->
+ | IPComplete {ic_kf=kf; ic_bhvs=cs} ->
(K kf :: A "complete" :: List.map (fun a -> A a) cs)
- | IPDisjoint(kf,_,_,cs) ->
+ | IPDisjoint {ic_kf=kf; ic_bhvs=cs} ->
(K kf :: A "disjoint" :: List.map (fun a -> A a) cs)
- | IPReachable (None, _, _) -> []
- | IPReachable (Some kf,Kglobal,Before) ->
+ | IPReachable {ir_kf=None} -> []
+ | IPReachable {ir_kf=Some kf; ir_kinstr=Kglobal; ir_program_point=Before} ->
[ K kf ; A "reachable" ]
- | IPReachable (Some kf,Kglobal,After) ->
+ | IPReachable {ir_kf=Some kf; ir_kinstr=Kglobal; ir_program_point=After} ->
[ K kf ; A "reachable_post" ]
- | IPReachable (Some kf,Kstmt s,Before) ->
+ | IPReachable {ir_kf=Some kf; ir_kinstr=Kstmt s; ir_program_point=Before} ->
[ K kf ; A "reachable" ; S s ]
- | IPReachable (Some kf,Kstmt s,After) ->
+ | IPReachable {ir_kf=Some kf; ir_kinstr=Kstmt s; ir_program_point=After} ->
[ K kf ; A "reachable_after" ; S s ]
| IPAxiomatic _
| IPAxiom _ -> []
- | IPLemma(name,_,_,p,_) ->
+ | IPLemma {il_name=name; il_pred=p} ->
[ A "lemma" ; A name ; P p ]
- | IPTypeInvariant(name,_,_,_)
- | IPGlobalInvariant(name,_,_) ->
+ | IPTypeInvariant {iti_name=name}
+ | IPGlobalInvariant {igi_name=name} ->
[ A "invariant" ; A name ]
- | IPOther(name,OLGlob _) -> [ A name ]
- | IPOther(name,OLContract kf) -> [ K kf ; A name ]
- | IPOther(name,OLStmt(kf,s)) -> [ K kf ; A name ; S s ]
+ | IPOther {io_name=name; io_loc=OLGlob _} -> [ A name ]
+ | IPOther {io_name=name; io_loc=OLContract kf} -> [ K kf ; A name ]
+ | IPOther {io_name=name; io_loc=OLStmt (kf, s)} -> [ K kf ; A name ; S s ]
- | IPExtended(ELGlob,{ext_name}) -> [ A ext_name ]
- | IPExtended(ELContract(kf),{ext_name}) -> [ K kf ; A ext_name ]
- | IPExtended(ELStmt(kf,s),{ext_name}) -> [ K kf ; A ext_name ; S s ]
+ | IPExtended {ie_loc=ELGlob; ie_ext={ext_name}} -> [A ext_name]
+ | IPExtended {ie_loc=ELContract kf; ie_ext={ext_name}} -> [K kf ; A ext_name]
+ | IPExtended {ie_loc=ELStmt (kf,s); ie_ext={ext_name}} ->
+ [K kf ; A ext_name ; S s]
- | IPPropertyInstance (_, _, _, ip) -> parts_of_property ip
+ | IPPropertyInstance {ii_ip} -> parts_of_property ii_ip
let get_prop_basename ?truncate ip =
let buffer =
@@ -1159,7 +1229,7 @@ struct
module NamesTbl =
State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
(struct
- let name = "Property.Names.NamesTbl"
+ let name = "Property.Names.NamesTbl"
let dependencies = [ ]
let size = 97
end)
@@ -1168,9 +1238,9 @@ struct
module IndexTbl = (* indexed by Property *)
State_builder.Hashtbl(Hashtbl)(Datatype.String)
(struct
- let name = "Property.Names.IndexTbl"
- let dependencies = [ Ast.self; NamesTbl.self; Globals.Functions.self ]
- let size = 97
+ let name = "Property.Names.IndexTbl"
+ let dependencies = [ Ast.self; NamesTbl.self; Globals.Functions.self ]
+ let size = 97
end)
let self = IndexTbl.self
@@ -1200,60 +1270,64 @@ end
(* --- Smart Constructors --- *)
(* -------------------------------------------------------------------------- *)
-let ip_other s le = IPOther(s,le)
+let ip_other io_name io_loc = IPOther {io_name; io_loc}
-let ip_reachable_stmt kf ki = IPReachable(Some kf, Kstmt ki, Before)
+let ip_reachable_stmt kf ki =
+ IPReachable {ir_kf=Some kf; ir_kinstr=Kstmt ki; ir_program_point=Before}
let ip_reachable_ppt p =
- let kf = get_kf p in
- let ki = get_kinstr p in
- let ba = match p with
- | IPPredicate((PKRequires _ | PKAssumes _ | PKTerminates), _, _, _)
+ let ir_kf = get_kf p in
+ let ir_kinstr = get_kinstr p in
+ let ir_program_point = match p with
+ | IPPredicate {ip_kind=(PKRequires _ | PKAssumes _ | PKTerminates)}
| IPAxiom _ | IPAxiomatic _ | IPLemma _ | IPComplete _
| IPDisjoint _ | IPCodeAnnot _ | IPAllocation _
| IPDecrease _ | IPPropertyInstance _ | IPOther _
| IPTypeInvariant _ | IPGlobalInvariant _
-> Before
- | IPPredicate(PKEnsures _, _, _, _) | IPAssigns _ | IPFrom _
+ | IPPredicate _ | IPAssigns _ | IPFrom _
| IPExtended _
| IPBehavior _
-> After
| IPReachable _ -> Kernel.fatal "IPReachable(IPReachable _) is not possible"
in
- IPReachable(kf, ki, ba)
+ IPReachable {ir_kf; ir_kinstr; ir_program_point}
-let ip_of_ensures kf st b (k,p) = IPPredicate (PKEnsures(b,k),kf,st,p)
+let ip_of_ensures ip_kf ip_kinstr b (k,ip_pred) =
+ IPPredicate {ip_kind=PKEnsures (b, k); ip_kf; ip_kinstr; ip_pred}
-let ip_of_extended le p = IPExtended (le, p)
+let ip_of_extended ie_loc ie_ext = IPExtended {ie_loc; ie_ext}
let ip_ensures_of_behavior kf st b =
List.map (ip_of_ensures kf st b) b.b_post_cond
-let ip_of_allocation kf st loc = function
+let ip_of_allocation ial_kf ial_kinstr ial_bhv = function
| FreeAllocAny -> None
- | FreeAlloc(f,a) -> Some (IPAllocation (kf,st,loc,(f,a)))
+ | FreeAlloc(f,a) ->
+ Some (IPAllocation {ial_kf;ial_kinstr;ial_bhv; ial_allocs=(f,a)})
let ip_allocation_of_behavior kf st ~active b =
let a = Datatype.String.Set.of_list active in
ip_of_allocation kf st (Id_contract (a,b)) b.b_allocation
-let ip_of_assigns kf st loc = function
+let ip_of_assigns ias_kf ias_kinstr ias_bhv = function
| WritesAny -> None
| Writes [(a,_)] when Logic_utils.is_result a.it_content ->
(* We're only assigning the result (with dependencies), but no
global variables, this amounts to \nothing.
*)
- Some (IPAssigns (kf, st, loc, []))
- | Writes a -> Some (IPAssigns (kf,st,loc,a))
+ Some (IPAssigns {ias_kf; ias_kinstr; ias_bhv; ias_froms=[]})
+ | Writes ias_froms ->
+ Some (IPAssigns {ias_kf; ias_kinstr; ias_bhv; ias_froms})
let ip_assigns_of_behavior kf st ~active b =
let a = Datatype.String.Set.of_list active in
ip_of_assigns kf st (Id_contract (a,b)) b.b_assigns
-let ip_of_from kf st loc from =
- match snd from with
+let ip_of_from if_kf if_kinstr if_bhv if_from =
+ match snd if_from with
| FromAny -> None
- | From _ -> Some (IPFrom (kf,st, loc, from))
+ | From _ -> Some (IPFrom {if_kf;if_kinstr;if_bhv;if_from})
let ip_from_of_behavior kf st ~active b =
match b.b_assigns with
@@ -1297,16 +1371,18 @@ let ip_post_cond_of_behavior kf st ~active b =
@ ip_from_of_behavior kf st active b
@ (Extlib.list_of_opt (ip_allocation_of_behavior kf st ~active b))
-let ip_of_behavior kf s ~active b =
- let a = Datatype.String.Set.of_list active in
- IPBehavior(kf, s, a, b)
+let ip_of_behavior ib_kf ib_kinstr ~active ib_bhv =
+ let ib_active = Datatype.String.Set.of_list active in
+ IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv}
-let ip_of_requires kf st b p = IPPredicate (PKRequires b,kf,st,p)
+let ip_of_requires ip_kf ip_kinstr b ip_pred =
+ IPPredicate {ip_kind=PKRequires b; ip_kf; ip_kinstr; ip_pred}
let ip_requires_of_behavior kf st b =
List.map (ip_of_requires kf st b) b.b_requires
-let ip_of_assumes kf st b p = IPPredicate (PKAssumes b,kf,st,p)
+let ip_of_assumes ip_kf ip_kinstr b ip_pred =
+ IPPredicate {ip_kind=PKAssumes b; ip_kf; ip_kinstr; ip_pred}
let ip_assumes_of_behavior kf st b =
List.map (ip_of_assumes kf st b) b.b_assumes
@@ -1318,25 +1394,29 @@ let ip_all_of_behavior kf st ~active b =
@ ip_post_cond_of_behavior kf st ~active b
@ List.map (ip_of_extended (e_loc_of_stmt kf st)) b.b_extended
-let ip_of_complete kf st ~active bhvs =
- let a = Datatype.String.Set.of_list active in IPComplete(kf,st,a,bhvs)
+let ip_of_complete ic_kf ic_kinstr ~active ic_bhvs =
+ let ic_active = Datatype.String.Set.of_list active in
+ IPComplete {ic_kf; ic_kinstr; ic_active; ic_bhvs}
let ip_complete_of_spec kf st ~active s =
List.map (ip_of_complete kf st ~active) s.spec_complete_behaviors
-let ip_of_disjoint kf st ~active bhvs =
- let a = Datatype.String.Set.of_list active in IPDisjoint(kf,st,a,bhvs)
+let ip_of_disjoint ic_kf ic_kinstr ~active ic_bhvs =
+ let ic_active = Datatype.String.Set.of_list active in
+ IPDisjoint {ic_kf; ic_kinstr; ic_active; ic_bhvs}
let ip_disjoint_of_spec kf st ~active s =
List.map (ip_of_disjoint kf st ~active) s.spec_disjoint_behaviors
-let ip_of_terminates kf st p = IPPredicate(PKTerminates,kf,st,p)
+let ip_of_terminates ip_kf ip_kinstr ip_pred =
+ IPPredicate {ip_kind = PKTerminates; ip_kf; ip_kinstr; ip_pred}
let ip_terminates_of_spec kf st s = match s.spec_terminates with
| None -> None
| Some p -> Some (ip_of_terminates kf st p)
-let ip_of_decreases kf st d = IPDecrease(kf,st,None,d)
+let ip_of_decreases id_kf id_kinstr id_variant =
+ IPDecrease {id_kf; id_kinstr; id_ca = None; id_variant}
let ip_decreases_of_spec kf st s =
Extlib.opt_map (ip_of_decreases kf st) s.spec_variant
@@ -1357,15 +1437,16 @@ let ip_lemma s = IPLemma s
let ip_type_invariant s = IPTypeInvariant s
let ip_global_invariant s = IPGlobalInvariant s
-let ip_property_instance kf stmt ipred iprop =
- IPPropertyInstance (kf, stmt, ipred, iprop)
+let ip_property_instance ii_kf ii_stmt ii_pred ii_ip =
+ IPPropertyInstance {ii_kf; ii_stmt; ii_pred; ii_ip}
let ip_of_code_annot kf stmt ca =
let ki = Kstmt stmt in
match ca.annot_content with
- | AAssert _ | AInvariant _ -> [ IPCodeAnnot(kf, stmt, ca) ]
+ | AAssert _ | AInvariant _ -> [ IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca=ca} ]
| AStmtSpec (active,s) -> ip_of_spec kf ki active s
- | AVariant t -> [ IPDecrease (kf,ki,(Some ca),t) ]
+ | AVariant t ->
+ [ IPDecrease {id_kf=kf;id_kinstr=ki;id_ca=Some ca; id_variant=t}]
| AAllocation _ ->
Extlib.list_of_opt (ip_allocation_of_code_annot kf ki ca)
@ ip_from_of_code_annot kf ki ca
@@ -1373,10 +1454,12 @@ let ip_of_code_annot kf stmt ca =
Extlib.list_of_opt (ip_assigns_of_code_annot kf ki ca)
@ ip_from_of_code_annot kf ki ca
| APragma p when Logic_utils.is_property_pragma p ->
- [ IPCodeAnnot (kf,stmt,ca) ]
+ [ IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca=ca} ]
| APragma _ -> []
| AExtended(_,_,ext) ->
- if ext.ext_has_status then [IPExtended(ELStmt(kf,stmt),ext)] else []
+ if ext.ext_has_status then
+ [IPExtended {ie_loc=ELStmt(kf,stmt); ie_ext=ext}]
+ else []
let ip_of_code_annot_single kf stmt ca = match ip_of_code_annot kf stmt ca with
| [] ->
@@ -1400,31 +1483,34 @@ let ip_of_code_annot_single kf stmt ca = match ip_of_code_annot kf stmt ca with
let ip_of_global_annotation a =
let once = true in
let rec aux acc = function
- | Daxiomatic(name, l, _, _) ->
- let ppts = List.fold_left aux [] l in
- IPAxiomatic(name, ppts) :: (ppts @ acc)
- | Dlemma(name, true, a, b, c, _, d) -> ip_axiom (name,a,b,c,d) :: acc
- | Dlemma(name, false, a, b, c, _, d) -> ip_lemma (name,a,b,c,d) :: acc
- | Dinvariant(l, loc) ->
- let pred = match l.l_body with
+ | Daxiomatic(iax_name, l, _, _) ->
+ let iax_props = List.fold_left aux [] l in
+ IPAxiomatic {iax_name; iax_props} :: (iax_props @ acc)
+ | Dlemma(il_name, true, il_labels, il_args, il_pred, _, il_loc) ->
+ ip_axiom {il_name; il_labels; il_args; il_pred; il_loc} :: acc
+ | Dlemma(il_name, false, il_labels, il_args, il_pred, _, il_loc) ->
+ ip_lemma {il_name; il_labels; il_args; il_pred; il_loc} :: acc
+ | Dinvariant(l, igi_loc) ->
+ let igi_pred = match l.l_body with
| LBpred p -> p
| _ -> assert false
in
- IPGlobalInvariant(l.l_var_info.lv_name,pred,loc) :: acc
- | Dtype_annot(l, loc) ->
+ IPGlobalInvariant {igi_name=l.l_var_info.lv_name; igi_pred; igi_loc} :: acc
+ | Dtype_annot(l, iti_loc) ->
let parameter = match l.l_profile with
| h :: [] -> h
| _ -> assert false
in
- let ty = match parameter.lv_type with
+ let iti_type = match parameter.lv_type with
| Ctype x -> x
| _ -> assert false
in
- let pred = match l.l_body with
+ let iti_pred = match l.l_body with
| LBpred p -> p
| _ -> assert false
in
- IPTypeInvariant(l.l_var_info.lv_name,ty,pred,loc) :: acc
+ IPTypeInvariant {iti_name=l.l_var_info.lv_name;
+ iti_type; iti_pred; iti_loc} :: acc
| Dcustom_annot(_c, _n, _, _) ->
(* TODO *)
Kernel.warning ~once "ignoring status of custom annotation";
@@ -1432,7 +1518,8 @@ let ip_of_global_annotation a =
| Dmodel_annot _ | Dfun_or_pred _ | Dvolatile _ | Dtype _ ->
(* no associated status for these annotations *)
acc
- | Dextended(ext,_,_) -> IPExtended (ELGlob, ext) :: acc
+ | Dextended(ie_ext,_,_) ->
+ IPExtended {ie_loc = ELGlob; ie_ext} :: acc
in
aux [] a
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 8b91f7fde54..6a74d626876 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -49,35 +49,60 @@ type behavior_or_loop = (* private *)
(** Only AAssert, AInvariant, or APragma. Other code annotations are
dispatched as identified_property of their own. *)
-type identified_code_annotation = kernel_function * stmt * code_annotation
-
-type identified_assigns =
- kernel_function * kinstr * behavior_or_loop * from list
-
-type identified_allocation =
- kernel_function * kinstr * behavior_or_loop * (identified_term list * identified_term list)
-
-type identified_from =
- kernel_function
- * kinstr
- * behavior_or_loop
- * from
-
-type identified_decrease =
- kernel_function * kinstr * code_annotation option * variant
+type identified_code_annotation = {
+ ica_kf : kernel_function;
+ ica_stmt : stmt;
+ ica_ca : code_annotation
+}
+
+type identified_assigns = {
+ ias_kf : kernel_function;
+ ias_kinstr : kinstr;
+ ias_bhv : behavior_or_loop;
+ ias_froms : from list
+}
+
+type identified_allocation = {
+ ial_kf : kernel_function;
+ ial_kinstr : kinstr;
+ ial_bhv : behavior_or_loop;
+ ial_allocs : identified_term list * identified_term list
+}
+
+type identified_from = {
+ if_kf : kernel_function;
+ if_kinstr : kinstr;
+ if_bhv : behavior_or_loop;
+ if_from : from
+}
+
+type identified_decrease = {
+ id_kf : kernel_function;
+ id_kinstr : kinstr;
+ id_ca : code_annotation option;
+ id_variant : variant
+}
(** code_annotation is None for decreases and [Some { AVariant }] for
loop variant. *)
-type identified_behavior =
- kernel_function * kinstr * Datatype.String.Set.t * funbehavior
- (** for statement contract, the set of parent behavior for which the
- contract is active is part of its identification. If the set is empty,
- the contract is active for all parent behaviors.
- *)
+type identified_behavior = {
+ ib_kf : kernel_function;
+ ib_kinstr : kinstr;
+ ib_active : Datatype.String.Set.t;
+ ib_bhv : funbehavior
+}
+(** for statement contract, the set of parent behavior for which the
+ contract is active is part of its identification. If the set is empty,
+ the contract is active for all parent behaviors.
+*)
-type identified_complete =
- kernel_function * kinstr * Datatype.String.Set.t * string list
- (** Same as for {!identified_behavior}. *)
+type identified_complete = {
+ ic_kf : kernel_function;
+ ic_kinstr : kinstr;
+ ic_active : Datatype.String.Set.t;
+ ic_bhvs : string list
+}
+(** Same as for {!identified_behavior}. *)
type identified_disjoint = identified_complete
@@ -87,12 +112,20 @@ type predicate_kind = private
| PKEnsures of funbehavior * termination_kind
| PKTerminates
-type identified_predicate =
- predicate_kind * kernel_function * kinstr * Cil_types.identified_predicate
+type identified_predicate = {
+ ip_kind : predicate_kind;
+ ip_kf : kernel_function;
+ ip_kinstr : kinstr;
+ ip_pred : Cil_types.identified_predicate
+}
type program_point = Before | After
-type identified_reachable = kernel_function option * kinstr * program_point
+type identified_reachable = {
+ ir_kf : kernel_function option;
+ ir_kinstr : kinstr;
+ ir_program_point : program_point
+}
(** [None, Kglobal] --> global property
[None, Some ki] --> impossible
[Some kf, Kglobal] --> property of a function without code
@@ -109,25 +142,53 @@ type extended_loc =
| ELStmt of kernel_function * stmt
| ELGlob
-type identified_extended = extended_loc * Cil_types.acsl_extension
+type identified_extended = {
+ ie_loc : extended_loc;
+ ie_ext : Cil_types.acsl_extension
+}
-and identified_axiomatic = string * identified_property list
+and identified_axiomatic = {
+ iax_name : string;
+ iax_props : identified_property list
+}
-and identified_lemma =
- string * logic_label list * string list * predicate * location
+and identified_lemma = {
+ il_name : string;
+ il_labels : logic_label list;
+ il_args : string list;
+ il_pred : predicate;
+ il_loc : location
+}
and identified_axiom = identified_lemma
(** Specialization of a property at a given point, identified by a statement
and a function, along with the predicate transposed at this point (if it
can be) and the original property. *)
-and identified_instance =
- kernel_function * stmt * Cil_types.identified_predicate option
- * identified_property
-
-and identified_type_invariant = string * typ * predicate * location
-
-and identified_global_invariant = string * predicate * location
+and identified_instance = {
+ ii_kf : kernel_function;
+ ii_stmt : stmt;
+ ii_pred : Cil_types.identified_predicate option;
+ ii_ip : identified_property
+}
+
+and identified_type_invariant = {
+ iti_name : string;
+ iti_type : typ;
+ iti_pred : predicate;
+ iti_loc : location
+}
+
+and identified_global_invariant = {
+ igi_name : string;
+ igi_pred : predicate;
+ igi_loc : location
+}
+
+and identified_other = {
+ io_name : string;
+ io_loc : other_loc
+}
and identified_property = private
| IPPredicate of identified_predicate
@@ -147,7 +208,7 @@ and identified_property = private
| IPPropertyInstance of identified_instance
| IPTypeInvariant of identified_type_invariant
| IPGlobalInvariant of identified_global_invariant
- | IPOther of string * other_loc
+ | IPOther of identified_other
include Datatype.S_with_collections with type t = identified_property
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 4842bcdeb30..76b09d36f78 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -355,61 +355,69 @@ That is forbidden (kernel invariant broken)."
register_as_kernel_logical_consequence ppt
(* the functions below and this one MUST be synchronized *)
-and register_as_kernel_logical_consequence ppt = match ppt with
- | Property.IPAxiom _
- | Property.IPPredicate(Property.PKAssumes _, _, _, _) ->
+and register_as_kernel_logical_consequence ppt =
+ let open Property in match ppt with
+ | IPAxiom _
+ | IPPredicate {ip_kind = PKAssumes _} ->
(* always valid, but must be verifiable by the end-user,
see [is_not_verifiable_but_valid] *)
()
- | Property.IPAxiomatic(_, l) -> logical_consequence Emitter.kernel ppt l
- | Property.IPBehavior(kf, ki, active, b) ->
- let active = Datatype.String.Set.elements active in
+ | IPAxiomatic {iax_props} -> logical_consequence Emitter.kernel ppt iax_props
+ | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
+ let active = Datatype.String.Set.elements ib_active in
(* logical consequence of its postconditions *)
logical_consequence
- Emitter.kernel ppt (Property.ip_post_cond_of_behavior kf ki active b)
- | Property.IPReachable(None, Cil_types.Kglobal, Property.Before) ->
+ Emitter.kernel ppt (ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv)
+ | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
+ ir_program_point = Before} ->
(* valid: global properties are always reachable *)
emit_valid ppt
- | Property.IPReachable(None, Cil_types.Kglobal, Property.After) ->
+ | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
+ ir_program_point = After} ->
assert false
- | Property.IPReachable(None, Cil_types.Kstmt _, _) ->
+ | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kstmt _} ->
Kernel.fatal "reachability of a stmt without function"
- | Property.IPReachable(Some kf, Cil_types.Kglobal, Property.Before) ->
+ | IPReachable {ir_kf = Some kf; ir_kinstr = Cil_types.Kglobal;
+ ir_program_point = Before} ->
let f = kf.Cil_types.fundec in
if Ast_info.Function.get_name f = Kernel.MainFunction.get_plain_string ()
(* main is always reachable *)
then emit_valid ppt
- | Property.IPOther _ | Property.IPReachable _
- | Property.IPExtended _
- | Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
- | Property.IPDisjoint _ | Property.IPAssigns _ | Property.IPFrom _
- | Property.IPAllocation _ | Property.IPDecrease _ | Property.IPLemma _
- | Property.IPPropertyInstance _
- | Property.IPTypeInvariant _ | Property.IPGlobalInvariant _ ->
+ | IPOther _ | IPReachable _
+ | IPExtended _
+ | IPPredicate _ | IPCodeAnnot _ | IPComplete _
+ | IPDisjoint _ | IPAssigns _ | IPFrom _
+ | IPAllocation _ | IPDecrease _ | IPLemma _
+ | IPPropertyInstance _
+ | IPTypeInvariant _ | IPGlobalInvariant _ ->
()
(* the functions above and below MUST be synchronized *)
-and is_kernel_logical_consequence ppt = match ppt with
- | Property.IPPredicate(Property.PKAssumes _, _, _, _)
- | Property.IPBehavior(_, _, _, _)
- | Property.IPReachable(None, Cil_types.Kglobal, Property.Before) ->
+and is_kernel_logical_consequence ppt =
+ let open Property in match ppt with
+ | IPPredicate {ip_kind = PKAssumes _}
+ | IPBehavior _
+ | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
+ ir_program_point = Before} ->
true
- | Property.IPReachable(None, Cil_types.Kglobal, Property.After) ->
+ | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
+ ir_program_point = After} ->
assert false
- | Property.IPReachable(None, Cil_types.Kstmt _, _) ->
+ | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kstmt _} ->
Kernel.fatal "reachability of a stmt without function"
- | Property.IPReachable(Some kf, Cil_types.Kglobal, Property.Before) ->
+ | IPReachable {ir_kf = Some kf; ir_kinstr = Cil_types.Kglobal;
+ ir_program_point = Before} ->
let f = kf.Cil_types.fundec in (* main is always reachable *)
Ast_info.Function.get_name f = Kernel.MainFunction.get_plain_string ()
- | Property.IPAxiom _
- | Property.IPExtended _
- | Property.IPAxiomatic _
- | Property.IPOther _ | Property.IPReachable _
- | Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
- | Property.IPDisjoint _ | Property.IPAssigns _ | Property.IPFrom _
- | Property.IPAllocation _ | Property.IPDecrease _ | Property.IPLemma _
- | Property.IPPropertyInstance _
- | Property.IPTypeInvariant _ | Property.IPGlobalInvariant _ ->
+ | IPAxiom _
+ | IPExtended _
+ | IPAxiomatic _
+ | IPOther _ | IPReachable _
+ | IPPredicate _ | IPCodeAnnot _ | IPComplete _
+ | IPDisjoint _ | IPAssigns _ | IPFrom _
+ | IPAllocation _ | IPDecrease _ | IPLemma _
+ | IPPropertyInstance _
+ | IPTypeInvariant _ | IPGlobalInvariant _ ->
false
and unsafe_emit_and_get e ~hyps ~auto ppt ?(distinct=false) s =
@@ -533,20 +541,20 @@ let () =
register_as_kernel_logical_consequence
let emit_and_get e ~hyps ppt ?distinct s =
- begin match ppt with
- | Property.IPBehavior _ | Property.IPAxiom _ | Property.IPAxiomatic _
- | Property.IPPredicate (Property.PKAssumes _, _, _, _) ->
+ let open Property in begin match ppt with
+ | IPBehavior _ | IPAxiom _ | IPAxiomatic _
+ | IPPredicate {ip_kind = PKAssumes _} ->
Kernel.fatal
"only the kernel should set the status of property %a"
- Property.pretty
+ pretty
ppt
- | Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
- | Property.IPDisjoint _ | Property.IPAssigns _ | Property.IPFrom _
- | Property.IPDecrease _ | Property.IPLemma _ | Property.IPReachable _
- | Property.IPAllocation _ | Property.IPOther _
- | Property.IPPropertyInstance _
- | Property.IPExtended _
- | Property.IPTypeInvariant _ | Property.IPGlobalInvariant _ -> ()
+ | IPPredicate _ | IPCodeAnnot _ | IPComplete _
+ | IPDisjoint _ | IPAssigns _ | IPFrom _
+ | IPDecrease _ | IPLemma _ | IPReachable _
+ | IPAllocation _ | IPOther _
+ | IPPropertyInstance _
+ | IPExtended _
+ | IPTypeInvariant _ | IPGlobalInvariant _ -> ()
end;
unsafe_emit_and_get e ~hyps ~auto:false ppt ?distinct s
@@ -653,11 +661,10 @@ let is_not_verifiable_but_valid ppt status = match status with
false
else
(* postconditions of functions without code are not verifiable *)
- match ppt with
- | Property.IPPredicate
- ((Property.PKEnsures _ | Property.PKTerminates), _, _, _)
- | Property.IPAssigns _ | Property.IPAllocation _
- | Property.IPFrom _ -> true
+ let open Property in match ppt with
+ | IPPredicate {ip_kind = PKEnsures _ | PKTerminates}
+ | IPAssigns _ | IPAllocation _
+ | IPFrom _ -> true
| _ -> false)
| Best((True | False_if_reachable | False_and_reachable | Dont_know), _)
| Inconsistent _ ->
diff --git a/src/kernel_services/ast_data/statuses_by_call.ml b/src/kernel_services/ast_data/statuses_by_call.ml
index e5506a00785..b9b69bd47ad 100644
--- a/src/kernel_services/ast_data/statuses_by_call.ml
+++ b/src/kernel_services/ast_data/statuses_by_call.ml
@@ -192,7 +192,7 @@ module PreCondAt =
let rec transpose_precondition stmt pid kf funcexp args =
let formals = Kernel_function.get_formals kf in
let ip = match pid with
- | Property.IPPredicate (_, _, _, ip) -> ip
+ | Property.(IPPredicate {ip_pred}) -> ip_pred
| _ -> assert false
in
let ip = transpose_pred_at_callsite ~formals ~concretes:args ip in
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 3f4baed5afc..89aa33d86d8 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -215,28 +215,28 @@ let pp_capitalize fmt s =
let pp_acsl_extension fmt {ext_name} = pp_capitalize fmt ext_name
let rec pp_prop kfopt kiopt kloc fmt = function
- | IPAxiom (s,_,_,_,_) -> Format.fprintf fmt "Axiom '%s'" s
- | IPLemma (s,_,_,_,_) -> Format.fprintf fmt "Lemma '%s'" s
- | IPTypeInvariant (s,_,_,_) -> Format.fprintf fmt "Type invariant '%s'" s
- | IPGlobalInvariant (s,_,_) -> Format.fprintf fmt "Global invariant '%s'" s
- | IPAxiomatic (s,_) -> Format.fprintf fmt "Axiomatic '%s'" s
- | IPOther(s,le) ->
+ | IPAxiom {il_name=s} -> Format.fprintf fmt "Axiom '%s'" s
+ | IPLemma {il_name=s} -> Format.fprintf fmt "Lemma '%s'" s
+ | IPTypeInvariant {iti_name=s} -> Format.fprintf fmt "Type invariant '%s'" s
+ | IPGlobalInvariant {igi_name=s} -> Format.fprintf fmt "Global invariant '%s'" s
+ | IPAxiomatic {iax_name=s} -> Format.fprintf fmt "Axiomatic '%s'" s
+ | IPOther {io_name=s;io_loc=le} ->
Format.fprintf fmt "%a%a" pp_capitalize s (pp_other_loc kfopt kiopt kloc) le
- | IPPredicate(kind,kf,Kglobal,idpred) ->
+ | IPPredicate {ip_kind; ip_kf; ip_kinstr=Kglobal; ip_pred} ->
Format.fprintf fmt "%a%a%a"
- pp_predicate kind
- (pp_idpred kloc) idpred
- (pp_context kfopt) (Some kf)
- | IPPredicate(kind,_,ki,idpred) ->
+ pp_predicate ip_kind
+ (pp_idpred kloc) ip_pred
+ (pp_context kfopt) (Some ip_kf)
+ | IPPredicate {ip_kind; ip_kinstr; ip_pred} ->
Format.fprintf fmt "%a%a%a"
- pp_predicate kind
- (pp_idpred kloc) idpred
- (pp_kinstr kloc) ki
- | IPExtended(le,ext) ->
+ pp_predicate ip_kind
+ (pp_idpred kloc) ip_pred
+ (pp_kinstr kloc) ip_kinstr
+ | IPExtended {ie_loc=le; ie_ext=ext} ->
Format.fprintf fmt "%a%a"
pp_acsl_extension ext
(pp_extended_loc kfopt kiopt kloc) (ext.ext_loc,le)
- | IPBehavior(_,ki, active, bhv) ->
+ | IPBehavior {ib_kinstr=ki; ib_active=active; ib_bhv=bhv} ->
if Cil.is_default_behavior bhv then
Format.fprintf fmt "Default behavior%a%a"
(pp_opt kiopt (pp_kinstr kloc)) ki (pp_opt kiopt pp_active) active
@@ -244,100 +244,104 @@ let rec pp_prop kfopt kiopt kloc fmt = function
Format.fprintf fmt "Behavior '%s'%a"
bhv.b_name
(pp_opt kiopt (pp_kinstr kloc)) ki
- | IPComplete(_,ki,active, bs) ->
+ | IPComplete {ic_kinstr; ic_active; ic_bhvs} ->
Format.fprintf fmt "Complete behaviors%a%a%a"
- pp_bhvs bs
- (pp_opt kiopt (pp_kinstr kloc)) ki (pp_opt kiopt pp_active) active
- | IPDisjoint(_,ki,active, bs) ->
+ pp_bhvs ic_bhvs
+ (pp_opt kiopt (pp_kinstr kloc)) ic_kinstr (pp_opt kiopt pp_active) ic_active
+ | IPDisjoint {ic_kinstr; ic_active; ic_bhvs} ->
Format.fprintf fmt "Disjoint behaviors%a%a%a"
- pp_bhvs bs
- (pp_opt kiopt (pp_kinstr kloc)) ki
- (pp_opt kiopt pp_active) active
- | IPCodeAnnot(_,_,{annot_content=AAssert(bs,Assert,np)}) ->
+ pp_bhvs ic_bhvs
+ (pp_opt kiopt (pp_kinstr kloc)) ic_kinstr
+ (pp_opt kiopt pp_active) ic_active
+ | IPCodeAnnot {ica_ca={annot_content=AAssert(bs,Assert,np)}} ->
Format.fprintf fmt "Assertion%a%a%a"
pp_for bs
pp_named np
(pp_kloc kloc) np.pred_loc
- | IPCodeAnnot(_,_,{annot_content=AAssert(bs,Check,np)}) ->
+ | IPCodeAnnot {ica_ca={annot_content=AAssert(bs,Check,np)}} ->
Format.fprintf fmt "Check%a%a%a"
pp_for bs
pp_named np
(pp_kloc kloc) np.pred_loc
- | IPCodeAnnot(_,_,{annot_content=AInvariant(bs,_,np)}) ->
+ | IPCodeAnnot {ica_ca={annot_content=AInvariant(bs,_,np)}} ->
Format.fprintf fmt "Invariant%a%a%a"
pp_for bs
pp_named np
(pp_kloc kloc) np.pred_loc
- | IPCodeAnnot(_,stmt,{annot_content=AExtended(bs,_,{ext_name})}) ->
+ | IPCodeAnnot {ica_ca={annot_content=AExtended(bs,_,{ext_name})};ica_stmt} ->
Format.fprintf fmt "%a%a %a"
- pp_capitalize ext_name pp_for bs (pp_stmt kloc) stmt
- | IPCodeAnnot(_,stmt,_) ->
- Format.fprintf fmt "Annotation %a" (pp_stmt kloc) stmt
- | IPAllocation(kf,Kglobal,Id_contract (_,bhv),(frees,allocates)) ->
+ pp_capitalize ext_name pp_for bs (pp_stmt kloc) ica_stmt
+ | IPCodeAnnot {ica_stmt} ->
+ Format.fprintf fmt "Annotation %a" (pp_stmt kloc) ica_stmt
+ | IPAllocation {ial_kf; ial_kinstr=Kglobal; ial_bhv=Id_contract (_,bhv);
+ ial_allocs = (frees, allocates)} ->
Format.fprintf fmt "Frees/Allocates%a %a/%a %a"
pp_bhv bhv
(pp_allocation kloc) frees
(pp_allocation kloc) allocates
- (pp_context kfopt) (Some kf)
- | IPAssigns(kf,Kglobal,Id_contract(_, bhv),region) ->
+ (pp_context kfopt) (Some ial_kf)
+ | IPAssigns {ias_kf; ias_kinstr=Kglobal; ias_bhv=Id_contract (_,bhv);
+ ias_froms = region} ->
Format.fprintf fmt "Assigns%a %a%a"
pp_bhv bhv
(pp_region kloc) region
- (pp_context kfopt) (Some kf)
- | IPFrom (kf,Kglobal,Id_contract(_,bhv),depend) ->
+ (pp_context kfopt) (Some ias_kf)
+ | IPFrom {if_kf; if_kinstr=Kglobal; if_bhv=Id_contract (_,bhv);
+ if_from = depend} ->
Format.fprintf fmt "Froms%a %a%a"
pp_bhv bhv
(pp_region kloc) [depend]
- (pp_context kfopt) (Some kf)
- | IPAllocation(_,ki,Id_contract (active,bhv),(frees,allocates)) ->
+ (pp_context kfopt) (Some if_kf)
+ | IPAllocation {ial_kinstr; ial_bhv=Id_contract (active,bhv);
+ ial_allocs = (frees, allocates)} ->
Format.fprintf fmt "Frees/Allocates%a %a/%a %a%a"
pp_bhv bhv
(pp_allocation kloc) frees
(pp_allocation kloc) allocates
- (pp_opt kiopt (pp_kinstr kloc)) ki
+ (pp_opt kiopt (pp_kinstr kloc)) ial_kinstr
(pp_opt kiopt pp_active) active
- | IPAssigns(_,ki,Id_contract (active,bhv),region) ->
+ | IPAssigns {ias_kinstr; ias_bhv=Id_contract (active,bhv); ias_froms = region} ->
Format.fprintf fmt "Assigns%a %a%a%a"
pp_bhv bhv
(pp_region kloc) region
- (pp_opt kiopt (pp_kinstr kloc)) ki
+ (pp_opt kiopt (pp_kinstr kloc)) ias_kinstr
(pp_opt kiopt pp_active) active
- | IPFrom (_,ki,Id_contract (active,bhv),depend) ->
+ | IPFrom {if_kinstr; if_bhv=Id_contract (active,bhv); if_from = depend} ->
Format.fprintf fmt "Froms%a %a%a%a"
pp_bhv bhv
(pp_region kloc) [depend]
- (pp_opt kiopt (pp_kinstr kloc)) ki
+ (pp_opt kiopt (pp_kinstr kloc)) if_kinstr
(pp_opt kiopt pp_active) active
- | IPAllocation(_,_,Id_loop _,(frees,allocates)) ->
+ | IPAllocation {ial_bhv=Id_loop _; ial_allocs = (frees, allocates)} ->
Format.fprintf fmt "Loop frees%a Loop allocates%a"
(pp_allocation kloc) frees
(pp_allocation kloc) allocates
- | IPAssigns(_,_,Id_loop _,region) ->
+ | IPAssigns {ias_bhv = Id_loop _; ias_froms = region} ->
Format.fprintf fmt "Loop assigns %a" (pp_region kloc) region
- | IPFrom(_,_,Id_loop _,depend) ->
+ | IPFrom {if_bhv = Id_loop _; if_from = depend} ->
Format.fprintf fmt "Loop froms %a" (pp_region kloc) [depend]
- | IPDecrease(_,Kglobal,_,_) ->
+ | IPDecrease {id_kinstr = Kglobal} ->
Format.fprintf fmt "Recursion variant"
- | IPDecrease(_,Kstmt stmt,_,_) ->
+ | IPDecrease {id_kinstr = Kstmt stmt} ->
Format.fprintf fmt "Loop variant at %a" (pp_stmt kloc) stmt
- | IPReachable (None, Kglobal, Before) ->
+ | IPReachable {ir_kf=None; ir_kinstr=Kglobal; ir_program_point = Before} ->
(* print "Unreachable": it seems that it is what the user want to see *)
Format.fprintf fmt "Unreachable entry point"
- | IPReachable (None, Kglobal, After)
- | IPReachable (None, Kstmt _, _) -> assert false
- | IPReachable (Some _, Kstmt stmt, ba) ->
+ | IPReachable {ir_kf=None; ir_kinstr=Kglobal; ir_program_point = After}
+ | IPReachable {ir_kf=None; ir_kinstr=Kstmt _} -> assert false
+ | IPReachable {ir_kf=Some _; ir_kinstr=Kstmt stmt; ir_program_point=ba} ->
(* print "Unreachable": it seems that it is what the user want to see *)
Format.fprintf fmt "Unreachable %a%s"
(pp_stmt kloc) stmt
(match ba with Before -> "" | After -> " (after it)")
- | IPReachable (Some kf, Kglobal, _) ->
+ | IPReachable {ir_kf=Some kf; ir_kinstr=Kglobal} ->
(* print "Unreachable": it seems that it is what the user want to see *)
Format.fprintf fmt "Unreachable %a" Kernel_function.pretty kf
- | IPPropertyInstance (kf, stmt, _, ip) ->
+ | IPPropertyInstance {ii_kf; ii_stmt; ii_ip} ->
Format.fprintf fmt "Instance of '%a'%a%a@."
- (pp_prop kfopt kiopt kloc) ip
- (pp_context kfopt) (Some kf)
- (pp_opt kiopt (pp_kinstr kloc)) (Kstmt stmt)
+ (pp_prop kfopt kiopt kloc) ii_ip
+ (pp_context kfopt) (Some ii_kf)
+ (pp_opt kiopt (pp_kinstr kloc)) (Kstmt ii_stmt)
@@ -375,18 +379,19 @@ let property_kind_and_node property =
let default kind = Some (kind, to_string Property.pretty property) in
let open Property in
match property with
- | IPCodeAnnot (_kf, _stmt, code_annot) -> code_annot_kind_and_node code_annot
- | IPPredicate (kind, _kf, _, p) ->
- let kind = match kind with
+ | IPCodeAnnot {ica_ca} -> code_annot_kind_and_node ica_ca
+ | IPPredicate {ip_kind; ip_pred} ->
+ let kind = match ip_kind with
| PKRequires _ -> "precondition"
| PKAssumes _ -> "behavior assumption"
| PKEnsures _ -> "postcondition"
| PKTerminates -> "termination clause"
in
- Some (kind, to_string Printer.pp_identified_predicate p)
- | IPPropertyInstance (_, _, _, IPPredicate (PKRequires _, kf', Kglobal, p)) ->
- let kind = "precondition of " ^ Kernel_function.get_name kf' in
- Some (kind, to_string Printer.pp_identified_predicate p)
+ Some (kind, to_string Printer.pp_identified_predicate ip_pred)
+ | IPPropertyInstance {ii_ip=IPPredicate {ip_kind=PKRequires _; ip_kf;
+ ip_kinstr=Kglobal; ip_pred}} ->
+ let kind = "precondition of " ^ Kernel_function.get_name ip_kf in
+ Some (kind, to_string Printer.pp_identified_predicate ip_pred)
| IPAssigns _ -> default "assigns clause"
| IPFrom _ -> default "from clause"
| IPComplete _ -> default "complete behaviors"
@@ -478,30 +483,40 @@ let loop_order = function
| Id_loop _ -> []
let rec ip_order = function
- | IPAxiomatic(a,_) -> [I 0;S a]
- | IPAxiom(a,_,_,_,_) | IPLemma(a,_,_,_,_) -> [I 1;S a]
- | IPOther(s,OLContract kf) -> [I 3;F kf;S s]
- | IPOther(s,OLStmt (kf, stmt)) -> [I 4;F kf;K (Kstmt stmt);S s]
- | IPOther (s, OLGlob _) -> [I 5; S s]
- | IPBehavior(kf,ki,a,bhv) -> [I 6;F kf;K ki;B bhv; A a]
- | IPComplete(kf,ki,a,bs) -> [I 7;F kf;K ki; A a] @ for_order 0 bs
- | IPDisjoint(kf,ki,a, bs) -> [I 8;F kf;K ki; A a] @ for_order 0 bs
- | IPPredicate(kind,kf,ki,_) -> [I 9;F kf;K ki] @ kind_order kind
- | IPCodeAnnot(kf,st,a) -> [I 10;F kf;K(Kstmt st)] @ annot_order a
- | IPAllocation(kf,ki,ib,_) -> [I 11;F kf;K ki] @ loop_order ib
- | IPAssigns(kf,ki,ib,_) -> [I 12;F kf;K ki] @ loop_order ib
- | IPFrom (kf,ki,ib,_) -> [I 13;F kf;K ki] @ loop_order ib
- | IPDecrease(kf,ki,None,_) -> [I 14;F kf;K ki]
- | IPDecrease(kf,ki,Some a,_) -> [I 15;F kf;K ki] @ annot_order a
- | IPReachable(None,_,_) -> [I 16]
- | IPReachable(Some kf,ki,_) -> [I 17;F kf;K ki]
- | IPPropertyInstance (kf, s, _, ip) -> [I 18; F kf; K (Kstmt s)] @ ip_order ip
- | IPTypeInvariant(a,_,_,_) -> [I 19; S a]
- | IPGlobalInvariant(a,_,_) -> [I 20; S a]
- | IPExtended(ELContract kf, {ext_name}) -> [I 21;F kf; S ext_name]
- | IPExtended(ELStmt (kf, stmt), {ext_name}) ->
+ | IPAxiomatic {iax_name=a} -> [I 0;S a]
+ | IPAxiom {il_name=a} | IPLemma {il_name=a} -> [I 1;S a]
+ | IPOther {io_name=s;io_loc=OLContract kf} -> [I 3;F kf;S s]
+ | IPOther {io_name=s;io_loc=OLStmt (kf, stmt)} -> [I 4;F kf;K (Kstmt stmt);S s]
+ | IPOther {io_name=s;io_loc=OLGlob _} -> [I 5; S s]
+ | IPBehavior {ib_kf;ib_kinstr;ib_active;ib_bhv} ->
+ [I 6;F ib_kf;K ib_kinstr;B ib_bhv; A ib_active]
+ | IPComplete {ic_kf;ic_kinstr;ic_active;ic_bhvs} ->
+ [I 7;F ic_kf;K ic_kinstr; A ic_active] @ for_order 0 ic_bhvs
+ | IPDisjoint {ic_kf;ic_kinstr;ic_active;ic_bhvs} ->
+ [I 8;F ic_kf;K ic_kinstr; A ic_active] @ for_order 0 ic_bhvs
+ | IPPredicate {ip_kind;ip_kf;ip_kinstr} ->
+ [I 9;F ip_kf;K ip_kinstr] @ kind_order ip_kind
+ | IPCodeAnnot {ica_kf;ica_stmt;ica_ca} ->
+ [I 10;F ica_kf;K(Kstmt ica_stmt)] @ annot_order ica_ca
+ | IPAllocation {ial_kf;ial_kinstr;ial_bhv} ->
+ [I 11;F ial_kf;K ial_kinstr] @ loop_order ial_bhv
+ | IPAssigns {ias_kf; ias_kinstr; ias_bhv} ->
+ [I 12;F ias_kf;K ias_kinstr] @ loop_order ias_bhv
+ | IPFrom {if_kf;if_kinstr;if_bhv} ->
+ [I 13;F if_kf;K if_kinstr] @ loop_order if_bhv
+ | IPDecrease {id_kf;id_kinstr;id_ca=None} -> [I 14;F id_kf;K id_kinstr]
+ | IPDecrease {id_kf;id_kinstr;id_ca=Some a} ->
+ [I 15;F id_kf;K id_kinstr] @ annot_order a
+ | IPReachable {ir_kf=None} -> [I 16]
+ | IPReachable {ir_kf=Some kf; ir_kinstr} -> [I 17;F kf;K ir_kinstr]
+ | IPPropertyInstance {ii_kf; ii_stmt; ii_ip} ->
+ [I 18; F ii_kf; K (Kstmt ii_stmt)] @ ip_order ii_ip
+ | IPTypeInvariant {iti_name=a} -> [I 19; S a]
+ | IPGlobalInvariant {igi_name=a} -> [I 20; S a]
+ | IPExtended {ie_loc=ELContract kf;ie_ext={ext_name}} -> [I 21;F kf; S ext_name]
+ | IPExtended {ie_loc=ELStmt (kf, stmt);ie_ext={ext_name}} ->
[ I 22; F kf; K (Kstmt stmt); S ext_name]
- | IPExtended(ELGlob, {ext_name}) -> [ I 23; S ext_name]
+ | IPExtended {ie_loc=ELGlob; ie_ext={ext_name}} -> [ I 23; S ext_name]
let pp_compare p q = cmp (ip_order p) (ip_order q)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 83eeb184084..ebf393201e4 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -221,13 +221,13 @@ struct
| Instr (Call _)
| Instr (Local_init (_, ConsInit _, _)) ->
let extract_instance_predicate = function
- | Property.IPPropertyInstance (_kf, _stmt, pred, _prop) -> pred
+ | Property.(IPPropertyInstance {ii_pred}) -> ii_pred
(* Other cases should not happen, unless a plugin has replaced call
preconditions. In this case, print nothing but do not crash. *)
| _ -> raise Not_found
in
let extract_predicate = function
- | Property.IPPredicate (_, _, _, p) -> p
+ | Property.(IPPredicate {ip_pred}) -> ip_pred
| _ -> assert false
in
(* Functons called at this point *)
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index d74c850f40c..49111c839e0 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -419,109 +419,109 @@ let to_do_on_select
(formal_or_local vi) pp_defining_fun vi pp_decl vi.vdecl
in
if button = 1 then begin
- match selected with
+ let open Property in match selected with
| PStmtStart _ -> ()
| PStmt (kf, stmt) ->
current_statement_msg (Some kf) (Kstmt stmt);
print_code_annotations main_ui kf stmt;
print_call_preconditions main_ui stmt;
- | PIP (Property.IPCodeAnnot (kf,stmt,ca) as ip) ->
+ | PIP (IPCodeAnnot {ica_kf;ica_stmt;ica_ca} as ip) ->
current_statement_msg
- ?loc:(Cil_datatype.Code_annotation.loc ca) (Some kf) (Kstmt stmt);
+ ?loc:(Cil_datatype.Code_annotation.loc ica_ca)
+ (Some ica_kf) (Kstmt ica_stmt);
if main_ui#show_ids then
- main_ui#pretty_information "Code annotation id: %d@." ca.annot_id;
+ main_ui#pretty_information "Code annotation id: %d@." ica_ca.annot_id;
main_ui#pretty_information "%a@." pretty_predicate_status ip
- | PIP(Property.IPAllocation _ as ip) ->
+ | PIP(IPAllocation _ as ip) ->
main_ui#pretty_information "This is an allocation clause@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPAssigns _ as ip) ->
+ main_ui#view_original (location ip)
+ | PIP(IPAssigns _ as ip) ->
main_ui#pretty_information "This is an assigns clause@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPFrom _ as ip) ->
+ main_ui#view_original (location ip)
+ | PIP(IPFrom _ as ip) ->
main_ui#pretty_information "This is a from clause@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPPredicate (Property.PKRequires _,_,_,_) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPPredicate {ip_kind = PKRequires _} as ip) ->
main_ui#pretty_information "This is a requires clause.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPExtended(_,{ext_name}) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPExtended {ie_ext={ext_name}} as ip) ->
main_ui#pretty_information "This clause is a %s extension.@.%a@."
ext_name pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPPredicate (Property.PKTerminates,_,_,_) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPPredicate {ip_kind = PKTerminates} as ip) ->
main_ui#pretty_information "This is a terminates clause.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPPredicate (Property.PKEnsures (_,Normal),_,_,_) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPPredicate {ip_kind = PKEnsures (_,Normal)} as ip) ->
main_ui#pretty_information "This is an ensures clause.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPPredicate (Property.PKEnsures (_,Exits),_,_,_) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPPredicate {ip_kind = PKEnsures (_,Exits)} as ip) ->
main_ui#pretty_information "This is an exits clause.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPPredicate (Property.PKEnsures (_,Returns),_,_,_) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPPredicate {ip_kind = PKEnsures (_,Returns)} as ip) ->
main_ui#pretty_information "This is a returns clause.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPPredicate (Property.PKEnsures (_,Breaks),_,_,_) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPPredicate {ip_kind = PKEnsures (_,Breaks)} as ip) ->
main_ui#pretty_information "This is a breaks clause.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP
- (Property.IPPredicate (Property.PKEnsures (_,Continues),_,_,_) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPPredicate {ip_kind = PKEnsures (_,Continues)} as ip) ->
main_ui#pretty_information "This is a continues clause.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPPredicate(Property.PKAssumes _,_,_,_) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPPredicate {ip_kind = PKAssumes _} as ip) ->
main_ui#pretty_information "This is an assumes clause.@.";
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPDecrease (_,Kglobal,_,_) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPDecrease {id_kinstr=Kglobal} as ip) ->
main_ui#pretty_information
"This is a decreases clause.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPDecrease (_,Kstmt _,_,_) as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPDecrease {id_kinstr=Kstmt _} as ip) ->
main_ui#pretty_information
"This is a loop variant.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPDisjoint _ as ip) ->
+ main_ui#view_original (location ip)
+ | PIP(IPDisjoint _ as ip) ->
main_ui#pretty_information
"This is a disjoint behaviors clause.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPComplete _ as ip) ->
+ main_ui#view_original (location ip)
+ | PIP(IPComplete _ as ip) ->
main_ui#pretty_information
"This is a complete behaviors clause.@.%a@."
pretty_predicate_status ip;
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPAxiom _ as ip) ->
+ main_ui#view_original (location ip)
+ | PIP(IPAxiom _ as ip) ->
main_ui#pretty_information "This is an axiom.@.";
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPAxiomatic _ as ip) ->
+ main_ui#view_original (location ip)
+ | PIP(IPAxiomatic _ as ip) ->
main_ui#pretty_information "This is an axiomatic.@.";
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPLemma _ as ip) ->
+ main_ui#view_original (location ip)
+ | PIP(IPLemma _ as ip) ->
main_ui#pretty_information "This is a lemma.@.";
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPTypeInvariant _ as ip) ->
+ main_ui#view_original (location ip)
+ | PIP(IPTypeInvariant _ as ip) ->
main_ui#pretty_information "This is a type invariant.@.";
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPGlobalInvariant _ as ip) ->
+ main_ui#view_original (location ip)
+ | PIP(IPGlobalInvariant _ as ip) ->
main_ui#pretty_information "This is a global invariant.@.";
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPBehavior _ as ip) ->
+ main_ui#view_original (location ip)
+ | PIP(IPBehavior _ as ip) ->
main_ui#pretty_information "This is a behavior.@.";
- main_ui#view_original (Property.location ip)
- | PIP (Property.IPPropertyInstance (_, _, _, ip') as ip) ->
+ main_ui#view_original (location ip)
+ | PIP (IPPropertyInstance {ii_ip=ip'} as ip) ->
main_ui#pretty_information "@[This is an instance of property `%a'.@]@."
- Property.short_pretty ip';
- main_ui#view_original (Property.location ip)
- | PIP(Property.IPReachable _ | Property.IPOther _) ->
+ short_pretty ip';
+ main_ui#view_original (location ip)
+ | PIP(IPReachable _ | IPOther _) ->
(* these properties are not selectable *)
assert false
| PGlobal _g -> main_ui#pretty_information "This is a global.@.";
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index d7fb0efbdcd..b472ddbdcf4 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -237,18 +237,19 @@ exception Found of int*int
the same location in the source code, typically because one of them
is not printed. Feel free to add other heuristics if needed. *)
let equal_or_same_loc loc1 loc2 =
+ let open Property in
Localizable.equal loc1 loc2 ||
match loc1, loc2 with
- | PIP (Property.IPReachable (_, Kstmt s, _)), PStmt (_, s')
- | PStmt (_, s'), PIP (Property.IPReachable (_, Kstmt s, _))
- | PIP (Property.IPPropertyInstance (_, s, _, _)), PStmt (_, s')
- | PStmt (_, s'), PIP (Property.IPPropertyInstance (_, s, _, _))
+ | PIP (IPReachable {ir_kinstr=Kstmt s}), PStmt (_, s')
+ | PStmt (_, s'), PIP (IPReachable {ir_kinstr=Kstmt s})
+ | PIP (IPPropertyInstance {ii_stmt=s}), PStmt (_, s')
+ | PStmt (_, s'), PIP (IPPropertyInstance {ii_stmt=s})
when
Cil_datatype.Stmt.equal s s' -> true
- | PIP (Property.IPReachable (Some kf, Kglobal, _)),
+ | PIP (IPReachable {ir_kf=Some kf; ir_kinstr=Kglobal}),
(PVDecl (_, _, vi) | PGlobal (GFun ({ svar = vi }, _)))
| (PVDecl (_, _, vi) | PGlobal (GFun ({ svar = vi }, _))),
- PIP (Property.IPReachable (Some kf, Kglobal, _))
+ PIP (IPReachable {ir_kf=Some kf;ir_kinstr=Kglobal})
when Kernel_function.get_vi kf = vi
-> true
| _ -> false
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 8ada692acfd..2a8a584f101 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -612,29 +612,30 @@ let make_panel (main_ui:main_window_extension_points) =
view#set_model (Some model#coerce);
- let visible ip = match ip with
- | Property.IPOther _ -> other.get ()
- | Property.IPReachable _ -> reachable.get ()
- | Property.IPBehavior (_,Kglobal,_,_) -> behaviors.get ()
- | Property.IPBehavior (_,Kstmt _,_,_) -> behaviors.get () && stmtSpec.get ()
- | Property.IPPredicate(Property.PKRequires _,_,Kglobal,_) ->
+ let visible ip =
+ let open Property in match ip with
+ | IPOther _ -> other.get ()
+ | IPReachable _ -> reachable.get ()
+ | IPBehavior {ib_kinstr=Kglobal} -> behaviors.get ()
+ | IPBehavior {ib_kinstr=Kstmt _} -> behaviors.get () && stmtSpec.get ()
+ | IPPredicate {ip_kind=PKRequires _;ip_kinstr=Kglobal} ->
preconditions.get ()
- | Property.IPPredicate(Property.PKRequires _,_,Kstmt _,_) ->
+ | IPPredicate {ip_kind=PKRequires _;ip_kinstr=Kstmt _} ->
preconditions.get () && stmtSpec.get ()
- | Property.IPPredicate(Property.PKAssumes _,_,_,_) -> false
- | Property.IPPredicate(Property.PKEnsures _,_,Kglobal,_) -> ensures.get ()
- | Property.IPExtended(_,_) -> extended.get ()
- | Property.IPPredicate(Property.PKEnsures _,_,Kstmt _,_) ->
+ | IPPredicate {ip_kind = PKAssumes _} -> false
+ | IPPredicate {ip_kind=PKEnsures _;ip_kinstr=Kglobal} -> ensures.get ()
+ | IPExtended _ -> extended.get ()
+ | IPPredicate {ip_kind=PKEnsures _;ip_kinstr=Kstmt _} ->
ensures.get() && stmtSpec.get()
- | Property.IPPredicate(Property.PKTerminates,_,_,_) -> terminates.get ()
- | Property.IPAxiom _ -> false
- | Property.IPTypeInvariant _ -> typeInvariants.get()
- | Property.IPGlobalInvariant _ -> globalInvariants.get()
- | Property.IPAxiomatic _ -> axiomatic.get () && not (onlyCurrent.get ())
- | Property.IPLemma _ -> lemmas.get ()
- | Property.IPComplete _ -> complete_disjoint.get ()
- | Property.IPDisjoint _ -> complete_disjoint.get ()
- | Property.IPCodeAnnot(_,_,({annot_content = AAssert (_, kind, _)} as ca)) ->
+ | IPPredicate {ip_kind = PKTerminates} -> terminates.get ()
+ | IPAxiom _ -> false
+ | IPTypeInvariant _ -> typeInvariants.get()
+ | IPGlobalInvariant _ -> globalInvariants.get()
+ | IPAxiomatic _ -> axiomatic.get () && not (onlyCurrent.get ())
+ | IPLemma _ -> lemmas.get ()
+ | IPComplete _ -> complete_disjoint.get ()
+ | IPDisjoint _ -> complete_disjoint.get ()
+ | IPCodeAnnot {ica_ca={annot_content = AAssert (_, kind, _)} as ca} ->
begin
match Alarms.find ca with
| Some a -> rte.get () && active_alarm a
@@ -643,24 +644,24 @@ let make_panel (main_ui:main_window_extension_points) =
| Assert -> user_assertions.get ()
| Check -> user_checks.get ()
end
- | Property.IPCodeAnnot(_,_,{annot_content = AInvariant _}) ->
+ | IPCodeAnnot {ica_ca={annot_content = AInvariant _}} ->
invariant.get ()
- | Property.IPCodeAnnot(_,_,{annot_content = APragma p}) ->
+ | IPCodeAnnot {ica_ca={annot_content = APragma p}} ->
Logic_utils.is_property_pragma p (* currently always false. *)
- | Property.IPCodeAnnot(_, _, _) -> false (* status of inner nodes *)
- | Property.IPAllocation (_,Kglobal,_,_) -> allocations.get ()
- | Property.IPAllocation (_,Kstmt _,Property.Id_loop _,_) ->
+ | IPCodeAnnot _ -> false (* status of inner nodes *)
+ | IPAllocation {ial_kinstr=Kglobal} -> allocations.get ()
+ | IPAllocation {ial_kinstr=Kstmt _;ial_bhv=Id_loop _} ->
allocations.get ()
- | Property.IPAllocation (_,Kstmt _,Property.Id_contract _,_) ->
+ | IPAllocation {ial_kinstr=Kstmt _;ial_bhv=Id_contract _} ->
allocations.get() && stmtSpec.get()
- | Property.IPAssigns (_,Kglobal,_,_) -> assigns.get ()
- | Property.IPAssigns (_,Kstmt _,Property.Id_loop _,_) ->
+ | IPAssigns {ias_kinstr=Kglobal} -> assigns.get ()
+ | IPAssigns {ias_kinstr=Kstmt _;ias_bhv=Id_loop _} ->
assigns.get ()
- | Property.IPAssigns (_,Kstmt _,Property.Id_contract _,_) ->
+ | IPAssigns {ias_kinstr=Kstmt _;ias_bhv=Id_contract _} ->
assigns.get() && stmtSpec.get()
- | Property.IPFrom _ -> from.get ()
- | Property.IPDecrease _ -> variant.get ()
- | Property.IPPropertyInstance _ -> instances.get ()
+ | IPFrom _ -> from.get ()
+ | IPDecrease _ -> variant.get ()
+ | IPPropertyInstance _ -> instances.get ()
in
let visible_status_aux = function
| Consolidation.Never_tried -> untried.get ()
@@ -774,7 +775,7 @@ let highlighter (buffer:reactive_buffer) localizable ~start ~stop =
'Unknown'. *)
let filter (ip_src, _ip_copy) =
match ip_src with
- | Property.IPPredicate (Property.PKRequires bhv, _, _, _) ->
+ | Property.(IPPredicate {ip_kind=PKRequires bhv}) ->
bhv.b_assumes = []
| _ -> false
in
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 1d3a931ccf0..cbb39030213 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -413,32 +413,32 @@ let rec monitored_property ip =
let open Property in
match ip with
| IPBehavior _ -> false
- | IPPredicate (PKAssumes _,_,_,_) -> false
- | IPPredicate (PKRequires _,_,_,_) -> true
- | IPPredicate (PKEnsures _,_,_,_) -> true
- | IPPredicate (PKTerminates,_,_,_) -> true
- | IPAllocation(_,_,_,_) -> true
- | IPAssigns(_,_,_,_) -> true
- | IPFrom(_,_,_,_) -> true
- | IPDecrease (_,_,_,_) -> true
- | IPCodeAnnot (_,_, { annot_content = AStmtSpec _ } ) -> false
- | IPCodeAnnot (_,_, { annot_content = APragma _ } ) -> false
- | IPCodeAnnot (_,_, { annot_content = AExtended _ } ) -> true
- | IPCodeAnnot (_,_, { annot_content = AAssert _ } ) -> true
- | IPCodeAnnot (_,_, { annot_content = AInvariant _ } ) -> true
- | IPCodeAnnot (_,_, { annot_content = AVariant _ } ) -> true
- | IPCodeAnnot (_,_, { annot_content = AAssigns _ } ) -> true
- | IPCodeAnnot (_,_, { annot_content = AAllocation _ } ) -> true
- | IPComplete (_,_,_,_) -> true
- | IPDisjoint(_,_,_,_) -> true
- | IPReachable (None,_,_) -> false
- | IPReachable (Some _,_,_) -> true
+ | IPPredicate {ip_kind = PKAssumes _} -> false
+ | IPPredicate {ip_kind = PKRequires _} -> true
+ | IPPredicate {ip_kind = PKEnsures _} -> true
+ | IPPredicate {ip_kind = PKTerminates} -> true
+ | IPAllocation _ -> true
+ | IPAssigns _ -> true
+ | IPFrom _-> true
+ | IPDecrease _ -> true
+ | IPCodeAnnot {ica_ca = { annot_content = AStmtSpec _ }} -> false
+ | IPCodeAnnot {ica_ca = { annot_content = APragma _ }} -> false
+ | IPCodeAnnot {ica_ca = { annot_content = AExtended _ }} -> true
+ | IPCodeAnnot {ica_ca = { annot_content = AAssert _ }} -> true
+ | IPCodeAnnot {ica_ca = { annot_content = AInvariant _ }} -> true
+ | IPCodeAnnot {ica_ca = { annot_content = AVariant _ }} -> true
+ | IPCodeAnnot {ica_ca = { annot_content = AAssigns _ }} -> true
+ | IPCodeAnnot {ica_ca = { annot_content = AAllocation _ }} -> true
+ | IPComplete _ -> true
+ | IPDisjoint _ -> true
+ | IPReachable {ir_kf=None} -> false
+ | IPReachable {ir_kf=Some _} -> true
| IPAxiomatic _ | IPAxiom _ -> false
- | IPLemma(_,_,_,_,_) -> true
- | IPTypeInvariant(_,_,_,_) | IPGlobalInvariant(_,_,_) -> true
- | IPOther(_,_) -> true
+ | IPLemma _ -> true
+ | IPTypeInvariant _ | IPGlobalInvariant _ -> true
+ | IPOther _ -> true
| IPExtended _ -> true
- | IPPropertyInstance (_, _, _, ip) -> monitored_property ip
+ | IPPropertyInstance {ii_ip} -> monitored_property ii_ip
let monitor_status properties ip =
if monitored_property ip then
diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/dpds_gui.ml
index b8b5b779c6e..653948a6f57 100644
--- a/src/plugins/scope/dpds_gui.ml
+++ b/src/plugins/scope/dpds_gui.ml
@@ -66,7 +66,7 @@ let ask_for_lval (main_ui:Design.main_window_extension_points) kf =
None
let get_annot_opt localizable = match localizable with
- | Pretty_source.PIP(Property.IPCodeAnnot(_,_,annot)) -> Some annot
+ | Pretty_source.PIP(Property.(IPCodeAnnot {ica_ca})) -> Some ica_ca
| _ -> None
(** [kf_opt] is used if we want to ask the lval to the user in a popup *)
@@ -464,8 +464,8 @@ let highlighter (buffer:Design.reactive_buffer) localizable ~start ~stop =
put_tag (DataScope.tag_stmt stmt);
put_tag (Zones.tag_stmt stmt );
put_tag (ShowDef.tag_stmt stmt)
- | PIP (Property.IPCodeAnnot (_, _, annot)) ->
- put_tag (Pscope.tag_annot annot)
+ | PIP (Property.(IPCodeAnnot {ica_ca})) ->
+ put_tag (Pscope.tag_annot ica_ca)
| PStmtStart _ | PExp _
| PVDecl _ | PTermLval _ | PLval _ | PGlobal _ | PIP _ -> ()
with Not_found -> ()
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index 06607377956..108079350d9 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -40,15 +40,14 @@ let term_c_type t =
let classify_pre_post kf ip =
let open Property in
match ip with
- | IPPredicate (PKEnsures (_, Normal),_,_,_) ->
- Some (GL_Post kf)
- | IPPredicate (PKEnsures _,_,_,_) | IPAxiom _ | IPAxiomatic _ | IPLemma _
+ | IPPredicate {ip_kind = PKEnsures (_, Normal)} -> Some (GL_Post kf)
+ | IPPredicate {ip_kind=PKEnsures _} | IPAxiom _ | IPAxiomatic _ | IPLemma _
| IPTypeInvariant _ | IPGlobalInvariant _
| IPOther _ | IPCodeAnnot _ | IPAllocation _ | IPReachable _
| IPExtended _
| IPBehavior _ -> None
- | IPPropertyInstance (kf, stmt, _, _ip) -> Some (GL_Stmt (kf, stmt))
- | IPPredicate (PKRequires _,_,_,_ | PKAssumes _,_,_,_ | PKTerminates ,_,_,_)
+ | IPPropertyInstance {ii_kf; ii_stmt} -> Some (GL_Stmt (ii_kf, ii_stmt))
+ | IPPredicate {ip_kind=PKRequires _ | PKAssumes _ | PKTerminates}
| IPComplete _ | IPDisjoint _ | IPAssigns _ | IPFrom _ | IPDecrease _ ->
Some (GL_Pre kf)
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 33fcef5d778..d455fab0fdc 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -461,8 +461,11 @@ module Select (Eval: Eval) = struct
| PVDecl (Some kf, Kstmt stmt, vi) ->
let lv = (Var vi, NoOffset) in
select_lv main_ui (GL_Stmt (kf, stmt)) lv
- | PIP (IPCodeAnnot (kf, stmt,
- ({annot_content = AAssert (_, _, p) | AInvariant (_, true, p)} as ca)) as ip) ->
+ | PIP (IPCodeAnnot {ica_kf = kf; ica_stmt = stmt;
+ ica_ca = {annot_content =
+ AAssert (_, _, p)
+ | AInvariant (_, true, p)} as ca
+ } as ip) ->
begin
let loc = GL_Stmt (kf, stmt) in
let alarm_or_property =
@@ -472,14 +475,15 @@ module Select (Eval: Eval) = struct
in
select_predicate_with_red main_ui loc (alarm_or_property, p)
end;
- | PIP (IPPredicate (_, kf, Kglobal, p) as ip) -> begin
+ | PIP (IPPredicate {ip_kf=kf; ip_kinstr=Kglobal; ip_pred=p} as ip) -> begin
match Gui_eval.classify_pre_post kf ip with
| None -> ()
| Some loc ->
select_predicate_with_red
main_ui loc (Red_statuses.Prop ip, Logic_const.pred_of_id_pred p)
end
- | PIP (IPPropertyInstance (kf, stmt, Some pred, ip)) ->
+ | PIP (IPPropertyInstance {ii_kf=kf;ii_stmt=stmt;
+ ii_pred=Some pred;ii_ip=ip}) ->
let loc = GL_Stmt (kf, stmt) in
select_predicate_with_red main_ui loc
(Red_statuses.Prop ip, Logic_const.pred_of_id_pred pred)
@@ -630,11 +634,12 @@ let add_keybord_shortcut_evaluate main_ui =
let bl = Ast_info.block_of_local fdec vi in
select (find_loc kf fdec bl)
end
- | PIP (Property.IPCodeAnnot (kf, stmt,
- {annot_content = AAssert _ | AInvariant (_, true, _)} )) ->
+ | PIP (Property.(IPCodeAnnot {ica_kf = kf; ica_stmt = stmt;
+ ica_ca = {annot_content =
+ AAssert _ | AInvariant (_, true, _)}})) ->
select (Some (GL_Stmt (kf, stmt)))
- | PIP (Property.IPPredicate (_, kf, Kglobal, _) as ip) ->
- select (Gui_eval.classify_pre_post kf ip)
+ | PIP (Property.(IPPredicate {ip_kf; ip_kinstr=Kglobal} as ip)) ->
+ select (Gui_eval.classify_pre_post ip_kf ip)
| _ -> select None
in
main_ui#register_source_selector can_eval_acsl_expr_selector;
diff --git a/src/plugins/value/utils/red_statuses.ml b/src/plugins/value/utils/red_statuses.ml
index 016ab1eedc8..8d81cea49f6 100644
--- a/src/plugins/value/utils/red_statuses.ml
+++ b/src/plugins/value/utils/red_statuses.ml
@@ -90,8 +90,7 @@ let add_red_property ki ip =
by modifying the callstack. Results in a better display *)
let open Property in
match ip with
- | IPPropertyInstance (_, _, _,
- (IPPredicate (PKRequires _, _, _, _) as ip')) ->
+ | IPPropertyInstance {ii_ip=IPPredicate {ip_kind=PKRequires _} as ip'} ->
add_red_ap Kglobal (Prop ip')
| _ -> add_red_ap ki (Prop ip)
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index 08ccbe8ea20..b7d6a7ad039 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -188,8 +188,8 @@ let get_results () =
aux_statuses (fun st -> Property.Hashtbl.add statuses ip st) ip
in
match ip with
- | Property.IPCodeAnnot (_,_,ca) -> begin
- match Alarms.find ca with
+ | Property.(IPCodeAnnot {ica_ca}) -> begin
+ match Alarms.find ica_ca with
| None -> (* real property *) add ()
| Some _ -> (* alarm; do not save it here *) ()
end
@@ -496,10 +496,10 @@ let make_report () =
let report = empty_report () in
let report_property ip =
match ip with
- | Property.IPCodeAnnot (_kf, _stmt, code_annot) ->
+ | Property.(IPCodeAnnot {ica_ca}) ->
begin
let status = get_status ip in
- match Alarms.find code_annot with
+ match Alarms.find ica_ca with
| None -> report_status report.assertions status
| Some alarm ->
let acc_status, acc_alarms = report.alarms in
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 0bab01bf8b9..1d74d1838b5 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -38,31 +38,31 @@ class type computer =
(* -------------------------------------------------------------------------- *)
let compute_ip cc ip =
- match ip with
- | Property.IPLemma _
- | Property.IPAxiomatic _
+ let open Property in match ip with
+ | IPLemma _
+ | IPAxiomatic _
->
let rec iter cc = function
- | Property.IPLemma(name,_,_,_,_) -> cc#add_lemma (LogicUsage.logic_lemma name)
- | Property.IPAxiomatic(_,ips) -> List.iter (iter cc) ips
+ | IPLemma {il_name} -> cc#add_lemma (LogicUsage.logic_lemma il_name)
+ | IPAxiomatic {iax_props} -> List.iter (iter cc) iax_props
| _ -> ()
in iter cc ip ;
cc#compute
- | Property.IPBehavior (kf,_,_,b) ->
+ | IPBehavior {ib_kf; ib_bhv} ->
let model = cc#model in
- let bhv = [b.Cil_types.b_name] in
+ let bhv = [ib_bhv.Cil_types.b_name] in
let assigns = WpAnnot.WithAssigns in
List.iter cc#add_strategy
- (WpAnnot.get_function_strategies ~model ~assigns ~bhv kf) ;
+ (WpAnnot.get_function_strategies ~model ~assigns ~bhv ib_kf) ;
cc#compute
- | Property.IPComplete _
- | Property.IPDisjoint _
- | Property.IPCodeAnnot _
- | Property.IPAllocation _
- | Property.IPAssigns _
- | Property.IPDecrease _
- | Property.IPPredicate _
+ | IPComplete _
+ | IPDisjoint _
+ | IPCodeAnnot _
+ | IPAllocation _
+ | IPAssigns _
+ | IPDecrease _
+ | IPPredicate _
->
let model = cc#model in
let assigns = WpAnnot.WithAssigns in
@@ -70,16 +70,16 @@ let compute_ip cc ip =
(WpAnnot.get_id_prop_strategies ~model ~assigns ip) ;
cc#compute
- | Property.IPFrom _
- | Property.IPAxiom _
- | Property.IPReachable _
- | Property.IPPropertyInstance _
- | Property.IPOther _
- | Property.IPTypeInvariant _
- | Property.IPGlobalInvariant _
- | Property.IPExtended _
+ | IPFrom _
+ | IPAxiom _
+ | IPReachable _
+ | IPPropertyInstance _
+ | IPOther _
+ | IPTypeInvariant _
+ | IPGlobalInvariant _
+ | IPExtended _
->
- Wp_parameters.result "Nothing to compute for '%a'" Property.pretty ip ;
+ Wp_parameters.result "Nothing to compute for '%a'" pretty ip ;
Bag.empty
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index d9aba8b6820..4786a43ee71 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -42,8 +42,8 @@ type focus =
| `Call of GuiSource.call
| `Property of Property.t ]
-let index_of_lemma (l,_,_,_,_) =
- match LogicUsage.section_of_lemma l with
+let index_of_lemma l =
+ match LogicUsage.section_of_lemma l.il_name with
| LogicUsage.Toplevel _ -> Wpo.Axiomatic None
| LogicUsage.Axiomatic a -> Wpo.Axiomatic (Some a.LogicUsage.ax_name)
@@ -54,7 +54,7 @@ let focus_of_selection selection scope =
| S_call c , `Module -> `Index (Wpo.Function(c.s_caller,None))
| S_fun kf , (`Select | `Module) -> `Index(Wpo.Function(kf,None))
| S_prop (IPLemma ilem) , `Module -> `Index(index_of_lemma ilem)
- | S_prop (IPAxiomatic(name,_)) , _ -> `Index(Wpo.Axiomatic (Some name))
+ | S_prop (IPAxiomatic {iax_name=name}) , _ -> `Index(Wpo.Axiomatic (Some name))
| S_prop ip , `Select -> `Property ip
| S_prop ip , `Module ->
begin
diff --git a/src/plugins/wp/GuiSource.ml b/src/plugins/wp/GuiSource.ml
index f08f6d217e1..66a2c8abcf0 100644
--- a/src/plugins/wp/GuiSource.ml
+++ b/src/plugins/wp/GuiSource.ml
@@ -73,7 +73,7 @@ let selection_of_localizable = function
let kind_of_property = function
| Property.IPLemma _ -> "lemma"
| Property.IPCodeAnnot _ -> "annotation"
- | Property.IPPredicate( Property.PKRequires _ , _ , Kglobal , _ ) ->
+ | Property.(IPPredicate {ip_kind=PKRequires _;ip_kinstr = Kglobal}) ->
"precondition for callers"
| _ -> "property"
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index f3e9b63d653..4073c841a93 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -191,9 +191,11 @@ let pp_profile fmt l =
(* -------------------------------------------------------------------------- *)
let ip_lemma l =
+ let open Property in
(if l.lem_axiom then Property.ip_axiom else Property.ip_lemma)
- (l.lem_name,l.lem_labels,l.lem_types,
- l.lem_property,(l.lem_position,l.lem_position))
+ {il_name = l.lem_name; il_labels = l.lem_labels;
+ il_args = l.lem_types; il_loc = (l.lem_position, l.lem_position);
+ il_pred = l.lem_property}
let lemma_of_global proof = function
| Dlemma(name,axiom,labels,types,pred,_,loc) -> {
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 1e2ce76c94b..6164537a9de 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -76,19 +76,20 @@ let wp_unreachable =
~tuning:[] (* TBC *)
let set_unreachable pid =
+ let open Property in
let emit = function
- | Property.IPPredicate(Property.PKAssumes _ ,_,_,_) -> ()
+ | IPPredicate {ip_kind = PKAssumes _} -> ()
| p ->
debug "unreachable annotation %a@." Property.pretty p;
Property_status.emit wp_unreachable ~hyps:[] p Property_status.True
in
let pids = match WpPropId.property_of_id pid with
- | Property.IPPredicate(Property.PKAssumes _ ,_,_,_) -> []
- | Property.IPBehavior(kf, kinstr, active, bhv) ->
- let active = Datatype.String.Set.elements active in
- (Property.ip_post_cond_of_behavior kf kinstr active bhv) @
- (Property.ip_requires_of_behavior kf kinstr bhv)
- | Property.IPExtended _ -> []
+ | IPPredicate {ip_kind = PKAssumes _} -> []
+ | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
+ let active = Datatype.String.Set.elements ib_active in
+ (ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv) @
+ (ip_requires_of_behavior ib_kf ib_kinstr ib_bhv)
+ | IPExtended _ -> []
(* Extended clauses might concern anything. Don't validate them
unless we know exactly what is going on. *)
| p ->
@@ -305,7 +306,7 @@ let filter_assign config pid =
let filter_speconly config pid =
if Cil2cfg.cfg_spec_only config.cfg then
match WpPropId.property_of_id pid with
- | Property.IPPredicate( Property.PKRequires _ , _ , Kglobal , _ ) -> true
+ | Property.(IPPredicate {ip_kind = PKRequires _; ip_kinstr = Kglobal}) -> true
| _ -> false
else true
@@ -1336,13 +1337,13 @@ let get_precond_strategies ~model p =
debug "[get_precond_strategies] %s@."
(Property.Names.get_prop_name_id p);
match p with
- | Property.IPPredicate (Property.PKRequires b, kf, Kglobal, _) ->
+ | Property.(IPPredicate {ip_kind = PKRequires b; ip_kf; ip_kinstr = Kglobal}) ->
let strategies =
- if WpStrategy.is_main_init kf then
- get_strategies NoAssigns kf model [b.b_name] None (IdProp p)
+ if WpStrategy.is_main_init ip_kf then
+ get_strategies NoAssigns ip_kf model [b.b_name] None (IdProp p)
else []
in
- let call_sites = Kernel_function.find_syntactic_callsites kf in
+ let call_sites = Kernel_function.find_syntactic_callsites ip_kf in
let add_call_pre_strategy acc (kf_caller, stmt) =
let asked = CallPre (stmt, Some p) in
get_strategies NoAssigns kf_caller model [] None asked @ acc
@@ -1350,7 +1351,7 @@ let get_precond_strategies ~model p =
if call_sites = [] then
(Wp_parameters.warning ~once:true
"No direct call sites for function '%a': cannot check pre-conditions"
- Kernel_function.pretty kf;
+ Kernel_function.pretty ip_kf;
strategies)
else List.fold_left add_call_pre_strategy strategies call_sites
| _ ->
@@ -1383,29 +1384,29 @@ let get_call_pre_strategies ~model stmt =
let get_id_prop_strategies ~model ?(assigns=WithAssigns) p =
debug "[get_id_prop_strategies] %s@."
(Property.Names.get_prop_name_id p);
- match p with
- | Property.IPCodeAnnot (kf,_,ca) ->
- let bhvs = match ca.annot_content with
+ let open Property in match p with
+ | IPCodeAnnot {ica_kf; ica_ca} ->
+ let bhvs = match ica_ca.annot_content with
| AAssert (l, _, _) | AInvariant (l, _, _) | AAssigns (l, _) -> l
| _ -> []
- in get_strategies assigns kf model bhvs None (IdProp p)
- | Property.IPAssigns (kf, _, Property.Id_loop _, _)
+ in get_strategies assigns ica_kf model bhvs None (IdProp p)
+ | IPAssigns {ias_kf = kf; ias_bhv = Id_loop _}
(*loop assigns: belongs to the default behavior *)
- | Property.IPDecrease (kf,_,_,_) ->
+ | IPDecrease {id_kf = kf} ->
(* any variant property is attached to the default behavior of
* the function, NOT to a statement behavior *)
let bhvs = [ Cil.default_behavior_name ] in
get_strategies assigns kf model bhvs None (IdProp p)
- | Property.IPPredicate (Property.PKRequires _, _kf, Kglobal, _p) ->
+ | IPPredicate {ip_kind = PKRequires _; ip_kinstr = Kglobal} ->
get_precond_strategies model p
| _ ->
- let strategies = match Property.get_kf p with
+ let strategies = match get_kf p with
| None -> Wp_parameters.warning
"WP of property outside functions: ignore %s"
(Property.Names.get_prop_name_id p); []
| Some kf ->
- let ki = Some (Property.get_kinstr p) in
- let bhv = match Property.get_behavior p with
+ let ki = Some (get_kinstr p) in
+ let bhv = match get_behavior p with
| None -> Cil.default_behavior_name
| Some fb -> fb.b_name
in get_strategies assigns kf model [bhv] ki (IdProp p)
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 6121459722a..404100399b5 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -453,27 +453,28 @@ let code_annot_names ca = match ca.annot_content with
(** This is used to give the name of the property that the user can give
* to select it from the command line (-wp-prop option) *)
-let user_prop_names p = match p with
- | Property.IPPredicate (kind,_,_,idp) ->
- Format.asprintf "@@%a" Property.pretty_predicate_kind kind ::
- idp.ip_content.pred_name
- | Property.IPExtended(_,{ext_name}) -> [ Printf.sprintf "@%s" ext_name ]
- | Property.IPCodeAnnot (_,_, ca) -> code_annot_names ca
- | Property.IPComplete (_, _,_,lb) ->
+let user_prop_names p =
+ let open Property in match p with
+ | IPPredicate {ip_kind; ip_pred} ->
+ Format.asprintf "@@%a" Property.pretty_predicate_kind ip_kind ::
+ ip_pred.ip_content.pred_name
+ | IPExtended {ie_ext={ext_name}} -> [ Printf.sprintf "@%s" ext_name ]
+ | IPCodeAnnot {ica_ca} -> code_annot_names ica_ca
+ | IPComplete {ic_bhvs} ->
let kind_name = "@complete_behaviors" in
- let name = Format.asprintf "complete_behaviors%a" pp_names lb
+ let name = Format.asprintf "complete_behaviors%a" pp_names ic_bhvs
in kind_name::[name]
- | Property.IPDisjoint (_, _,_, lb) ->
+ | IPDisjoint {ic_bhvs} ->
let kind_name = "@disjoint_behaviors" in
- let name = Format.asprintf "disjoint_behaviors%a" pp_names lb
+ let name = Format.asprintf "disjoint_behaviors%a" pp_names ic_bhvs
in kind_name::[name]
- | Property.IPAssigns (_, _, _, l) ->
+ | IPAssigns {ias_froms} ->
List.fold_left
(fun acc (t,_) -> (ident_names t.it_content.term_name) @ acc)
- ["@assigns"] l
- | Property.IPDecrease (_,_, Some ca,_) -> "@decreases"::code_annot_names ca
- | Property.IPDecrease _ -> [ "@decreases" ]
- | Property.IPLemma (a,_,_,l,_) ->
+ ["@assigns"] ias_froms
+ | IPDecrease {id_ca=Some ca} -> "@decreases"::code_annot_names ca
+ | IPDecrease _ -> [ "@decreases" ]
+ | IPLemma {il_name = a; il_pred = l} ->
let names = "@lemma"::a::(ident_names l.pred_name)
in begin
match LogicUsage.section_of_lemma a with
@@ -481,16 +482,16 @@ let user_prop_names p = match p with
| LogicUsage.Axiomatic ax -> ax.LogicUsage.ax_name::names
end
(* TODO *)
- | Property.IPFrom _
- | Property.IPAllocation _
- | Property.IPAxiomatic _
- | Property.IPAxiom _
- | Property.IPBehavior _
- | Property.IPReachable _
- | Property.IPPropertyInstance _
- | Property.IPTypeInvariant _
- | Property.IPGlobalInvariant _
- | Property.IPOther _ -> []
+ | IPFrom _
+ | IPAllocation _
+ | IPAxiomatic _
+ | IPAxiom _
+ | IPBehavior _
+ | IPReachable _
+ | IPPropertyInstance _
+ | IPTypeInvariant _
+ | IPGlobalInvariant _
+ | IPOther _ -> []
let string_of_termination_kind = function
Normal -> "post"
@@ -578,8 +579,10 @@ let kinstr_hints hs = function
let propid_hints hs p =
match p.p_kind , p.p_prop with
| PKCheck , _ -> ()
- | PKProp , Property.IPAssigns (_ , Kstmt _, _, _) -> add_required hs "stmt-assigns"
- | PKProp , Property.IPAssigns (_ , Kglobal, _, _) -> add_required hs "fct-assigns"
+ | PKProp , Property.(IPAssigns {ias_kinstr=Kstmt _}) ->
+ add_required hs "stmt-assigns"
+ | PKProp , Property.(IPAssigns {ias_kinstr=Kglobal}) ->
+ add_required hs "fct-assigns"
| PKPropLoop , Property.IPAssigns _ -> add_required hs "loop-assigns"
| PKPropLoop , _ -> add_required hs "invariant"
| PKProp , _ -> add_required hs "property"
@@ -622,21 +625,23 @@ let annot_hints hs = function
| AAllocation _ | AAssigns(_,WritesAny) | AStmtSpec _
| AVariant _ | APragma _ | AExtended _ -> ()
-let property_hints hs = function
- | Property.IPAxiom (s,_,_,p,_)
- | Property.IPLemma (s,_,_,p,_) -> List.iter (add_required hs) (s::p.pred_name)
- | Property.IPBehavior _ -> ()
- | Property.IPComplete(_,_,_,ps) | Property.IPDisjoint(_,_,_,ps) ->
- List.iter (add_required hs) ps
- | Property.IPPredicate(_,_,_,ipred) ->
- List.iter (add_hint hs) ipred.ip_content.pred_name
- | Property.IPExtended(_,{ext_name}) -> List.iter (add_hint hs) [ext_name]
- | Property.IPCodeAnnot(_,_,ca) -> annot_hints hs ca.annot_content
- | Property.IPAssigns(_,_,_,froms) -> assigns_hints hs froms
- | Property.IPAllocation _ (* TODO *)
- | Property.IPFrom _ | Property.IPDecrease _ | Property.IPPropertyInstance _
- | Property.IPReachable _ | Property.IPAxiomatic _ | Property.IPOther _
- | Property.IPTypeInvariant _ | Property.IPGlobalInvariant _ -> ()
+let property_hints hs =
+ let open Property in function
+ | IPAxiom {il_name; il_pred}
+ | IPLemma {il_name; il_pred} ->
+ List.iter (add_required hs) (il_name::il_pred.pred_name)
+ | IPBehavior _ -> ()
+ | IPComplete {ic_bhvs} | IPDisjoint {ic_bhvs} ->
+ List.iter (add_required hs) ic_bhvs
+ | IPPredicate {ip_pred} ->
+ List.iter (add_hint hs) ip_pred.ip_content.pred_name
+ | IPExtended {ie_ext={ext_name}} -> List.iter (add_hint hs) [ext_name]
+ | IPCodeAnnot {ica_ca} -> annot_hints hs ica_ca.annot_content
+ | IPAssigns {ias_froms} -> assigns_hints hs ias_froms
+ | IPAllocation _ (* TODO *)
+ | IPFrom _ | Property.IPDecrease _ | Property.IPPropertyInstance _
+ | IPReachable _ | Property.IPAxiomatic _ | Property.IPOther _
+ | IPTypeInvariant _ | Property.IPGlobalInvariant _ -> ()
let prop_id_keys p =
begin
@@ -705,7 +710,7 @@ let is_assigns p =
| _ -> false
let is_requires = function
- | Property.IPPredicate (Property.PKRequires _,_,_,_) -> true
+ | Property.(IPPredicate {ip_kind = PKRequires _}) -> true
| _ -> false
let is_loop_preservation p =
@@ -998,11 +1003,11 @@ let get_loop_stmt kf stmt =
(** Quite don't understand what is going on here... what is it supposed to do ?
* [2011-07-07-Anne] *)
let get_induction p =
- let get_stmt = function
- | Property.IPDecrease(kf,Kstmt stmt,_,_) -> Some (kf, stmt)
- | Property.IPCodeAnnot(kf,stmt,_) -> Some (kf, stmt)
- | Property.IPAssigns(kf,Kstmt stmt,_,_) -> Some (kf, stmt)
- | _ -> None
+ let get_stmt = let open Property in function
+ | IPDecrease {id_kf;id_kinstr=Kstmt stmt} -> Some (id_kf, stmt)
+ | IPCodeAnnot {ica_kf;ica_stmt} -> Some (ica_kf, ica_stmt)
+ | IPAssigns {ias_kf; ias_kinstr=Kstmt stmt} -> Some (ias_kf, stmt)
+ | _ -> None
in match p.p_kind with
| PKCheck | PKAFctOut|PKAFctExit|PKPre _ | PKTactic -> None
| PKProp ->
@@ -1011,13 +1016,13 @@ let get_induction p =
| Some (kf, s) -> get_loop_stmt kf s
in loop_stmt_opt
| PKPropLoop ->
+ let open Property in
let loop_stmt_opt = match property_of_id p with
- | Property.IPCodeAnnot(kf,stmt,
- {annot_content = AInvariant(_, loop, _)})
- ->
- if loop then (*loop invariant *) Some stmt
- else (* invariant inside loop *) get_loop_stmt kf stmt
- | Property.IPAssigns (_, Kstmt stmt, Property.Id_loop _, _) ->
+ | IPCodeAnnot {ica_kf; ica_stmt;
+ ica_ca = {annot_content = AInvariant(_, loop, _)}} ->
+ if loop then (*loop invariant *) Some ica_stmt
+ else (* invariant inside loop *) get_loop_stmt ica_kf ica_stmt
+ | IPAssigns {ias_kinstr=Kstmt stmt; ias_bhv = Id_loop _} ->
(* loop assigns *) Some stmt
| _ -> None (* assert false ??? *)
in loop_stmt_opt
--
GitLab