diff --git a/tests/pretty_printing/annotations.i b/tests/pretty_printing/annotations.i
index c42249060c9e8008387b530cc9fbdcd83a1fc92b..d55336cd4c7bd029260f672953b2a38d8d39bcf1 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 b6faaf2100018a347a525b9d92c1f1204765c9b6..125ea27e9affb6da2ad8d94318302702e602d56c 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 1f621523d2d90cd6714bc1aa9c3021d60034e538..3149bcdb238e9dcd951850f1bf69e11db605d1eb 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 79cdc64d68cd8d06e45db07a2084eac9205b38b4..b59174093b427f5066ee7460d3eccb3583401913 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 7b7a156933340dd22d0f0adec92531ba5670e342..5bceeeddce699bc5a3084090c18ab1688df12417 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 89c2f9e6fa735e1702c8201cf350f28cbdf179a4..aba4109d0645ace1de99ae08255e1613fd4868af 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 1def9b69986ada84b2f0ffe0a1ba1544ac89120d..90a4fb65484eb6b1f0b87ef22d7316f26c957f76 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 57fd04716549a6f65afcb8cb34b7cd0a9319557c..835272dea4a54227e9d3d3224ac4c9ab8a0789fb 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 1f02fd47e908d4d2eef0496fb797738d2723bb46..40a98c9c66ea7c9da1dc2bbf587ce0f60acf7cb9 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 665fd6a6fe72d6bccdc6bd97ab278e48cdabb57e..81fc9c14866ec279b39966d809e09077028b6e99 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 5ec50a0290215899883e4f8a05b416e828335ba6..6a8f1922b9870d826dfcddb54638ba9386401f1d 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 00d02e6665a1ff8aa1a5cc14d79c76fbcd1fb191..927d6e7828ef7aae13dd854fadfddb0e4e386cd0 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) */ ;