From d110f32fc23a1c439716023bc91b6893743a0276 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 5 Nov 2019 14:30:24 +0100
Subject: [PATCH] [ghost] Warns on ghost qualification of an already ghost
element
---
src/kernel_internals/typing/cabs2cil.ml | 11 +++++++++++
.../plugin_entry_points/kernel.ml | 3 +++
.../plugin_entry_points/kernel.mli | 4 ++++
.../syntax/oracle/ghost_cv_valid_ref.res.oracle | 16 ++++++++--------
.../syntax/oracle/ghost_cv_valid_use.res.oracle | 16 ++++++++--------
.../syntax/oracle/ghost_cv_var_decl.1.res.oracle | 4 ++--
6 files changed, 36 insertions(+), 18 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 3f3d36715e0..fdfcd39735b 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4799,6 +4799,17 @@ and makeVarInfoCabs
we do it afterwards *)
bt (A.PARENTYPE(attrs, ndt, a)) in
(*Format.printf "Got yp:%a->%a(%a)@." d_type bt d_type vtype d_attrlist nattr;*)
+ if not isgenerated && ghost then begin
+ if hasAttribute "ghost" (Cil.typeAttrs vtype) then
+ Kernel.warning
+ ~wkey:Kernel.wkey_ghost_already_ghost ~once:true ~current:true
+ "'%s' is already ghost" n;
+ if isArrayType vtype then
+ if hasAttribute "ghost" (Cil.typeAttrs (typeOf_array_elem vtype)) then
+ Kernel.warning
+ ~wkey:Kernel.wkey_ghost_already_ghost ~once:true ~current:true
+ "'%s' elements are already ghost" n;
+ end ;
if inline && not (isFunctionType vtype) then
Kernel.error ~once:true ~current:true "inline for a non-function: %s" n;
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index cce382d5d4e..17d8e601999 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -133,6 +133,9 @@ let dkey_visitor = register_category "visitor"
let wkey_annot_error = register_warn_category "annot-error"
let () = set_warn_status wkey_annot_error Log.Wabort
+let wkey_ghost_already_ghost = register_warn_category "ghost:already-ghost"
+let () = set_warn_status wkey_ghost_already_ghost Log.Wfeedback
+
let wkey_ghost_bad_use = register_warn_category "ghost:bad-use"
let () = set_warn_status wkey_ghost_bad_use Log.Werror
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index bbfdc8097ff..402b5bf5f0e 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -132,6 +132,10 @@ val dkey_visitor: category
val wkey_annot_error: warn_category
(** error in annotation. If only a warning, annotation will just be ignored. *)
+val wkey_ghost_already_ghost: warn_category
+(** ghost element is qualified with \ghost while this is already the case
+ by default *)
+
val wkey_ghost_bad_use: warn_category
(** error in ghost code *)
diff --git a/tests/syntax/oracle/ghost_cv_valid_ref.res.oracle b/tests/syntax/oracle/ghost_cv_valid_ref.res.oracle
index efafba59287..da3f96ebfcd 100644
--- a/tests/syntax/oracle/ghost_cv_valid_ref.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_valid_ref.res.oracle
@@ -3,16 +3,16 @@
struct Type {
int field ;
};
-void decl_ghost(void)/*@ ghost (int \ghost *p) */;
+void decl_ghost(void) /*@ ghost (int \ghost *p) */;
-void def_ghost(void)/*@ ghost (int \ghost *p) */
+void def_ghost(void) /*@ ghost (int \ghost *p) */
{
return;
}
-void decl_not_ghost(void)/*@ ghost (int *p) */;
+void decl_not_ghost(void) /*@ ghost (int *p) */;
-void def_not_ghost(void)/*@ ghost (int *p) */
+void def_not_ghost(void) /*@ ghost (int *p) */
{
return;
}
@@ -35,10 +35,10 @@ int main(void)
/*@ ghost int *a_ptr_2 = & ng_var.field; */
/*@ ghost int \ghost *a_ptr_4 = & g_var.field; */
/*@ ghost int b = 42; */
- decl_ghost()/*@ ghost (& b) */;
- def_ghost()/*@ ghost (& b) */;
- decl_not_ghost()/*@ ghost (& i) */;
- def_not_ghost()/*@ ghost (& i) */;
+ decl_ghost() /*@ ghost (& b) */;
+ def_ghost() /*@ ghost (& b) */;
+ decl_not_ghost() /*@ ghost (& i) */;
+ def_not_ghost() /*@ ghost (& i) */;
__retres = 0;
return __retres;
}
diff --git a/tests/syntax/oracle/ghost_cv_valid_use.res.oracle b/tests/syntax/oracle/ghost_cv_valid_use.res.oracle
index 52480a3d068..a79c5598817 100644
--- a/tests/syntax/oracle/ghost_cv_valid_use.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_valid_use.res.oracle
@@ -87,19 +87,19 @@ void g_decl_star(int \ghost *p); */
*/
/*@ assigns *p; */
-void ng_decl_star(void)/*@ ghost (int \ghost *p) */;
+void ng_decl_star(void) /*@ ghost (int \ghost *p) */;
/*@ assigns *p; */
-void ng_def_star(void)/*@ ghost (int \ghost *p) */
+void ng_def_star(void) /*@ ghost (int \ghost *p) */
{
return;
}
/*@ assigns *p; */
-void ng_decl_star_ng(void)/*@ ghost (int *p) */;
+void ng_decl_star_ng(void) /*@ ghost (int *p) */;
/*@ assigns *p; */
-void ng_def_star_ng(void)/*@ ghost (int *p) */
+void ng_def_star_ng(void) /*@ ghost (int *p) */
{
return;
}
@@ -136,19 +136,19 @@ void g_decl_set(int \ghost *p, int max); */
*/
/*@ assigns *(p + (0 .. max)); */
-void ng_decl_set(int max)/*@ ghost (int \ghost *p) */;
+void ng_decl_set(int max) /*@ ghost (int \ghost *p) */;
/*@ assigns *(p + (0 .. max)); */
-void ng_def_set(int max)/*@ ghost (int \ghost *p) */
+void ng_def_set(int max) /*@ ghost (int \ghost *p) */
{
return;
}
/*@ assigns *(p + (0 .. max)); */
-void ng_decl_set_ng(int max)/*@ ghost (int \ghost *p) */;
+void ng_decl_set_ng(int max) /*@ ghost (int \ghost *p) */;
/*@ assigns *(p + (0 .. max)); */
-void ng_def_set_ng(int max)/*@ ghost (int \ghost *p) */
+void ng_def_set_ng(int max) /*@ ghost (int \ghost *p) */
{
return;
}
diff --git a/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle b/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
index 91b2f42a890..abe9b55416e 100644
--- a/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
@@ -275,7 +275,7 @@
ng: normal -> normal
[kernel] tests/syntax/ghost_cv_var_decl.c:232
ga: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:238
+[kernel] tests/syntax/ghost_cv_var_decl.c:245
x: ghost
[kernel] tests/syntax/ghost_cv_var_decl.c:239
i: normal
@@ -291,5 +291,5 @@
main: normal
[kernel] tests/syntax/ghost_cv_var_decl.c:248
value: ghost
-[kernel] :0
+[kernel] tests/syntax/ghost_cv_var_decl.c:249
__retres: normal
--
GitLab