From 5ec2cfd0d3d08b3ea678fdc815dc11b0a0aeae1b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 18 Mar 2024 15:53:58 +0100
Subject: [PATCH] [logic/kernel] introducing modules in AST and IP
---
src/kernel_internals/typing/mergecil.ml | 206 ++++++++++--------
src/kernel_services/ast_data/annotations.ml | 5 +-
src/kernel_services/ast_data/cil_types.ml | 1 +
src/kernel_services/ast_data/property.ml | 84 ++++---
src/kernel_services/ast_data/property.mli | 13 +-
.../ast_data/property_status.ml | 4 +-
.../ast_printing/cil_printer.ml | 10 +-
.../ast_printing/cil_types_debug.ml | 4 +
.../ast_printing/description.ml | 4 +-
src/kernel_services/ast_queries/ast_diff.ml | 2 +-
src/kernel_services/ast_queries/cil.ml | 19 +-
.../ast_queries/cil_datatype.ml | 14 +-
src/kernel_services/ast_queries/file.ml | 2 +-
.../ast_queries/logic_utils.ml | 16 +-
src/plugins/eva/api/general_requests.ml | 3 +-
src/plugins/eva/gui/gui_eval.ml | 2 +-
src/plugins/gui/design.ml | 3 +
src/plugins/gui/filetree.ml | 1 +
src/plugins/gui/property_navigator.ml | 11 +-
src/plugins/metrics/metrics_cilast.ml | 2 +-
src/plugins/metrics/metrics_pivot.ml | 4 +
src/plugins/report/classify.ml | 2 +-
src/plugins/server/kernel_properties.ml | 2 +
src/plugins/wp/LogicUsage.ml | 9 +-
src/plugins/wp/cfgCalculus.ml | 2 +-
src/plugins/wp/cfgGenerator.ml | 2 +
src/plugins/wp/wpPropId.ml | 7 +-
27 files changed, 259 insertions(+), 175 deletions(-)
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 61b53f17a3c..b4d19c325b8 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -858,6 +858,9 @@ let rec global_annot_without_irrelevant_attributes ga =
| Daxiomatic(n,l,attr,loc) ->
Daxiomatic(n,List.map global_annot_without_irrelevant_attributes l,
drop_attributes_for_merge attr,loc)
+ | Dmodule(n,l,attr,loc) ->
+ Dmodule(n,List.map global_annot_without_irrelevant_attributes l,
+ drop_attributes_for_merge attr,loc)
| Dlemma (id,labs,typs,st,attr,loc) ->
Dlemma (id,labs,typs,st,drop_attributes_for_merge attr,loc)
| Dtype (lti,loc) ->
@@ -896,6 +899,11 @@ let rec global_annot_pass1 g =
ignore (PlainMerging.getNode laEq laSyn !currentFidx id (id,decls)
(Some (l,!currentDeclIdx)));
List.iter global_annot_pass1 decls
+ | Dmodule(id,decls,_,l) ->
+ Current_loc.set l;
+ ignore (PlainMerging.getNode laEq laSyn !currentFidx id (id,decls)
+ (Some (l,!currentDeclIdx)));
+ List.iter global_annot_pass1 decls
| Dfun_or_pred (li,l) ->
let mynode =
LogicMerging.getNode
@@ -1712,79 +1720,79 @@ let oneFilePass1 (f:file) : unit =
let iter g =
let<> UpdatedCurrentLoc = Cil_datatype.Global.loc g in
match g with
- | GVarDecl (vi, l) | GVar (vi, _, l) | GFunDecl (_, vi, l)->
- incr currentDeclIdx;
- if vi.vstorage <> Static then begin
- matchVarinfo ~fromGFun:false vi (l, !currentDeclIdx);
- end
+ | GVarDecl (vi, l) | GVar (vi, _, l) | GFunDecl (_, vi, l)->
+ incr currentDeclIdx;
+ if vi.vstorage <> Static then begin
+ matchVarinfo ~fromGFun:false vi (l, !currentDeclIdx);
+ end
- | GFun (fdec, l) ->
- incr currentDeclIdx;
- (* Save the names of the formal arguments *)
- let _, args, _, _ = splitFunctionTypeVI fdec.svar in
- H.add formalNames (!currentFidx, fdec.svar.vname)
- (List.map (fun (n,_,_) -> n) (argsToList args));
- (* Force inline functions to be static. *)
- (* GN: This turns out to be wrong. inline functions are external,
- * unless specified to be static. *)
- (*
- if fdec.svar.vinline && fdec.svar.vstorage = NoStorage then
- fdec.svar.vstorage <- Static;
- *)
- if fdec.svar.vstorage <> Static then begin
- matchVarinfo ~fromGFun:true fdec.svar (l, !currentDeclIdx)
- end else begin
- if fdec.svar.vinline && mergeInlines then
- (* Just create the nodes for inline functions *)
- ignore (PlainMerging.getNode iEq iSyn !currentFidx
- fdec.svar.vname fdec.svar (Some (l, !currentDeclIdx)))
- end
- (* Make nodes for the defined type and structure tags *)
- | GType (t, l) ->
- incr currentDeclIdx;
- t.treferenced <- false;
- if t.tname <> "" then (* The empty names are just for introducing
- * undefined comp tags *)
- ignore (PlainMerging.getNode tEq tSyn !currentFidx t.tname t
- (Some (l, !currentDeclIdx)))
- else begin (* Go inside and clean the referenced flag for the
- * declared tags *)
- match t.ttype with
- TComp (ci, _ ) ->
- ci.creferenced <- false;
- (* Create a node for it *)
- ignore
- (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci None)
-
- | TEnum (ei, _) ->
- ei.ereferenced <- false;
- ignore
- (EnumMerging.getNode eEq eSyn !currentFidx ei ei None)
-
- | _ -> (Kernel.fatal "Anonymous Gtype is not TComp")
- end
+ | GFun (fdec, l) ->
+ incr currentDeclIdx;
+ (* Save the names of the formal arguments *)
+ let _, args, _, _ = splitFunctionTypeVI fdec.svar in
+ H.add formalNames (!currentFidx, fdec.svar.vname)
+ (List.map (fun (n,_,_) -> n) (argsToList args));
+ (* Force inline functions to be static. *)
+ (* GN: This turns out to be wrong. inline functions are external,
+ * unless specified to be static. *)
+ (*
+ if fdec.svar.vinline && fdec.svar.vstorage = NoStorage then
+ fdec.svar.vstorage <- Static;
+ *)
+ if fdec.svar.vstorage <> Static then begin
+ matchVarinfo ~fromGFun:true fdec.svar (l, !currentDeclIdx)
+ end else begin
+ if fdec.svar.vinline && mergeInlines then
+ (* Just create the nodes for inline functions *)
+ ignore (PlainMerging.getNode iEq iSyn !currentFidx
+ fdec.svar.vname fdec.svar (Some (l, !currentDeclIdx)))
+ end
+ (* Make nodes for the defined type and structure tags *)
+ | GType (t, l) ->
+ incr currentDeclIdx;
+ t.treferenced <- false;
+ if t.tname <> "" then (* The empty names are just for introducing
+ * undefined comp tags *)
+ ignore (PlainMerging.getNode tEq tSyn !currentFidx t.tname t
+ (Some (l, !currentDeclIdx)))
+ else begin (* Go inside and clean the referenced flag for the
+ * declared tags *)
+ match t.ttype with
+ TComp (ci, _ ) ->
+ ci.creferenced <- false;
+ (* Create a node for it *)
+ ignore
+ (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci None)
+
+ | TEnum (ei, _) ->
+ ei.ereferenced <- false;
+ ignore
+ (EnumMerging.getNode eEq eSyn !currentFidx ei ei None)
+
+ | _ -> (Kernel.fatal "Anonymous Gtype is not TComp")
+ end
- | GCompTag (ci, l) ->
- incr currentDeclIdx;
- ci.creferenced <- false;
- ignore (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci
- (Some (l, !currentDeclIdx)))
- | GCompTagDecl (ci,_) -> ci.creferenced <- false
- | GEnumTagDecl (ei,_) -> ei.ereferenced <- false
- | GEnumTag (ei, l) ->
- incr currentDeclIdx;
- let orig_name =
- if ei.eorig_name = "" then ei.ename else ei.eorig_name
- in
- ignore (Alpha.newAlphaName ~alphaTable:aeAlpha ~undolist:None
- ~lookupname:orig_name ~data:l);
- ei.ereferenced <- false;
- ignore
- (EnumMerging.getNode eEq eSyn !currentFidx ei ei
- (Some (l, !currentDeclIdx)))
+ | GCompTag (ci, l) ->
+ incr currentDeclIdx;
+ ci.creferenced <- false;
+ ignore (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci
+ (Some (l, !currentDeclIdx)))
+ | GCompTagDecl (ci,_) -> ci.creferenced <- false
+ | GEnumTagDecl (ei,_) -> ei.ereferenced <- false
+ | GEnumTag (ei, l) ->
+ incr currentDeclIdx;
+ let orig_name =
+ if ei.eorig_name = "" then ei.ename else ei.eorig_name
+ in
+ ignore (Alpha.newAlphaName ~alphaTable:aeAlpha ~undolist:None
+ ~lookupname:orig_name ~data:l);
+ ei.ereferenced <- false;
+ ignore
+ (EnumMerging.getNode eEq eSyn !currentFidx ei ei
+ (Some (l, !currentDeclIdx)))
| GAnnot (gannot, _) ->
- incr currentDeclIdx;
- global_annot_pass1 gannot
+ incr currentDeclIdx;
+ global_annot_pass1 gannot
| GText _ | GPragma _ | GAsm _ -> ()
in
List.iter iter f.globals
@@ -2194,7 +2202,9 @@ class renameInlineVisitorClass = object(self)
end
let renameInlinesVisitor = new renameInlineVisitorClass
-let rec logic_annot_pass2 ~in_axiomatic g a =
+type context = Toplevel | InAxiomatic | InModule
+
+let rec logic_annot_pass2 context g a =
let open Current_loc.Operators in
let<> UpdatedCurrentLoc = Cil_datatype.Global_annotation.loc a in
match a with
@@ -2202,18 +2212,18 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
begin
match LogicMerging.findReplacement true lfEq !currentFidx li with
| None ->
- if not in_axiomatic then
+ if context = Toplevel then
mergePushGlobals (visitCilGlobal renameVisitor g);
Logic_utils.add_logic_function li;
| Some _ -> ()
(* FIXME: should we perform same actions
- as the case Dlogic_reads above ? *)
+ as the case Dlogic_reads above ? *)
end
| Dtype (t, _) ->
begin
match PlainMerging.findReplacement true ltEq !currentFidx t.lt_name with
| None ->
- if not in_axiomatic then
+ if context = Toplevel then
mergePushGlobals (visitCilGlobal renameVisitor g);
let def =
(PlainMerging.find_eq_table ltEq (!currentFidx,t.lt_name)).ndata
@@ -2231,7 +2241,7 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
begin
match LogicMerging.findReplacement true lfEq !currentFidx li with
| None ->
- if in_axiomatic then Kernel.abort ~current:true
+ if context <> Toplevel then Kernel.abort ~current:true
"nested axiomatics are not allowed in ACSL";
mergePushGlobals (visitCilGlobal renameVisitor g);
Logic_utils.add_logic_function
@@ -2243,13 +2253,13 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
match LogicMerging.findReplacement true lfEq !currentFidx n with
| None ->
let g = visitCilGlobal renameVisitor g in
- if not in_axiomatic then
+ if context = Toplevel then
mergePushGlobals g;
Logic_utils.add_logic_function
(LogicMerging.find_eq_table lfEq (!currentFidx,n)).ndata
| Some _ -> ()
end
- | Dmodel_annot (mf, l) ->
+ | Dmodel_annot (mf,l) ->
begin
match
ModelMerging.findReplacement
@@ -2263,8 +2273,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
mfEq (!currentFidx,(mf'.mi_name,mf'.mi_base_type))
in
(* Adds a new representative. Do not replace directly
- my_node, as there might be some pointers to it from
- other files.
+ my_node, as there might be some pointers to it from
+ other files.
*)
let my_node' = { my_node with ndata = mf' } in
my_node.nrep <- my_node'; (* my_node' represents my_node *)
@@ -2275,7 +2285,7 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
(!currentFidx,(mf'.mi_name,mf'.mi_base_type))
my_node';
end;
- if not in_axiomatic then begin
+ if context = Toplevel then begin
mergePushGlobals [GAnnot (Dmodel_annot(mf',l),l)];
end;
Logic_env.add_model_field
@@ -2287,11 +2297,11 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
begin
match PlainMerging.findReplacement true llEq !currentFidx n with
None ->
- if not in_axiomatic then
+ if context = Toplevel then
mergePushGlobals (visitCilGlobal renameVisitor g)
| Some _ -> ()
end
- | Dvolatile(vi, rd, wr, attr, loc) ->
+ | Dvolatile(vi,rd,wr,attr,loc) ->
let is_representative id =
Option.is_none
(VolatileMerging.findReplacement true lvEq !currentFidx id)
@@ -2345,10 +2355,32 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
begin
match PlainMerging.findReplacement true laEq !currentFidx n with
None ->
- if in_axiomatic then Kernel.abort ~current:true
+ begin match context with
+ | Toplevel -> ()
+ | InAxiomatic ->
+ Kernel.abort ~current:true
"nested axiomatics are not allowed in ACSL";
+ | InModule ->
+ Kernel.abort ~current:true
+ "mixed axiomatics and modules are not allowed in ACSL";
+ end ;
+ mergePushGlobals (visitCilGlobal renameVisitor g);
+ List.iter (logic_annot_pass2 InAxiomatic g) l
+ | Some _ -> ()
+ end
+ | Dmodule(n,l,_,loc) ->
+ begin
+ Current_loc.set loc;
+ match PlainMerging.findReplacement true laEq !currentFidx n with
+ None ->
+ begin match context with
+ | Toplevel | InModule -> ()
+ | InAxiomatic ->
+ Kernel.abort ~current:true
+ "mixed axiomatics and modules are not allowed in ACSL";
+ end ;
mergePushGlobals (visitCilGlobal renameVisitor g);
- List.iter (logic_annot_pass2 ~in_axiomatic:true g) l
+ List.iter (logic_annot_pass2 InModule g) l
| Some _ -> ()
end
| Dextended(ext, _, _) ->
@@ -2356,7 +2388,7 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
| None -> mergePushGlobals (visitCilGlobal renameVisitor g);
| Some _ -> ())
-let global_annot_pass2 g a = logic_annot_pass2 ~in_axiomatic:false g a
+let global_annot_pass2 g a = logic_annot_pass2 Toplevel g a
(* sm: First attempt at a semantic checksum for function bodies.
* Ideally, two function's checksums would be equal only when their
@@ -2972,8 +3004,8 @@ let oneFilePass2 (f: file) =
end
| GCompTagDecl (ci, _) -> begin
(* This is here just to introduce an undefined
- * structure. But maybe the structure was defined
- * already. *)
+ * structure. But maybe the structure was defined
+ * already. *)
(* Do not increment currentDeclIdx because it is not incremented in
* pass 1*)
if H.mem emittedCompDecls ci.cname then
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index db1b59e51d9..c2f26d3a55a 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1690,7 +1690,7 @@ let rec remove_declared_global_annot logic_vars = function
| Dvolatile _ | Dtype _ | Dlemma _ | Dmodel_annot _
| Dextended _ ->
logic_vars
- | Daxiomatic (_,l,_, _) ->
+ | Daxiomatic (_,l,_, _) | Dmodule (_,l,_, _) ->
List.fold_left remove_declared_global_annot logic_vars l
let remove_declared_global c_vars logic_vars = function
@@ -1806,7 +1806,8 @@ let logic_info_of_global s =
let rec check_one acc = function
| Dfun_or_pred(li,_) | Dinvariant(li,_) | Dtype_annot(li,_) ->
check_logic_info li acc
- | Daxiomatic (_,l, _, _) -> List.fold_left check_one acc l
+ | Daxiomatic (_,l, _, _) | Dmodule (_,l, _, _) ->
+ List.fold_left check_one acc l
| Dtype _ | Dvolatile _ | Dlemma _ | Dmodel_annot _
| Dextended _
-> acc
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index e144f4363da..ff8cade0ca3 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1800,6 +1800,7 @@ and global_annotation =
* attributes * location
(** associated terms, reading function, writing function *)
| Daxiomatic of string * global_annotation list * attributes * location
+ | Dmodule of string * global_annotation list * attributes * location
| Dtype of logic_type_info * location (** declaration of a logic type. *)
| Dlemma of
string * logic_label list * string list *
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 1e5f0f1fdd9..b1460dbef17 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -123,6 +123,12 @@ and identified_axiomatic = {
iax_attrs : attributes;
}
+and identified_module = {
+ im_name : string;
+ im_props : identified_property list;
+ im_attrs : attributes;
+}
+
and identified_lemma = {
il_name : string;
il_labels : logic_label list;
@@ -161,6 +167,7 @@ and identified_property =
| IPPredicate of identified_predicate
| IPExtended of identified_extended
| IPAxiomatic of identified_axiomatic
+ | IPModule of identified_module
| IPLemma of identified_lemma
| IPBehavior of identified_behavior
| IPComplete of identified_complete
@@ -234,7 +241,7 @@ let get_kinstr = function
| IPFrom {if_kinstr=ki}
| IPReachable {ir_kinstr=ki}
| IPDecrease {id_kinstr=ki} -> ki
- | IPAxiomatic _
+ | IPAxiomatic _ | IPModule _
| IPLemma _ -> Kglobal
| IPOther {io_loc} -> ki_of_o_loc io_loc
| IPExtended {ie_loc} -> ki_of_e_loc ie_loc
@@ -261,7 +268,7 @@ let get_kf = function
| IPFrom {if_kf=kf}
| IPDecrease {id_kf=kf}
| IPPropertyInstance {ii_kf=kf} -> Some kf
- | IPAxiomatic _
+ | IPAxiomatic _ | IPModule _
| IPLemma _ -> None
| IPReachable {ir_kf} -> ir_kf
| IPExtended {ie_loc} -> kf_of_loc_e ie_loc
@@ -271,9 +278,9 @@ let get_kf = function
let get_ir p =
let get_pp = function
| IPPredicate {ip_kind = PKRequires _ | PKAssumes _ | PKTerminates }
- | IPAxiomatic _ | IPLemma _ | IPComplete _ | IPDisjoint _ | IPCodeAnnot _
- | IPAllocation _ | IPDecrease _ | IPPropertyInstance _ | IPOther _
- | IPTypeInvariant _ | IPGlobalInvariant _
+ | IPAxiomatic _ | IPModule _ | IPLemma _ | IPComplete _ | IPDisjoint _
+ | IPCodeAnnot _ | IPAllocation _ | IPDecrease _ | IPPropertyInstance _
+ | IPOther _ | IPTypeInvariant _ | IPGlobalInvariant _
-> Before
| IPPredicate _ | IPAssigns _ | IPFrom _ | IPExtended _ | IPBehavior _
-> After
@@ -302,6 +309,7 @@ let rec get_names = function
| IPPredicate ip -> (Logic_const.pred_of_id_pred ip.ip_pred).pred_name
| IPExtended { ie_ext = {ext_name = name} }
| IPAxiomatic { iax_name = name }
+ | IPModule { im_name = name }
| IPLemma { il_name = name }
| IPBehavior { ib_bhv = {b_name = name} }
| IPTypeInvariant { iti_name = name }
@@ -355,6 +363,10 @@ let rec location = function
(match iax_props with
| [] -> Cil_datatype.Location.unknown
| p :: _ -> location p)
+ | IPModule {im_props} ->
+ (match im_props with
+ | [] -> Cil_datatype.Location.unknown
+ | p :: _ -> location p)
| IPLemma {il_loc} -> il_loc
| IPExtended {ie_ext={ext_loc}} -> ext_loc
| IPOther {io_loc} -> loc_of_loc_o io_loc
@@ -388,6 +400,7 @@ let get_behavior = function
| IPAssigns {ias_bhv=Id_loop _}
| IPFrom {if_bhv=Id_loop _}
| IPAxiomatic _
+ | IPModule _
| IPExtended _
| IPLemma _
| IPCodeAnnot _
@@ -423,6 +436,7 @@ let get_for_behaviors = function
end
| IPAxiomatic _
+ | IPModule _
| IPExtended _
| IPLemma _
| IPComplete _
@@ -457,7 +471,7 @@ let rec has_status = function
| IPCodeAnnot {ica_ca={annot_content}} -> has_status_ca annot_content
| IPPropertyInstance {ii_ip} -> has_status ii_ip
| IPOther _ | IPReachable _
- | IPAxiomatic _ | IPBehavior _
+ | IPAxiomatic _ | IPModule _ | IPBehavior _
| IPDisjoint _ | IPComplete _
| IPAssigns _ | IPFrom _
| IPAllocation _ | IPDecrease _ | IPLemma _
@@ -482,6 +496,7 @@ let rec pretty_ip fmt = function
Cil_printer.pp_identified_predicate ip_pred
| IPExtended {ie_ext} -> Cil_printer.pp_extended fmt ie_ext
| IPAxiomatic {iax_name} -> Format.fprintf fmt "axiomatic@ %s" iax_name
+ | IPModule {im_name} -> Format.fprintf fmt "module@ %s" im_name
| IPLemma {il_name; il_pred} ->
Format.fprintf fmt "%a@ %s"
Cil_printer.pp_lemma_kind il_pred.tp_kind il_name
@@ -546,7 +561,8 @@ let rec hash_ip =
in
function
| IPPredicate {ip_pred=x} -> Hashtbl.hash (1, x.ip_id)
- | IPAxiomatic {iax_name=x} -> Hashtbl.hash (3, (x:string))
+ | IPAxiomatic {iax_name=x}
+ | IPModule {im_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} ->
@@ -637,6 +653,7 @@ include Datatype.Make_with_collections
| IPExtended {ie_ext={ext_id=i1}}, IPExtended {ie_ext={ext_id=i2}} ->
Datatype.Int.equal i1 i2
| IPAxiomatic {iax_name=s1}, IPAxiomatic {iax_name=s2}
+ | IPModule {im_name=s1}, IPModule {im_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} ->
@@ -676,7 +693,7 @@ include Datatype.Make_with_collections
IPPropertyInstance {ii_kf=kf2;ii_stmt=s2;ii_ip=ip2} ->
Kernel_function.equal kf1 kf2 &&
Stmt.equal s1 s2 && equal ip1 ip2
- | (IPPredicate _ | IPExtended _ | IPAxiomatic _ | IPLemma _
+ | (IPPredicate _ | IPExtended _ | IPAxiomatic _ | IPModule _ | IPLemma _
| IPCodeAnnot _ | IPComplete _ | IPDisjoint _ | IPAssigns _
| IPFrom _ | IPDecrease _ | IPBehavior _ | IPReachable _
| IPAllocation _ | IPOther _ | IPPropertyInstance _
@@ -736,6 +753,7 @@ include Datatype.Make_with_collections
else
n
| IPAxiomatic {iax_name=s1}, IPAxiomatic {iax_name=s2}
+ | IPModule {im_name=s1}, IPModule {im_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} ->
@@ -754,7 +772,7 @@ include Datatype.Make_with_collections
if c <> 0 then c else compare ip1 ip2
| (IPPredicate _ | IPExtended _ | IPCodeAnnot _ | IPBehavior _ | IPComplete _ |
IPDisjoint _ | IPAssigns _ | IPFrom _ | IPDecrease _ |
- IPReachable _ | IPAxiomatic _ | IPLemma _ |
+ IPReachable _ | IPAxiomatic _ | IPModule _ | IPLemma _ |
IPOther _ | IPAllocation _ | IPPropertyInstance _ |
IPTypeInvariant _ | IPGlobalInvariant _) as x, y ->
let nb = function
@@ -762,19 +780,20 @@ include Datatype.Make_with_collections
| IPAssigns _ -> 2
| IPDecrease _ -> 3
| IPAxiomatic _ -> 5
- | IPLemma _ -> 6
- | IPCodeAnnot _ -> 7
- | IPComplete _ -> 8
- | IPDisjoint _ -> 9
- | IPFrom _ -> 10
- | IPBehavior _ -> 11
- | IPReachable _ -> 12
- | IPAllocation _ -> 13
- | IPOther _ -> 14
- | IPPropertyInstance _ -> 15
- | IPTypeInvariant _ -> 16
- | IPGlobalInvariant _ -> 17
- | IPExtended _ -> 18
+ | IPModule _ -> 6
+ | IPLemma _ -> 7
+ | IPCodeAnnot _ -> 8
+ | IPComplete _ -> 9
+ | IPDisjoint _ -> 10
+ | IPFrom _ -> 11
+ | IPBehavior _ -> 12
+ | IPReachable _ -> 13
+ | IPAllocation _ -> 14
+ | IPOther _ -> 15
+ | IPPropertyInstance _ -> 16
+ | IPTypeInvariant _ -> 17
+ | IPGlobalInvariant _ -> 18
+ | IPExtended _ -> 19
in
Datatype.Int.compare (nb x) (nb y)
@@ -793,6 +812,7 @@ module Ordered_by_function = Datatype.Make_with_collections(
let cmp_kind p1 p2 =
let nb = function
| IPAxiomatic _ -> 1
+ | IPModule _ -> 2
| IPLemma _ -> 3
| IPTypeInvariant _ -> 4
| IPGlobalInvariant _ -> 5
@@ -822,6 +842,7 @@ module Ordered_by_function = Datatype.Make_with_collections(
let rec cmp_same_kind p1 p2 =
match (p1,p2) with
| IPAxiomatic { iax_name = n1 }, IPAxiomatic { iax_name = n2 }
+ | IPModule { im_name = n1 }, IPModule { im_name = n2 }
| IPLemma { il_name = n1 }, IPLemma { il_name = n2 }
| IPTypeInvariant { iti_name = n1 }, IPTypeInvariant { iti_name = n2 }
| IPGlobalInvariant { igi_name = n1 },
@@ -910,7 +931,8 @@ let rec short_pretty fmt p = match p with
| IPExtended {ie_ext={ext_name}} -> Format.pp_print_string fmt ext_name
| IPLemma {il_name=n}
| IPTypeInvariant {iti_name=n} | IPGlobalInvariant {igi_name=n}
- | IPAxiomatic {iax_name=n} -> Format.pp_print_string fmt n
+ | IPAxiomatic {iax_name=n} | IPModule {im_name=n} ->
+ Format.pp_print_string fmt n
| IPBehavior {ib_kf; ib_bhv={b_name}} ->
Format.fprintf fmt "behavior %s in function %a"
b_name Kernel_function.pretty ib_kf
@@ -1031,6 +1053,11 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_string iax_name
(Cil_types_debug.pp_list pretty_debug) iax_props
Cil_types_debug.pp_attributes iax_attrs
+ | IPModule {im_name; im_props; im_attrs} ->
+ Format.fprintf fmt "IPModule(%a,%a,%a)"
+ Cil_types_debug.pp_string im_name
+ (Cil_types_debug.pp_list pretty_debug) im_props
+ Cil_types_debug.pp_attributes im_attrs
| IPLemma {il_name; il_labels; il_args; il_pred; il_attrs; il_loc} ->
Format.fprintf fmt "IPLemma(%a,%a,%a,%a,%a,%a)"
Cil_types_debug.pp_string il_name
@@ -1218,7 +1245,7 @@ struct
| IPReachable {ir_kf=Some kf; ir_kinstr=Kstmt s; ir_program_point=After} ->
[ K kf ; A "reachable_after" ; S s ]
- | IPAxiomatic _ -> []
+ | IPAxiomatic _ | IPModule _ -> []
| IPLemma {il_name=name; il_pred=p} ->
let a = Cil_printer.ident_of_lemma p.tp_kind in
[ A a ; A name ; P p.tp_statement ]
@@ -1493,6 +1520,9 @@ let ip_of_global_annotation a =
| Daxiomatic(iax_name, l, iax_attrs, _) ->
let iax_props = List.fold_left aux [] l in
IPAxiomatic {iax_name; iax_props; iax_attrs} :: (iax_props @ acc)
+ | Dmodule(im_name, l, im_attrs, _) ->
+ let im_props = List.fold_left aux [] l in
+ IPModule {im_name; im_props; im_attrs} :: (im_props @ acc)
| Dlemma(il_name, il_labels, il_args, il_pred, il_attrs, il_loc) ->
ip_lemma {il_name; il_labels; il_args; il_pred; il_attrs; il_loc} :: acc
| Dinvariant(l, igi_loc) ->
@@ -1529,9 +1559,3 @@ let ip_of_global_annotation_single a = match ip_of_global_annotation a with
| ip :: _ ->
(* the first one is the good one, see ip_of_global_annotation *)
Some ip
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index f957ff21d99..caff84ad582 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -154,6 +154,12 @@ and identified_axiomatic = {
iax_attrs : attributes;
}
+and identified_module = {
+ im_name : string;
+ im_props : identified_property list;
+ im_attrs : attributes;
+}
+
and identified_lemma = {
il_name : string;
il_labels : logic_label list;
@@ -195,6 +201,7 @@ and identified_property = private
| IPPredicate of identified_predicate
| IPExtended of identified_extended
| IPAxiomatic of identified_axiomatic
+ | IPModule of identified_module
| IPLemma of identified_lemma
| IPBehavior of identified_behavior
| IPComplete of identified_complete
@@ -548,9 +555,3 @@ sig
(** returns the basename of the property. *)
end
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 9edd052f73c..be7acef29cd 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -525,7 +525,7 @@ and unsafe_emit_and_get e ~hyps ~auto ppt ?(distinct=false) s =
| Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
| Property.IPDisjoint _ | Property.IPAssigns _ | Property.IPFrom _
| Property.IPAllocation _ | Property.IPDecrease _ | Property.IPBehavior _
- | Property.IPAxiomatic _ | Property.IPLemma _
+ | Property.IPAxiomatic _ | Property.IPModule _ | Property.IPLemma _
| Property.IPTypeInvariant _ | Property.IPGlobalInvariant _
| Property.IPExtended _ ->
Kernel.fatal "unregistered property %a" Property.pretty ppt
@@ -693,7 +693,7 @@ and get_status ?(must_register=true) ppt =
| Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
| Property.IPDisjoint _ | Property.IPAssigns _ | Property.IPFrom _
| Property.IPDecrease _ | Property.IPAllocation _
- | Property.IPAxiomatic _ | Property.IPLemma _
+ | Property.IPAxiomatic _ | Property.IPModule _ | Property.IPLemma _
| Property.IPTypeInvariant _ | Property.IPGlobalInvariant _ ->
Kernel.fatal "trying to get status of unregistered property `%a'.\n\
That is forbidden (kernel invariant broken)."
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 75c2da8a093..4cfa94c087b 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3407,8 +3407,14 @@ class cil_printer () = object (self)
| Daxiomatic(id,decls,_attr, _) ->
(* attributes are meant to be purely internal for now. *)
fprintf fmt "@[<v 2>@[%a %s {@]@\n%a}@]@\n"
- self#pp_acsl_keyword "axiomatic"
- id
+ self#pp_acsl_keyword "axiomatic" id
+ (Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
+ self#global_annotation)
+ decls
+ | Dmodule(id,decls,_attr, _) ->
+ (* attributes are meant to be purely internal for now. *)
+ fprintf fmt "@[<v 2>@[%a %s {@]@\n%a}@]@\n"
+ self#pp_acsl_keyword "module" id
(Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
self#global_annotation)
decls
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 12e2557c256..745b403090a 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -971,6 +971,10 @@ and pp_global_annotation fmt = function
Format.fprintf fmt "Daxiomatic(%a,%a,%a,%a)" pp_string string
(pp_list pp_global_annotation) global_annotation_list
pp_attributes attributes pp_location location
+ | Dmodule(string,global_annotation_list,attributes,location) ->
+ Format.fprintf fmt "Dmodule(%a,%a,%a,%a)" pp_string string
+ (pp_list pp_global_annotation) global_annotation_list
+ pp_attributes attributes pp_location location
| Dtype(logic_type_info,location) ->
Format.fprintf fmt "Dtype(%a,%a)" pp_logic_type_info logic_type_info pp_location location
| Dlemma(string,logic_label_list,string_list,predicate,attributes,location) ->
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index ab7ccf849a4..b827571399f 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -228,6 +228,7 @@ let rec pp_prop kfopt kiopt kloc fmt = function
| 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
+ | IPModule {im_name=s} -> Format.fprintf fmt "Module '%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 {ip_kind; ip_kf; ip_kinstr=Kglobal; ip_pred} ->
@@ -497,7 +498,8 @@ let loop_order = function
let rec ip_order = function
| IPAxiomatic {iax_name=a} -> [I 0;S a]
- | IPLemma {il_name=a} -> [I 1;S a]
+ | IPModule {im_name=a} -> [I 1;S a]
+ | IPLemma {il_name=a} -> [I 2;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]
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 9dc42b8d8cf..749a1f3d111 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -1517,7 +1517,7 @@ let rec gannot_correspondence =
| Dvolatile _ -> ()
(* reading and writing function themselves will be checked elsewhere. *)
- | Daxiomatic(_,l,_,_) ->
+ | Daxiomatic(_,l,_,_) | Dmodule(_,l,_,_) ->
List.iter gannot_correspondence l
| Dtype (ti,loc) -> ignore (logic_type_correspondence ~loc ti empty_env)
| Dlemma _ -> ()
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 1b3ace6387f..dc3aa585729 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -428,7 +428,7 @@ let attributeHash: (string, attributeClass) Hashtbl.t =
"selectany"; "allocate"; "nothrow"; "novtable"; "property";
"uuid"; "align" ];
List.iter (fun a -> Hashtbl.add table a (AttrFunType false))
- [ "format"; "regparm"; "longcall"; "noinline"; "always_inline";];
+ [ "format"; "regparm"; "longcall"; "noinline"; "always_inline"; ];
List.iter (fun a -> Hashtbl.add table a (AttrFunType true))
[ "stdcall";"cdecl"; "fastcall"; "noreturn"];
List.iter (fun a -> Hashtbl.add table a AttrType)
@@ -1916,12 +1916,13 @@ and childrenAnnotation vis a =
Dvolatile(tset',rvi',wvi',attr',loc)
else a
| Daxiomatic(id,l,attr,loc) ->
- (*
- Format.eprintf "cil.visitCilAnnotation on axiomatic %s@." id;
- *)
let l' = Extlib.map_no_copy (visitCilAnnotation vis) l in
let attr' = visitCilAttributes vis attr in
if l' != l || attr != attr' then Daxiomatic(id,l',attr',loc) else a
+ | Dmodule(id,l,attr,loc) ->
+ let l' = Extlib.map_no_copy (visitCilAnnotation vis) l in
+ let attr' = visitCilAttributes vis attr in
+ if l' != l || attr != attr' then Dmodule(id,l',attr',loc) else a
| Dextended (e,attr,loc) ->
let e' = visitCilExtended vis e in
let attr' = visitCilAttributes vis attr in
@@ -2177,7 +2178,7 @@ and visitCilStmt (vis:cilVisitor) (s: stmt) : stmt =
let last = mkStmt ~ghost:res.ghost res.skind in
let block = mkBlockNonScoping (List.map make instr_list @ [ last ]) in
block.battrs <- addAttribute (Attr (vis_tmp_attr, [])) block.battrs;
- (* Make our statement contain the instructions to prepend *)
+ (* Make our statement contain the instructions to prepend *)
res.skind <- Block block;
vis#pop_stmt s; res
@@ -4132,7 +4133,7 @@ and bitsSizeOf t =
raise
(SizeOfError
(Format.sprintf "abstract type '%s'" (compFullName comp), t))
- | TComp ({cfields=Some[]}, _) when acceptEmptyCompinfo () ->
+ | TComp ({cfields=Some[]}, _) when acceptEmptyCompinfo() ->
find_sizeof t (fun () -> t,0)
| TComp ({cfields=Some[]} as comp,_) ->
find_sizeof t
@@ -5254,7 +5255,7 @@ let mapGlobals (fl: file)
let global_annotation_attributes = function
| Dfun_or_pred ({l_var_info = { lv_attr }}, _) -> lv_attr
| Dvolatile (_,_,_,attrs,_) -> attrs
- | Daxiomatic (_,_,attrs,_) -> attrs
+ | Daxiomatic (_,_,attrs,_) | Dmodule(_,_,attrs,_) -> attrs
| Dtype ({ lt_attr }, _) -> lt_attr
| Dlemma (_,_,_,_,attrs,_) -> attrs
| Dinvariant ({l_var_info = { lv_attr }}, _) -> lv_attr
@@ -6693,14 +6694,14 @@ let rec has_flexible_array_member t =
let is_flexible_array t =
match unrollType t with
| TArray (_, None, _) -> true
- | TArray (_, Some z, _) -> (msvcMode () || gccMode ()) && isZero z
+ | TArray (_, Some z, _) -> (msvcMode() || gccMode()) && isZero z
| _ -> false
in
match unrollType t with
| TComp ({ cfields = Some ((_::_) as l) },_) ->
let last = (Extlib.last l).ftype in
is_flexible_array last ||
- ((gccMode () || msvcMode ()) && has_flexible_array_member last)
+ ((gccMode() || msvcMode()) && has_flexible_array_member last)
| _ -> false
(* last_field is [true] if the given type is the type of the last field of
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index f11de6f809e..bd87f8264e0 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2219,6 +2219,10 @@ module Global_annotation = struct
if res = 0 then Attributes.compare attr1 attr2 else res
| Daxiomatic _, _ -> -1
| _, Daxiomatic _ -> 1
+ | Dmodule (m1,_,_,_), Dmodule (m2,_,_,_) ->
+ String.compare m1 m2
+ | Dmodule _, _ -> -1
+ | _, Dmodule _ -> 1
| Dtype(t1,_), Dtype(t2,_) -> Logic_type_info.compare t1 t2
| Dtype _, _ -> -1
| _, Dtype _ -> 1
@@ -2250,6 +2254,7 @@ module Global_annotation = struct
| Daxiomatic (_,[],_,_) -> 5
(* Empty axiomatic is weird but authorized. *)
| Daxiomatic (_,g::_,_,_) -> 5 * hash g
+ | Dmodule (m,_,_,_) -> 5 * Datatype.String.hash m
| Dtype (t,_) -> 7 * Logic_type_info.hash t
| Dlemma(n,_,_,_,_,_) -> 11 * Datatype.String.hash n
| Dinvariant(l,_) -> 13 * Logic_info.hash l
@@ -2263,6 +2268,7 @@ module Global_annotation = struct
let loc = function
| Dfun_or_pred(_, loc)
| Daxiomatic(_, _, _, loc)
+ | Dmodule(_, _, _, loc)
| Dtype (_, loc)
| Dlemma(_, _, _, _, _, loc)
| Dinvariant(_, loc)
@@ -2273,7 +2279,7 @@ module Global_annotation = struct
let attr = function
| Dfun_or_pred({ l_var_info = { lv_attr }}, _) -> lv_attr
- | Daxiomatic(_, _, attr, _) -> attr
+ | Daxiomatic(_, _, attr, _) | Dmodule(_, _, attr, _) -> attr
| Dtype ({lt_attr}, _) -> lt_attr
| Dlemma(_, _, _, _, attr, _) -> attr
| Dinvariant({ l_var_info = { lv_attr }}, _) -> lv_attr
@@ -2682,9 +2688,3 @@ module Syntactic_scope =
(* -------------------------------------------------------------------------- *)
let clear_caches () = List.iter (fun f -> f ()) !clear_caches
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 6e4d2204269..d9b52fed187 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -1255,7 +1255,7 @@ let extract_logic_infos g =
| Dfun_or_pred (li,_) | Dinvariant (li,_) | Dtype_annot (li,_) -> li :: acc
| Dvolatile _ | Dtype _ | Dlemma _
| Dmodel_annot _ | Dextended _ -> acc
- | Daxiomatic(_,l,_,_) -> List.fold_left aux acc l
+ | Daxiomatic(_,l,_,_) | Dmodule(_,l,_,_) -> List.fold_left aux acc l
in aux [] g
let find_logic_info_decl li =
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 4fbd3210b47..3e298120913 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -739,6 +739,9 @@ let rec add_attribute_glob_annot a g =
| Daxiomatic(n,l,al,loc) ->
Daxiomatic(n,List.map (add_attribute_glob_annot a) l,
Cil.addAttribute a al,loc)
+ | Dmodule(n,l,al,loc) ->
+ Dmodule(n,List.map (add_attribute_glob_annot a) l,
+ Cil.addAttribute a al,loc)
| Dtype(ti,_) -> ti.lt_attr <- Cil.addAttribute a ti.lt_attr; g
| Dlemma(n,labs,t,p,al,l) ->
Dlemma(n,labs,t,p,Cil.addAttribute a al,l)
@@ -1217,6 +1220,9 @@ let rec is_same_global_annotation ga1 ga2 =
| Daxiomatic (id1,ga1,attr1,_), Daxiomatic (id2,ga2,attr2,_) ->
id1 = id2 && is_same_list is_same_global_annotation ga1 ga2
&& is_same_attributes attr1 attr2
+ | Dmodule (id1,ga1,attr1,_), Dmodule (id2,ga2,attr2,_) ->
+ id1 = id2 && is_same_list is_same_global_annotation ga1 ga2
+ && is_same_attributes attr1 attr2
| Dtype (t1,_), Dtype (t2,_) -> is_same_logic_type_info t1 t2
| Dlemma(n1,labs1,typs1,st1,attr1,_),
Dlemma(n2,labs2,typs2,st2,attr2,_) ->
@@ -1233,10 +1239,10 @@ let rec is_same_global_annotation ga1 ga2 =
is_same_opt (fun x y -> x.vname = y.vname) w1 w2 &&
is_same_attributes attr1 attr2
| Dextended(id1,_,_), Dextended(id2,_,_) -> id1 = id2
- | (Dfun_or_pred _ | Daxiomatic _ | Dtype _ | Dlemma _
+ | (Dfun_or_pred _ | Daxiomatic _ | Dmodule _ | Dtype _ | Dlemma _
| Dinvariant _ | Dtype_annot _ | Dmodel_annot _
| Dvolatile _ | Dextended _),
- (Dfun_or_pred _ | Daxiomatic _ | Dtype _ | Dlemma _
+ (Dfun_or_pred _ | Daxiomatic _ | Dmodule _ | Dtype _ | Dlemma _
| Dinvariant _ | Dtype_annot _ | Dmodel_annot _
| Dvolatile _ | Dextended _) -> false
@@ -2670,9 +2676,3 @@ class simplify_const_lval global_find_init = object (self)
end
let () = Cil_datatype.punrollLogicType := unroll_type
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 1f44c023b73..fa5ff5e1979 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -263,7 +263,8 @@ let property_evaluation_point = function
| IPAssigns {ias_kf = kf} | IPFrom {if_kf = kf} ->
Pre kf
| IPPredicate _ | IPComplete _ | IPDisjoint _ | IPDecrease _
- | IPAxiomatic _ | IPLemma _ | IPTypeInvariant _ | IPGlobalInvariant _
+ | IPAxiomatic _ | IPModule _ | IPLemma _
+ | IPTypeInvariant _ | IPGlobalInvariant _
| IPOther _ | IPAllocation _ | IPReachable _ | IPExtended _ | IPBehavior _ ->
raise Not_found
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index 05999668da4..ad9d93edab3 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -38,7 +38,7 @@ let classify_pre_post kf ip =
let open Property in
match ip with
| IPPredicate {ip_kind = PKEnsures (_, Normal)} -> Some (GL_Post kf)
- | IPPredicate {ip_kind=PKEnsures _} | IPAxiomatic _ | IPLemma _
+ | IPPredicate {ip_kind=PKEnsures _} | IPAxiomatic _ | IPModule _ | IPLemma _
| IPTypeInvariant _ | IPGlobalInvariant _
| IPOther _ | IPCodeAnnot _ | IPAllocation _ | IPReachable _
| IPExtended _
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 33403999da9..e728a759797 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -504,6 +504,9 @@ let to_do_on_select
| PIP(IPAxiomatic _ as ip) ->
main_ui#pretty_information "This is an axiomatic.@.";
main_ui#view_original (location ip)
+ | PIP(IPModule _ as ip) ->
+ main_ui#pretty_information "This is an ACSL module.@.";
+ main_ui#view_original (location ip)
| PIP(IPLemma { il_pred } as ip) ->
main_ui#pretty_information "This is a %a.@."
Cil_printer.pp_lemma_kind il_pred.tp_kind;
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index 4543cc17c76..6fbec82d38d 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -316,6 +316,7 @@ module MYTREE = struct
Some (global_name li.l_var_info.lv_name)
| Dvolatile _ -> Some "volatile clause"
| Daxiomatic (s, _, _,_) -> Some (global_name s)
+ | Dmodule (s, _, _,_) -> Some (global_name s)
| Dtype (lti, _) -> Some (global_name lti.lt_name)
| Dlemma (s, _, _, _, _,_) -> Some (global_name s)
| Dinvariant (li, _) -> Some (global_name li.l_var_info.lv_name)
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 5592bd188cd..a8537e8587e 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -133,6 +133,7 @@ module Refreshers: sig
val instances: check
val lemmas: check
val axiomatic: check
+ val modules: check
val typeInvariants: check
val globalInvariants: check
@@ -274,6 +275,8 @@ struct
~hint:"Show lemmas" ()
let axiomatic = add ~name:"Axiomatic" ~default:false
~hint:"Show global axiomatics" ()
+ let modules = add ~name:"Module" ~default:false
+ ~hint:"Show global modules" ()
let instances = add ~name:"Instances"
~hint:"Show properties that are instances of root properties" ()
let typeInvariants = add ~name:"Type invariants"
@@ -387,6 +390,7 @@ struct
terminates.add hb;
stmtSpec.add hb;
axiomatic.add hb;
+ modules.add hb;
lemmas.add hb;
typeInvariants.add hb;
globalInvariants.add hb;
@@ -639,6 +643,7 @@ let make_panel (main_ui:main_window_extension_points) =
| IPTypeInvariant _ -> typeInvariants.get()
| IPGlobalInvariant _ -> globalInvariants.get()
| IPAxiomatic _ -> axiomatic.get () && not (onlyCurrent.get ())
+ | IPModule _ -> modules.get () && not (onlyCurrent.get ())
| IPLemma _ -> lemmas.get ()
| IPComplete _ -> complete_disjoint.get ()
| IPDisjoint _ -> complete_disjoint.get ()
@@ -842,9 +847,3 @@ let extend (main_ui:main_window_extension_points) =
main_ui#register_source_highlighter highlighter
let () = Design.register_extension extend
-
-(*
- Local Variables:
- compile-command: "make -C ../../.."
- End:
-*)
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index f2f587d755f..82c8d0eb87d 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -320,7 +320,7 @@ class slocVisitor ~libc : sloc_visitor = object(self)
match an with
| Dfun_or_pred (li, _) -> li.l_var_info.lv_name
| Dvolatile (_, _, _, _, _) -> " (Volatile) "
- | Daxiomatic (s, _, _, _) -> s
+ | Daxiomatic (s, _, _, _) | Dmodule (s, _, _, _) -> s
| Dtype (lti, _) -> lti.lt_name
| Dlemma (ln, _, _, _, _, _) -> ln
| Dinvariant (toto, _) -> toto.l_var_info.lv_name
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index 11e68d855c3..9cf5c9ac08f 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -97,6 +97,7 @@ let node_of_global_annotation = function
| Dfun_or_pred _ -> "logic_fun_or_pred"
| Dvolatile _ -> "logic_volatile"
| Daxiomatic _ -> "axiomatic"
+ | Dmodule _ -> "module"
| Dtype _ -> "logic_type"
| Dlemma _ -> "logic_lemma"
| Dinvariant _ -> "invariant"
@@ -142,6 +143,7 @@ let name_of_global_annotation = function
| Dinvariant (li, _)
| Dtype_annot (li, _) -> Some (name_of_logic_info li)
| Daxiomatic (name, _, _, _)
+ | Dmodule (name, _, _, _)
| Dtype ({lt_name = name}, _)
| Dlemma (name, _, _, _, _, _)
| Dmodel_annot ({mi_name = name}, _)
@@ -157,6 +159,7 @@ let node_of_property = function
Format.asprintf "%a" Property.pretty_predicate_kind idp.ip_kind
| IPCodeAnnot ica -> node_of_code_annotation_node ica.ica_ca.annot_content
| IPAxiomatic _ -> "axiomatic"
+ | IPModule _ -> "module"
| IPLemma _ -> "lemma"
| IPBehavior _ -> "behavior"
| IPComplete _ -> "complete"
@@ -176,6 +179,7 @@ let names_of_property = function
| Property.IPPredicate idp -> idp.ip_pred.ip_content.tp_statement.pred_name
| IPCodeAnnot _ -> []
| IPAxiomatic _ -> []
+ | IPModule _ -> []
| IPLemma _ -> []
| IPBehavior _ -> []
| IPComplete _ -> []
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 5ff525c353c..b25a011b683 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -431,7 +431,7 @@ let rec monitored_property ip =
| IPDisjoint _ -> true
| IPReachable {ir_kf=None} -> false
| IPReachable {ir_kf=Some _} -> true
- | IPAxiomatic _ -> false
+ | IPAxiomatic _ | IPModule _ -> false
| IPLemma _ -> true
| IPTypeInvariant _ | IPGlobalInvariant _ -> true
| IPOther _ -> true
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index c80c97892fa..bba21be7666 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -78,6 +78,7 @@ struct
let t_global_invariant = t_kind "global_invariant" "Global invariant"
let t_axiomatic = t_kind "axiomatic" "Axiomatic definitions"
+ let t_module = t_kind "module" "Logic module"
let t_axiom = t_kind "axiom" "Logical axiom"
let t_lemma = t_kind "lemma" "Logical lemma"
let t_check_lemma = t_kind "check_lemma" "Logical check lemma"
@@ -101,6 +102,7 @@ struct
end
| IPExtended { ie_ext={ ext_name=_ } } -> t_ext
| IPAxiomatic _ -> t_axiomatic
+ | IPModule _ -> t_module
| IPLemma { il_pred = { tp_kind = Admit } } -> t_axiom
| IPLemma { il_pred = { tp_kind = Assert } } -> t_lemma
| IPLemma { il_pred = { tp_kind = Check } } -> t_check_lemma
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index 7cebbc5d2e4..d454697e775 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -223,7 +223,7 @@ let ip_of_axiomatic g =
| Some ip -> ip
let axiomatic_of_global ~context = function
- | Daxiomatic(name,globals,_,loc) as g ->
+ | (Daxiomatic(name,globals,_,loc) | Dmodule(name,globals,_,loc)) as g ->
let a = {
ax_name = name ;
ax_position = fst loc ;
@@ -234,8 +234,7 @@ let axiomatic_of_global ~context = function
List.iter (populate a ~context) globals ;
a.ax_types <- List.rev a.ax_types ;
a.ax_logics <- List.rev a.ax_logics ;
- a.ax_lemmas <- List.rev a.ax_lemmas ;
- a
+ a.ax_lemmas <- List.rev a.ax_lemmas ; a
| _ -> assert false
let register_logic d section l =
@@ -365,9 +364,9 @@ class visitor =
method! vannotation global =
match global with
- (* --- AXIOMATICS --- *)
+ (* --- AXIOMATICS & MODULES --- *)
- | Daxiomatic _ ->
+ | Daxiomatic _ | Dmodule _ ->
begin
let pf = database.proofcontext in
let ax = axiomatic_of_global ~context:pf global in
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index ec6b9b0cf75..b296586692f 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -99,7 +99,7 @@ let is_active_mode ~mode ~goal (p: Property.t) =
| IPComplete _ | IPDisjoint _ -> is_default_bhv mode
| IPOther _ -> true
| IPFrom _ | IPGlobalInvariant _ | IPTypeInvariant _
- | IPAxiomatic _ | IPLemma _
+ | IPAxiomatic _ | IPModule _ | IPLemma _
| IPExtended _ | IPBehavior _
| IPReachable _ | IPPropertyInstance _
-> assert false (* n/a *)
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index f9c0980cbdc..de3e46df8be 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -134,6 +134,8 @@ let rec strategy_ip model pool target =
add_lemma_task pool (LogicUsage.logic_lemma il_name)
| IPAxiomatic { iax_props } ->
List.iter (strategy_ip model pool) iax_props
+ | IPModule { im_props } ->
+ List.iter (strategy_ip model pool) im_props
| IPBehavior { ib_kf = kf ; ib_bhv = bhv } ->
add_fun_task model pool ~kf ~bhvs:[bhv] ()
| IPPredicate { ip_kf = kf ; ip_kind ; ip_kinstr = ki } ->
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 0d00f2dc2ef..15abb61bcfb 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -470,6 +470,7 @@ let user_prop_names p =
| IPFrom _
| IPAllocation _
| IPAxiomatic _
+ | IPModule _
| IPBehavior _
| IPReachable _
| IPPropertyInstance _
@@ -659,9 +660,9 @@ let property_hints hs =
| 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 _ -> ()
+ | IPFrom _ | IPDecrease _ | IPPropertyInstance _
+ | IPReachable _ | IPAxiomatic _ | IPModule _ | IPOther _
+ | IPTypeInvariant _ | IPGlobalInvariant _ -> ()
let prop_id_keys p =
begin
--
GitLab