From ba1415b238dd1fb433115f1aebed461f97ca3bcf Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 5 Nov 2019 16:06:54 +0100
Subject: [PATCH] [ghost] Update tests for ghost qualifier

---
 tests/pretty_printing/annotations.i           |  5 +++-
 tests/pretty_printing/ghost_parameters.c      |  5 ++++
 .../oracle/annotations.res.oracle             | 14 +++++++---
 .../oracle/ghost_parameters.res.oracle        | 28 +++++++++----------
 tests/rte/bts621.c                            |  8 ++++--
 tests/rte/oracle/bts621.res.oracle            | 12 ++++----
 tests/spec/assigns_from_kf.i                  |  4 ++-
 tests/spec/ghost.c                            |  2 +-
 tests/spec/oracle/assigns_from_kf.res.oracle  | 28 +++++++++----------
 tests/spec/oracle/ghost.res.oracle            |  2 +-
 tests/syntax/ghost_cv_var_decl.c              |  4 +--
 .../syntax/ghost_parameters_side_effect_arg.i |  5 ++++
 12 files changed, 70 insertions(+), 47 deletions(-)

diff --git a/tests/pretty_printing/annotations.i b/tests/pretty_printing/annotations.i
index c42249060c9..d55336cd4c7 100644
--- a/tests/pretty_printing/annotations.i
+++ b/tests/pretty_printing/annotations.i
@@ -88,7 +88,7 @@ void function_with_ghost(int x) {
       y++;
       /@ assert y <= x ; @/
     }
-    
+
     /@ assert y == x ; @/
 
     /@ requires y == x ;
