diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index f6b1012b3192e43a6b11e97b07b667eb8978d3b9..adef0ac0916fad00d6aceea5e0acda85788c5404 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -461,22 +461,20 @@ module ExtMerging =
Merging
(struct
type t = acsl_extension
- let hash ((_,name,_,_,kind) : acsl_extension) =
- Datatype.String.hash name + 5 * hash_ext_kind kind
- let compare
- ((_,name1,_,s1,kind1) : acsl_extension)
- ((_,name2,_,s2,kind2) : acsl_extension) =
- let res = Datatype.String.compare name1 name2 in
+ let hash (e : acsl_extension) =
+ Datatype.String.hash e.ext_name + 5 * hash_ext_kind e.ext_kind
+ let compare (e1 : acsl_extension) (e2 : acsl_extension) =
+ let res = Datatype.String.compare e1.ext_name e2.ext_name in
if res <> 0 then res
else
- let res = Datatype.Bool.compare s1 s2 in
+ let res = Datatype.Bool.compare e1.ext_has_status e2.ext_has_status in
if res <> 0 then res
else
- compare_ext_kind kind1 kind2
+ compare_ext_kind e1.ext_kind e2.ext_kind
let equal x y = compare x y = 0
let merge_synonym _ = true
- let output fmt (_,name,_,_,_) =
- Format.fprintf fmt "global ACSL extension %s" name
+ let output fmt {ext_name} =
+ Format.fprintf fmt "global ACSL extension %s" ext_name
end)
type volatile_kind = R | W
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 99c30feec37f0d16370a52667a113963f80bf435..c7dcf53a99fc2f9ad23ef10b86036b3af042eb67 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1665,7 +1665,13 @@ and spec = {
grammar ambiguous.
@plugin development guide *)
-and acsl_extension = int * string * location * bool * acsl_extension_kind
+and acsl_extension = {
+ ext_id : int;
+ ext_name : string;
+ ext_loc : location;
+ ext_has_status : bool;
+ ext_kind : acsl_extension_kind
+}
(** @plugin development guide *)
and acsl_extension_kind =
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 2b35d02c825e07820bec0be9d2192080fe912288..ffd1ed30d7e08381192130e1442b5ccca37ddf00 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -254,7 +254,7 @@ let rec location = function
| [] -> Cil_datatype.Location.unknown
| p :: _ -> location p)
| IPLemma (_,_,_,_,loc) -> loc
- | IPExtended(_,(_,_,loc,_,_)) -> loc
+ | IPExtended(_,{ext_loc}) -> ext_loc
| IPOther(_,loc_e) -> loc_of_loc_o loc_e
| IPTypeInvariant(_,_,_,loc) | IPGlobalInvariant(_,_,loc) -> loc
@@ -303,7 +303,8 @@ let get_behavior = function
(* --- Property Status --- *)
(* -------------------------------------------------------------------------- *)
-let has_status_ext ((_,_,_,status,_) : Cil_types.acsl_extension) = status
+let has_status_ext ({ext_has_status} : Cil_types.acsl_extension) =
+ ext_has_status
let has_status_ca = function
| AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _ | AAllocation _
@@ -455,7 +456,7 @@ include Datatype.Make_with_collections
| IPOther(s,_) -> Hashtbl.hash (15, (s:string))
| IPTypeInvariant(s,_,_,_) -> Hashtbl.hash (16, (s:string))
| IPGlobalInvariant(s,_,_) -> Hashtbl.hash (17, (s:string))
- | IPExtended (_,(i,_,_,_,_)) -> Hashtbl.hash (18, i)
+ | IPExtended (_,{ext_id}) -> Hashtbl.hash (18, ext_id)
let rec equal p1 p2 =
let eq_bhv (f1,ki1,b1) (f2,ki2,b2) =
@@ -472,7 +473,8 @@ include Datatype.Make_with_collections
in
match p1, p2 with
| IPPredicate (_,_,_,s1), IPPredicate (_,_,_,s2) -> s1.ip_id = s2.ip_id
- | IPExtended (_,(i1,_,_,_,_)), IPExtended (_,(i2,_,_,_,_)) -> Datatype.Int.equal i1 i2
+ | 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,_,_,_)
@@ -532,7 +534,7 @@ include Datatype.Make_with_collections
match x, y with
| IPPredicate (_,_,_,s1), IPPredicate (_,_,_,s2) ->
Datatype.Int.compare s1.ip_id s2.ip_id
- | IPExtended (_,(i1,_,_,_,_)), IPExtended (_,(i2,_,_,_,_)) ->
+ | IPExtended (_,{ext_id=i1}), IPExtended (_,{ext_id=i2}) ->
Datatype.Int.compare i1 i2
| IPCodeAnnot(_,_,ca1), IPCodeAnnot(_,_,ca2) ->
Datatype.Int.compare ca1.annot_id ca2.annot_id
@@ -614,7 +616,7 @@ let rec short_pretty fmt p = match p with
| IPPredicate (_,_,_,{ ip_content = {pred_name = name :: _ }}) ->
Format.pp_print_string fmt name
| IPPredicate _ -> pretty fmt p
- | IPExtended (_,(_,name,_,_,_)) -> Format.pp_print_string fmt name
+ | 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
@@ -903,8 +905,8 @@ struct
Format.asprintf "%s%s%a"
(kf_prefix kf) (predicate_kind_txt pk ki)
pp_names idp.ip_content.pred_name
- | IPExtended (le,(_,name,_,_,_)) ->
- Format.asprintf "%sextended%a" (extended_loc_prefix le) pp_names [name]
+ | IPExtended (le,{ext_name}) ->
+ 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"
@@ -916,7 +918,7 @@ struct
| AAssigns _ -> "assigns"
| AVariant _ -> "variant"
| AAllocation _ -> "allocates"
- | AExtended(_,_,(_,clause,_,_,_)) -> clause
+ | 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"
@@ -1092,8 +1094,8 @@ struct
| IPCodeAnnot (kf,stmt, { annot_content = APragma _ } ) ->
[ K kf ; A "pragma" ; S stmt ]
- | IPCodeAnnot (kf,stmt, { annot_content = AExtended(_,_,(_,clause,_,_,_)) } )
- -> [ K kf ; A clause ; S stmt ]
+ | IPCodeAnnot (kf,stmt, { annot_content = AExtended(_,_,{ext_name}) } ) ->
+ [ K kf ; A ext_name ; S stmt ]
| IPCodeAnnot (kf,_, { annot_content = AAssert(_,Assert,p) } ) ->
[K kf ; A "assert" ; P p ]
@@ -1138,9 +1140,9 @@ struct
| IPOther(name,OLContract kf) -> [ K kf ; A name ]
| IPOther(name,OLStmt(kf,s)) -> [ K kf ; A name ; S s ]
- | IPExtended(ELGlob,(_,name,_,_,_)) -> [ A name ]
- | IPExtended(ELContract(kf),(_,name,_,_,_)) -> [ K kf ; A name ]
- | IPExtended(ELStmt(kf,s),(_,name,_,_,_)) -> [ 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 ]
| IPPropertyInstance (_, _, _, ip) -> parts_of_property ip
@@ -1373,8 +1375,8 @@ let ip_of_code_annot kf stmt ca =
| APragma p when Logic_utils.is_property_pragma p ->
[ IPCodeAnnot (kf,stmt,ca) ]
| APragma _ -> []
- | AExtended(_,_,(_,_,_,status,_ as ext)) ->
- if status then [IPExtended(ELStmt(kf,stmt),ext)] else []
+ | AExtended(_,_,ext) ->
+ if ext.ext_has_status then [IPExtended(ELStmt(kf,stmt),ext)] else []
let ip_of_code_annot_single kf stmt ca = match ip_of_code_annot kf stmt ca with
| [] ->
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 1907d10435bd5f9c3b35152e63a07c3395a5f270..8bd5ca9b33d04613798ea2fb00fffc9bb820f951 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -42,13 +42,13 @@ module Behavior_extensions = struct
| Ext_preds preds ->
Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt preds
- let pp (printer) fmt (_,name,_,_,ext) =
+ let pp (printer) fmt {ext_name; ext_kind} =
let pp =
try
- Hashtbl.find printer_tbl name
+ Hashtbl.find printer_tbl ext_name
with Not_found -> default_pp
in
- Format.fprintf fmt "@[<hov 2>%s %a;@]" name (pp printer) ext
+ Format.fprintf fmt "@[<hov 2>%s %a;@]" ext_name (pp printer) ext_kind
end
let register_behavior_extension = Behavior_extensions.register
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index a257df94803dba685cad02225f88df1a5cad0250..6b1f5e7d77942ece1fe48c12f68334488fe9763c 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -902,7 +902,11 @@ and pp_spec fmt spec =
(pp_list (pp_list pp_string)) spec.spec_complete_behaviors
(pp_list (pp_list pp_string)) spec.spec_disjoint_behaviors
-and pp_acsl_extension fmt = pp_tuple5 pp_int pp_string pp_location pp_bool pp_acsl_extension_kind fmt
+and pp_acsl_extension fmt ext =
+ Format.fprintf fmt
+ "{ext_id=%d;ext_name=%s;ext_loc=%a;ext_has_status=%B;ext_kind=%a}"
+ ext.ext_id ext.ext_name pp_location ext.ext_loc ext.ext_has_status
+ pp_acsl_extension_kind ext.ext_kind
and pp_acsl_extension_kind fmt = function
| Ext_id(int) -> Format.fprintf fmt "Ext_id(%a)" pp_int int
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index e314dca611ad44aa5f4d27d8db5e9e31311bed5c..3f4baed5afc864a2a3da0f951a13b2e96f00b6e2 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -212,7 +212,7 @@ let pp_active fmt active =
let pp_capitalize fmt s =
Format.pp_print_string fmt (Transitioning.String.capitalize_ascii s)
-let pp_acsl_extension fmt (_,s,_,_,_) = 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
@@ -232,10 +232,10 @@ let rec pp_prop kfopt kiopt kloc fmt = function
pp_predicate kind
(pp_idpred kloc) idpred
(pp_kinstr kloc) ki
- | IPExtended(le,(_,_,loc,_,_ as ext)) ->
+ | IPExtended(le,ext) ->
Format.fprintf fmt "%a%a"
pp_acsl_extension ext
- (pp_extended_loc kfopt kiopt kloc) (loc,le)
+ (pp_extended_loc kfopt kiopt kloc) (ext.ext_loc,le)
| IPBehavior(_,ki, active, bhv) ->
if Cil.is_default_behavior bhv then
Format.fprintf fmt "Default behavior%a%a"
@@ -268,9 +268,9 @@ let rec pp_prop kfopt kiopt kloc fmt = function
pp_for bs
pp_named np
(pp_kloc kloc) np.pred_loc
- | IPCodeAnnot(_,stmt,{annot_content=AExtended(bs,_,(_,clause,_,_,_))}) ->
+ | IPCodeAnnot(_,stmt,{annot_content=AExtended(bs,_,{ext_name})}) ->
Format.fprintf fmt "%a%a %a"
- pp_capitalize clause pp_for bs (pp_stmt kloc) stmt
+ 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)) ->
@@ -498,10 +498,10 @@ let rec ip_order = function
| 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,(_,n,_,_,_)) -> [I 21;F kf; S n]
- | IPExtended(ELStmt (kf, stmt), (_,n,_,_,_)) ->
- [ I 22; F kf; K (Kstmt stmt); S n]
- | IPExtended(ELGlob, (_,n,_,_,_)) -> [ I 23; S n]
+ | IPExtended(ELContract kf, {ext_name}) -> [I 21;F kf; S ext_name]
+ | IPExtended(ELStmt (kf, stmt), {ext_name}) ->
+ [ I 22; F kf; K (Kstmt stmt); S ext_name]
+ | IPExtended(ELGlob, {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_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 892f3a46cbc482965317ac27d94cdc3e48d02bcf..c1b1928bf7efb053ecafd7a341cdd547da89fb41 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -2953,15 +2953,16 @@ and childrenBehavior vis b =
b.b_extended <- mapNoCopy (visitCilExtended vis) b.b_extended;
b
-and visitCilExtended vis (i,a,l,s,e as orig) =
+and visitCilExtended vis orig =
let visit =
- try Hashtbl.find visitor_tbl a
+ try Hashtbl.find visitor_tbl orig.ext_name
with Not_found -> (fun _ _ -> DoChildren)
in
- let e' = doVisitCil vis id (visit vis) childrenCilExtended e in
+ let e' = doVisitCil vis id (visit vis) childrenCilExtended orig.ext_kind in
if is_fresh_behavior vis#behavior then
- Logic_const.new_acsl_extension a l s e'
- else if e == e' then orig else (i,a,l,s,e')
+ Logic_const.new_acsl_extension orig.ext_name orig.ext_loc
+ orig.ext_has_status e'
+ else if orig.ext_kind == e' then orig else {orig with ext_kind = e'}
and childrenCilExtended vis p =
match p with
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 9dd7af1b0dcf63529d9afc09538193880c56f539..5e519e73979b352d4375c72dbf51febae20cb07f 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -1992,8 +1992,8 @@ module Global_annotation = struct
if res = 0 then Attributes.compare attr1 attr2 else res
| Dcustom_annot _, _ -> -1
| _, Dcustom_annot _ -> 1
- | Dextended ((id1,_,_,_,_),_,_), Dextended((id2,_,_,_,_),_,_) ->
- Datatype.Int.compare id1 id2
+ | Dextended (ext1, _, _), Dextended (ext2, _, _) ->
+ Datatype.Int.compare ext1.ext_id ext2.ext_id
let equal = Datatype.from_compare
@@ -2012,7 +2012,7 @@ module Global_annotation = struct
| Dtype_annot(l,_) -> 17 * Logic_info.hash l
| Dmodel_annot(l,_) -> 19 * Model_info.hash l
| Dcustom_annot(_,n,_,_) -> 23 * Datatype.String.hash n
- | Dextended ((id,_,_,_,_),_,_) -> 29 * Datatype.Int.hash id
+ | Dextended ({ext_id},_,_) -> 29 * Datatype.Int.hash ext_id
let copy = Datatype.undefined
end)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 1f1726189a09cf9422cab0e6a3d1c11e3c29f5cf..daef01e19de961518a5197f84fe02c428a0b75dd 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -733,8 +733,8 @@ let synchronize_source_annot has_new_stmt kf =
match annot.annot_content with
| AStmtSpec _ | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt)
-> true
- | AExtended(_,is_loop,(_,name,_,_,_)) ->
- (match Logic_env.extension_category name with
+ | AExtended(_,is_loop,{ext_name}) ->
+ (match Logic_env.extension_category ext_name with
| Some (Ext_code_annot (Ext_here | Ext_next_loop)) -> false
| Some (Ext_code_annot Ext_next_stmt) -> true
| Some (Ext_code_annot Ext_next_both) -> not is_loop
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 4bce2e9f47358e0217e4be1ae5dff931bc6b52f0..a145816ff6a252b6a4290cc759a36b1dc8f14b25 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -612,8 +612,8 @@ class check ?(is_normalized=true) what : Visitor.frama_c_visitor =
in
let my_labels =
match ca.annot_content with
- | AExtended (_, is_loop, (_, name, _, _, _)) ->
- (match Logic_env.extension_category name, is_loop with
+ | AExtended (_, is_loop, {ext_name}) ->
+ (match Logic_env.extension_category ext_name, is_loop with
| Some (Ext_code_annot (Ext_next_stmt | Ext_next_both)), false ->
Logic_const.post_label :: my_labels
| Some (Ext_code_annot Ext_here), false -> my_labels
@@ -624,18 +624,18 @@ class check ?(is_normalized=true) what : Visitor.frama_c_visitor =
Kernel.(
warning ~wkey:wkey_acsl_extension
"%s is a code annotation extension, \
- but used as a loop annotation" name);
+ but used as a loop annotation" ext_name);
my_labels
| Some (Ext_code_annot (Ext_next_loop)), false ->
Kernel.(
warning ~wkey:wkey_acsl_extension
"%s is a loop annotation extension, \
- but used as a code annotation" name;
+ but used as a code annotation" ext_name;
my_labels)
| (Some (Ext_contract | Ext_global) | None), _ ->
Kernel.(
warning ~wkey:wkey_acsl_extension
- "%s is not a known code annotation extension" name);
+ "%s is not a known code annotation extension" ext_name);
my_labels)
| AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _
| AAssigns _ | AAllocation _ | APragma _ -> my_labels
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index f7a548fd135710c450a03ca36754d3cd3bc75666..de7fd61e1c36b4282b2ff28658fca7dda6d06285 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -55,8 +55,8 @@ let refresh_predicate p = { p with ip_id = PredicateId.next () }
let new_identified_term t =
{ it_id = TermId.next (); it_content = t }
-let new_acsl_extension name l s k : acsl_extension =
- ExtendedId.next (), name, l, s , k
+let new_acsl_extension ext_name ext_loc ext_has_status ext_kind =
+ {ext_id = ExtendedId.next (); ext_name; ext_loc; ext_has_status; ext_kind}
let fresh_term_id = TermId.next
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index d85fd2d87048f8bfc46ee8a03c070a4cac99a460..4ba6bcb2ddf97252e83205652997f9d94ce826a2 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1002,10 +1002,10 @@ let is_same_pragma p1 p2 =
| Impact_pragma p1, Impact_pragma p2 -> is_same_impact_pragma p1 p2
| (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false
-let is_same_extension (_,e1,_,s1,c1) (_,e2,_,s2,c2) =
- Datatype.String.equal e1 e2 &&
- (s1 = s2) &&
- match c1, c2 with
+let is_same_extension x1 x2 =
+ Datatype.String.equal x1.ext_name x2.ext_name &&
+ (x1.ext_has_status = x2.ext_has_status) &&
+ match x1.ext_kind, x2.ext_kind with
| Ext_id i1, Ext_id i2 -> i1 = i2
| Ext_terms t1, Ext_terms t2 ->
is_same_list is_same_term t1 t2
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index cbcc2b5f8f7724fcd5f567a38cc3e0d44e9f0286..d74c850f40c6055db78e7cc12bb582a693cf6cb9 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -447,10 +447,9 @@ let to_do_on_select
main_ui#pretty_information "This is a requires clause.@.%a@."
pretty_predicate_status ip;
main_ui#view_original (Property.location ip)
- | PIP (Property.IPExtended(_,(_,name,_,_,_)) as ip) ->
+ | PIP (Property.IPExtended(_,{ext_name}) as ip) ->
main_ui#pretty_information "This clause is a %s extension.@.%a@."
- name
- pretty_predicate_status ip;
+ ext_name pretty_predicate_status ip;
main_ui#view_original (Property.location ip)
| PIP (Property.IPPredicate (Property.PKTerminates,_,_,_) as ip) ->
main_ui#pretty_information "This is a terminates clause.@.%a@."
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index b43c4f593db11d9679434a52a86a084ec7843434..d8eb7c7c5226fdb464a53fe9e63c78a9ab2c4364 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -325,7 +325,7 @@ module MYTREE = struct
| Dtype_annot (li, _) -> Some (global_name li.l_var_info.lv_name)
| Dmodel_annot (mf, _) -> Some (global_name mf.mi_name)
| Dcustom_annot _ -> Some "custom clause"
- | Dextended ((_,name,_,_,_),_,_) -> Some ("ACSL extension " ^ name)
+ | Dextended ({ext_name},_,_) -> Some ("ACSL extension " ^ ext_name)
let make_list_globals hide sort_order globs =
(* Association list binding names to globals. *)
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 9ccc80eb23103cbb27441673f342fe6a8687730f..53c8b51170f36737210249d4a674c638ce519295 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -323,7 +323,7 @@ class slocVisitor ~libc : sloc_visitor = object(self)
| Dtype_annot (ta, _) -> ta.l_var_info.lv_name
| Dmodel_annot (mi, _) -> mi.mi_name
| Dcustom_annot (_c, _n, _, _) -> " (Custom) "
- | Dextended ((_, n, _, _, _), _, _) -> " (Extension " ^ n ^ ")"
+ | Dextended ({ext_name}, _, _) -> " (Extension " ^ ext_name ^ ")"
end
method private images (globs:global list) =
diff --git a/src/plugins/value/utils/partitioning_annots.ml b/src/plugins/value/utils/partitioning_annots.ml
index f88bf5cf6cdd1ea39b851ee5d658b23822b0aeb1..a4ee12b872fc082a8c50fbba71c4121408fbfd60 100644
--- a/src/plugins/value/utils/partitioning_annots.ml
+++ b/src/plugins/value/utils/partitioning_annots.ml
@@ -91,9 +91,9 @@ struct
let get stmt =
let filter_add _emitter annot acc =
match annot.annot_content with
- | Cil_types.AExtended (_, is_loop_annot', (_,name',_,_,data))
+ | Cil_types.AExtended (_, is_loop_annot', {ext_name=name'; ext_kind})
when name' = name && is_loop_annot' = is_loop_annot ->
- import data :: acc
+ import ext_kind :: acc
| _ -> acc
in
List.rev (Annotations.fold_code_annot filter_add stmt [])
diff --git a/src/plugins/value/utils/widen_hints_ext.ml b/src/plugins/value/utils/widen_hints_ext.ml
index f9c808f43ee687b0c9e98c9ad8b674e49a1d8090..743fc237c94b8db4fe15f4689cf34d6b9ec2da5c 100644
--- a/src/plugins/value/utils/widen_hints_ext.ml
+++ b/src/plugins/value/utils/widen_hints_ext.ml
@@ -167,7 +167,7 @@ let get_widen_hints_annots stmt =
(fun _emitter annot acc ->
match annot with
| {annot_content =
- AExtended (_, _,(_,"widen_hints", _, _,Ext_terms terms))} ->
+ AExtended (_, _, {ext_name = "widen_hints"; ext_kind = Ext_terms terms})} ->
(* loop widen_hints *)
acc @ [terms]
| _ -> acc
diff --git a/src/plugins/wp/dyncall.ml b/src/plugins/wp/dyncall.ml
index b7ab106b39aefdc31e7a7be26f210d6bfb692f3d..ad7bbf995c38f93f37686fe06d6fdd112f22826e 100644
--- a/src/plugins/wp/dyncall.ml
+++ b/src/plugins/wp/dyncall.ml
@@ -67,7 +67,7 @@ let get_calls ecmd bhvs : (string * Kernel_function.t list) list =
let fs = ref [] in
List.iter
(function
- | _,cmd, _, _, Ext_terms ts when cmd = ecmd ->
+ | {ext_name; ext_kind = Ext_terms ts} when ext_name = ecmd ->
fs := !fs @ List.map get_call ts
| _ -> ())
bhv.Cil_types.b_extended ;
@@ -138,48 +138,49 @@ class dyncall =
method! vcode_annot ca =
match ca.annot_content with
| Cil_types.AExtended
- (bhvs,_,((_,"calls",_,_,Ext_terms calls) as extended)) ->
- if calls <> [] && (scope <> [] || not (Stack.is_empty block_calls))
- then begin
- let bhvs =
- match bhvs with
- | [] -> [ Cil.default_behavior_name ]
- | bhvs -> bhvs
- in
- let debug_calls bhv stmt kfs =
- if Wp_parameters.has_dkey dkey_calls then
- let source = snd (Stmt.loc stmt) in
- if Cil.default_behavior_name = bhv then
- Wp_parameters.result ~source
- "@[<hov 2>Calls%a@]" pp_calls kfs
- else
- Wp_parameters.result ~source
- "@[<hov 2>Calls (for %s)%a@]" bhv pp_calls kfs
- in
- let pool = ref [] in (* collect emitted properties *)
- let add_calls_info kf stmt =
- count <- succ count ;
- List.iter
- (fun bhv ->
- let kfs = List.map get_call calls in
- debug_calls bhv stmt kfs ;
- let prop = property ~kf ~bhv ~stmt kfs in
- pool := prop :: !pool ;
- CallPoints.add (bhv,stmt) (prop,kfs))
- bhvs
- in
- let kf = self#kf in
+ (bhvs, _,
+ ({ext_name = "calls"; ext_kind = Ext_terms calls} as extended)) ->
+ if calls <> [] && (scope <> [] || not (Stack.is_empty block_calls))
+ then begin
+ let bhvs =
+ match bhvs with
+ | [] -> [ Cil.default_behavior_name ]
+ | bhvs -> bhvs
+ in
+ let debug_calls bhv stmt kfs =
+ if Wp_parameters.has_dkey dkey_calls then
+ let source = snd (Stmt.loc stmt) in
+ if Cil.default_behavior_name = bhv then
+ Wp_parameters.result ~source
+ "@[<hov 2>Calls%a@]" pp_calls kfs
+ else
+ Wp_parameters.result ~source
+ "@[<hov 2>Calls (for %s)%a@]" bhv pp_calls kfs
+ in
+ let pool = ref [] in (* collect emitted properties *)
+ let add_calls_info kf stmt =
+ count <- succ count ;
List.iter
- (add_calls_info kf)
- (if scope <> [] then scope else Stack.top block_calls) ;
- if !pool <> [] then
- begin
- let eloc = Property.ELStmt(kf,self#stmt) in
- let annot = Property.ip_of_extended eloc extended in
- Property_status.logical_consequence emitter annot !pool ;
- end
- end;
- SkipChildren
+ (fun bhv ->
+ let kfs = List.map get_call calls in
+ debug_calls bhv stmt kfs ;
+ let prop = property ~kf ~bhv ~stmt kfs in
+ pool := prop :: !pool ;
+ CallPoints.add (bhv,stmt) (prop,kfs))
+ bhvs
+ in
+ let kf = self#kf in
+ List.iter
+ (add_calls_info kf)
+ (if scope <> [] then scope else Stack.top block_calls) ;
+ if !pool <> [] then
+ begin
+ let eloc = Property.ELStmt(kf,self#stmt) in
+ let annot = Property.ip_of_extended eloc extended in
+ Property_status.logical_consequence emitter annot !pool ;
+ end
+ end;
+ SkipChildren
| _ -> SkipChildren
method! vspec spec =
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 894def5654e6c88349bb8a1f22669a3cf852d950..6121459722a1fd373080a398f3de1bcc3607b663 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -448,7 +448,7 @@ let code_annot_names ca = match ca.annot_content with
| AAssert (_, Assert, named_pred) -> "@assert"::(ident_names named_pred.pred_name)
| AInvariant (_,_,named_pred) -> "@invariant"::(ident_names named_pred.pred_name)
| AVariant (term, _) -> "@variant"::(ident_names term.term_name)
- | AExtended(_,_,(_,name,_,_,_)) -> [Printf.sprintf "@%s" name]
+ | AExtended(_,_,{ext_name}) -> [Printf.sprintf "@%s" ext_name]
| _ -> [] (* TODO : add some more names ? *)
(** This is used to give the name of the property that the user can give
@@ -457,7 +457,7 @@ 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(_,(_,name,_,_,_)) -> [ Printf.sprintf "@%s" name ]
+ | Property.IPExtended(_,{ext_name}) -> [ Printf.sprintf "@%s" ext_name ]
| Property.IPCodeAnnot (_,_, ca) -> code_annot_names ca
| Property.IPComplete (_, _,_,lb) ->
let kind_name = "@complete_behaviors" in
@@ -630,7 +630,7 @@ let property_hints hs = function
List.iter (add_required hs) ps
| Property.IPPredicate(_,_,_,ipred) ->
List.iter (add_hint hs) ipred.ip_content.pred_name
- | Property.IPExtended(_,(_,name,_,_,_)) -> List.iter (add_hint hs) [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 *)