@@ -105,6 +105,9 @@ void function_with_ghost(int x) {
 */
 
 /*@ ghost
+  /@ requires variable > 0 ;
+     assigns \nothing ;
+  @/
   void function_declaration(int variable) ;
 */
 
diff --git a/tests/pretty_printing/ghost_parameters.c b/tests/pretty_printing/ghost_parameters.c
index b6faaf21000..125ea27e9af 100644
--- a/tests/pretty_printing/ghost_parameters.c
+++ b/tests/pretty_printing/ghost_parameters.c
@@ -1,3 +1,8 @@
+/* run.config
+  STDOPT: +"-kernel-warn-key ghost:bad-use=inactive"
+*/
+// Note: we deactivate ghost:bad-use to check that pretty-printing ghost well
+
 void decl_function_void_no_ghost(void);
 void def_function_void_no_ghost(void) {}
 void decl_function_void_ghost(void) /*@ ghost (int y) */;
diff --git a/tests/pretty_printing/oracle/annotations.res.oracle b/tests/pretty_printing/oracle/annotations.res.oracle
index 1f621523d2d..3149bcdb238 100644
--- a/tests/pretty_printing/oracle/annotations.res.oracle
+++ b/tests/pretty_printing/oracle/annotations.res.oracle
@@ -98,7 +98,10 @@ void function_with_ghost(int x)
 
 */
 
-/*@ ghost void function_declaration(int variable); */
+/*@ ghost
+/@ requires variable > 0;
+   assigns \nothing; @/
+void function_declaration(int variable); */
 
 void reference_function(void)
 {
@@ -115,8 +118,8 @@ void reference_function(void)
   def'n of func function_with_ghost at tests/pretty_printing/annotations.i:43 (sum 9297192) conflicts with the one at tests/pretty_printing/result/annotations.c:38 (sum 14988159); keeping the one at tests/pretty_printing/result/annotations.c:38.
 [kernel] tests/pretty_printing/annotations.i:80: Warning: 
   def'n of func ghost_function at tests/pretty_printing/annotations.i:80 (sum 9297192) conflicts with the one at tests/pretty_printing/result/annotations.c:71 (sum 14988159); keeping the one at tests/pretty_printing/result/annotations.c:71.
-[kernel] tests/pretty_printing/annotations.i:111: Warning: 
-  dropping duplicate def'n of func reference_function at tests/pretty_printing/annotations.i:111 in favor of that at tests/pretty_printing/result/annotations.c:102
+[kernel] tests/pretty_printing/annotations.i:114: Warning: 
+  dropping duplicate def'n of func reference_function at tests/pretty_printing/annotations.i:114 in favor of that at tests/pretty_printing/result/annotations.c:105
 /* Generated by Frama-C */
 /*@ axiomatic A {
       predicate P(ℤ x) 
@@ -216,7 +219,10 @@ void function_with_ghost(int x)
 
 */
 
-/*@ ghost void function_declaration(int variable); */
+/*@ ghost
+/@ requires variable > 0;
+   assigns \nothing; @/
+void function_declaration(int variable); */
 
 void reference_function(void)
 {
diff --git a/tests/pretty_printing/oracle/ghost_parameters.res.oracle b/tests/pretty_printing/oracle/ghost_parameters.res.oracle
index 79cdc64d68c..b59174093b4 100644
--- a/tests/pretty_printing/oracle/ghost_parameters.res.oracle
+++ b/tests/pretty_printing/oracle/ghost_parameters.res.oracle
@@ -79,20 +79,20 @@ int main(void)
 
 [kernel] Parsing tests/pretty_printing/result/ghost_parameters.c (with preprocessing)
 [kernel] Parsing tests/pretty_printing/ghost_parameters.c (with preprocessing)
-[kernel] tests/pretty_printing/ghost_parameters.c:2: Warning: 
-  dropping duplicate def'n of func def_function_void_no_ghost at tests/pretty_printing/ghost_parameters.c:2 in favor of that at tests/pretty_printing/result/ghost_parameters.c:4
-[kernel] tests/pretty_printing/ghost_parameters.c:4: Warning: 
-  dropping duplicate def'n of func def_function_void_ghost at tests/pretty_printing/ghost_parameters.c:4 in favor of that at tests/pretty_printing/result/ghost_parameters.c:11
-[kernel] tests/pretty_printing/ghost_parameters.c:6: Warning: 
-  dropping duplicate def'n of func def_function_x_no_ghost at tests/pretty_printing/ghost_parameters.c:6 in favor of that at tests/pretty_printing/result/ghost_parameters.c:18
-[kernel] tests/pretty_printing/ghost_parameters.c:8: Warning: 
-  dropping duplicate def'n of func def_function_x_ghost at tests/pretty_printing/ghost_parameters.c:8 in favor of that at tests/pretty_printing/result/ghost_parameters.c:25
-[kernel] tests/pretty_printing/ghost_parameters.c:10: Warning: 
-  dropping duplicate def'n of func def_with_fptr at tests/pretty_printing/ghost_parameters.c:10 in favor of that at tests/pretty_printing/result/ghost_parameters.c:32
-[kernel] tests/pretty_printing/ghost_parameters.c:17: Warning: 
-  dropping duplicate def'n of func def_variadic at tests/pretty_printing/ghost_parameters.c:17 in favor of that at tests/pretty_printing/result/ghost_parameters.c:42
-[kernel] tests/pretty_printing/ghost_parameters.c:19: Warning: 
-  def'n of func main at tests/pretty_printing/ghost_parameters.c:19 (sum 21482) conflicts with the one at tests/pretty_printing/result/ghost_parameters.c:47 (sum 23256); keeping the one at tests/pretty_printing/result/ghost_parameters.c:47.
+[kernel] tests/pretty_printing/ghost_parameters.c:7: Warning: 
+  dropping duplicate def'n of func def_function_void_no_ghost at tests/pretty_printing/ghost_parameters.c:7 in favor of that at tests/pretty_printing/result/ghost_parameters.c:4
+[kernel] tests/pretty_printing/ghost_parameters.c:9: Warning: 
+  dropping duplicate def'n of func def_function_void_ghost at tests/pretty_printing/ghost_parameters.c:9 in favor of that at tests/pretty_printing/result/ghost_parameters.c:11
+[kernel] tests/pretty_printing/ghost_parameters.c:11: Warning: 
+  dropping duplicate def'n of func def_function_x_no_ghost at tests/pretty_printing/ghost_parameters.c:11 in favor of that at tests/pretty_printing/result/ghost_parameters.c:18
+[kernel] tests/pretty_printing/ghost_parameters.c:13: Warning: 
+  dropping duplicate def'n of func def_function_x_ghost at tests/pretty_printing/ghost_parameters.c:13 in favor of that at tests/pretty_printing/result/ghost_parameters.c:25
+[kernel] tests/pretty_printing/ghost_parameters.c:15: Warning: 
+  dropping duplicate def'n of func def_with_fptr at tests/pretty_printing/ghost_parameters.c:15 in favor of that at tests/pretty_printing/result/ghost_parameters.c:32
+[kernel] tests/pretty_printing/ghost_parameters.c:22: Warning: 
+  dropping duplicate def'n of func def_variadic at tests/pretty_printing/ghost_parameters.c:22 in favor of that at tests/pretty_printing/result/ghost_parameters.c:42
+[kernel] tests/pretty_printing/ghost_parameters.c:24: Warning: 
+  def'n of func main at tests/pretty_printing/ghost_parameters.c:24 (sum 21482) conflicts with the one at tests/pretty_printing/result/ghost_parameters.c:47 (sum 23256); keeping the one at tests/pretty_printing/result/ghost_parameters.c:47.
 /* Generated by Frama-C */
 void decl_function_void_no_ghost(void);
 
diff --git a/tests/rte/bts621.c b/tests/rte/bts621.c
index 7b7a1569333..5bceeeddce6 100644
--- a/tests/rte/bts621.c
+++ b/tests/rte/bts621.c
@@ -1,8 +1,10 @@
 /* run.config
    OPT: -print -then -no-print -rte -warn-signed-overflow -then -print
 */
-//@ assigns *p;
-float g(float* p);
+/*@ ghost
+  /@ assigns *p; @/
+  float g(float \ghost* p) ; 
+*/
 
-void f(float a) { /*@ ghost float x = g(&a); */ }
+void f(void) /*@ ghost (float a) */ { /*@ ghost float x = g(&a); */ }
 
diff --git a/tests/rte/oracle/bts621.res.oracle b/tests/rte/oracle/bts621.res.oracle
index 89c2f9e6fa7..aba4109d064 100644
--- a/tests/rte/oracle/bts621.res.oracle
+++ b/tests/rte/oracle/bts621.res.oracle
@@ -1,9 +1,9 @@
 [kernel] Parsing tests/rte/bts621.c (with preprocessing)
 /* Generated by Frama-C */
-/*@ assigns *p; */
-float g(float *p);
+/*@ ghost /@ assigns *p; @/
+float g(float \ghost *p); */
 
-void f(float a)
+void f(void) /*@ ghost (float a) */
 {
   /*@ ghost float x = g(& a); */
   return;
@@ -12,10 +12,10 @@ void f(float a)
 
 [rte] annotating function f
 /* Generated by Frama-C */
-/*@ assigns *p; */
-float g(float *p);
+/*@ ghost /@ assigns *p; @/
+float g(float \ghost *p); */
 
-void f(float a)
+void f(void) /*@ ghost (float a) */
 {
   /*@ ghost float x = g(& a); */
   return;
diff --git a/tests/spec/assigns_from_kf.i b/tests/spec/assigns_from_kf.i
index 1def9b69986..90a4fb65484 100644
--- a/tests/spec/assigns_from_kf.i
+++ b/tests/spec/assigns_from_kf.i
@@ -1,7 +1,9 @@
 /* run.config
   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
-  OPT: -print
+  OPT: -kernel-warn-key ghost:bad-use=inactive -print
 */
+// Note: we deactivate "ghost:bad-use" because the typing phase checks on call
+// that ghost functions that are only declared have a contract.
 
 void nothing(void);
 int nothing_r(void);
diff --git a/tests/spec/ghost.c b/tests/spec/ghost.c
index 57fd0471654..835272dea4a 100644
--- a/tests/spec/ghost.c
+++ b/tests/spec/ghost.c
@@ -9,6 +9,6 @@ struct A { int x; };
 int main() {
   /*@ ghost struct B b; */
   struct A a;
-  /*@ ghost b.y = 0; a.x = b.y; */
+  /*@ ghost b.y = 0; b.y += a.x ; */
   return 0;
 }
diff --git a/tests/spec/oracle/assigns_from_kf.res.oracle b/tests/spec/oracle/assigns_from_kf.res.oracle
index 1f02fd47e90..40a98c9c66e 100644
--- a/tests/spec/oracle/assigns_from_kf.res.oracle
+++ b/tests/spec/oracle/assigns_from_kf.res.oracle
@@ -1,31 +1,31 @@
 [kernel] Parsing tests/spec/assigns_from_kf.i (no preprocessing)
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function both, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function both_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function g_both, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function g_both_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function g_nothing, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function g_nothing_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function g_something_non_ghost, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function g_something_non_ghost_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function nothing, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function nothing_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function something_ghost, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function something_ghost_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function something_non_ghost, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:29: Warning: 
   Neither code nor specification for function something_non_ghost_r, generating default assigns from the prototype
 /* Generated by Frama-C */
 /*@ assigns \nothing; */
diff --git a/tests/spec/oracle/ghost.res.oracle b/tests/spec/oracle/ghost.res.oracle
index 665fd6a6fe7..81fc9c14866 100644
--- a/tests/spec/oracle/ghost.res.oracle
+++ b/tests/spec/oracle/ghost.res.oracle
@@ -14,7 +14,7 @@ int main(void)
   /*@ ghost struct B b; */
   struct A a;
   /*@ ghost b.y = 0; */
-  /*@ ghost a.x = b.y; */
+  /*@ ghost b.y += a.x; */
   __retres = 0;
   return __retres;
 }
diff --git a/tests/syntax/ghost_cv_var_decl.c b/tests/syntax/ghost_cv_var_decl.c
index 5ec50a02902..6a8f1922b98 100644
--- a/tests/syntax/ghost_cv_var_decl.c
+++ b/tests/syntax/ghost_cv_var_decl.c
@@ -1,9 +1,9 @@
 /* run.config
-   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT:-cpp-extra-args="-DFAIL_DECL_TYPE"
-   OPT:
+   OPT:-load-script @PTEST_DIR@/@PTEST_NAME@.ml
 */
 
+
 /* When there is no comment, the code should be allowed */
 void f_ints(){
   int ng ;
diff --git a/tests/syntax/ghost_parameters_side_effect_arg.i b/tests/syntax/ghost_parameters_side_effect_arg.i
index 00d02e6665a..927d6e7828e 100644
--- a/tests/syntax/ghost_parameters_side_effect_arg.i
+++ b/tests/syntax/ghost_parameters_side_effect_arg.i
@@ -1,3 +1,8 @@
+/* run.config
+   STDOPT: +"-kernel-warn-key ghost:bad-use=inactive"
+*/
+// Note: we deactivate "ghost:bad-use" to check that printing goes right
+
 void function(int x) /*@ ghost(int y) */ ;
 int other(int x) /*@ ghost(int y) */ ;
 
-- 
GitLab