diff --git a/share/libc/netdb.c b/share/libc/netdb.c
index 74b43f2bf9eb3a5e35eaea2ce8cbd899c067edd5..fc34e7139b96a3b1f54a2ee1b07554158076e124 100644
--- a/share/libc/netdb.c
+++ b/share/libc/netdb.c
@@ -58,11 +58,11 @@ int getaddrinfo(
       struct sockaddr* sa = malloc(sizeof(*sa));
       if (!sa) return EAI_MEMORY;
       sa -> sa_family = Frama_C_interval(0,AF_MAX);
-      //@ slevel 15;
+      //@ \eva::slevel 15;
       for (int i = 0; i < 14; i++) {
         sa -> sa_data[i] = Frama_C_interval(CHAR_MIN,CHAR_MAX);
       }
-      //@ slevel default;
+      //@ \eva::slevel default;
       ai -> ai_flags = 0;
       ai -> ai_family = sa -> sa_family;
       ai -> ai_socktype = Frama_C_interval(0,SOCK_SEQPACKET);
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 0c4d68c1b552fbead932965cf4fe801f323973d4..0fc779ca63897ee5164581e9b1e9e0e012129418 100644
--- a/src/plugins/aorai/tests/ya/serial.c
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -71,7 +71,7 @@ void main(void)
           n = 0;
           continue;
         }
-        //@ split data & 0x40;
+        //@ \eva::split data & 0x40;
       }
       else { // data receieved
         if (n == 0) { // but status was expected}
diff --git a/src/plugins/wp/tests/wp_plugin/nullable_ext.c b/src/plugins/wp/tests/wp_plugin/nullable_ext.c
index a275cb746380c0809ec8d906a7c4db515c198ec6..aac3f9c478127075782514f9bef34c73c8fa4a34 100644
--- a/src/plugins/wp/tests/wp_plugin/nullable_ext.c
+++ b/src/plugins/wp/tests/wp_plugin/nullable_ext.c
@@ -17,7 +17,7 @@ int x;
 int *g;
 
 /*@ assigns *g, *p, x ;
-    wp_nullable_args p ;
+    \wp::wp_nullable_args p ;
 */
 void nullable_coherence(int *p) {
   if (p == (void *)0) {
@@ -31,7 +31,7 @@ void nullable_coherence(int *p) {
 }
 
 /*@ assigns *p, *q, *r, *s, *t ;
-    wp_nullable_args p, q, r ;
+    \wp::wp_nullable_args p, q, r ;
 */
 void nullable_in_context(int *p, int *q, int *r, int *s, int *t) {
   *p = 42;
@@ -41,35 +41,35 @@ void nullable_in_context(int *p, int *q, int *r, int *s, int *t) {
 }
 
 /*@ assigns *ptr ;
-    wp_nullable_args ptr  ;
+    \wp::wp_nullable_args ptr  ;
 */
 void with_declaration(int *ptr);
 void with_declaration(int *ptr) {}
 
 #ifdef FAIL_1
 /*@ assigns *ptr ;
-    wp_nullable_args unexisting_ptr ;
+    \wp::wp_nullable_args unexisting_ptr ;
 */
 void fails_no_variable(int *ptr) {}
 #endif
 
 #ifdef FAIL_2
 /*@ assigns *ptr ;
-    wp_nullable_args *ptr ;
+    \wp::wp_nullable_args *ptr ;
 */
 void not_a_variable(int *ptr) {}
 #endif
 
 #ifdef FAIL_3
 /*@ assigns *ptr ;
-    wp_nullable_args g ;
+    \wp::wp_nullable_args g ;
 */
 void not_a_formal(int *ptr) {}
 #endif
 
 #ifdef FAIL_4
 /*@ assigns x ;
-    wp_nullable_args f ;
+    \wp::wp_nullable_args f ;
 */
 void not_a_pointer(int f) {}
 #endif
diff --git a/src/plugins/wp/tests/wp_region/annot.i b/src/plugins/wp/tests/wp_region/annot.i
index bbc6d48ea3416b628a4e32cb4e51dc45a3ca1efe..e141f13431ac5907cd8a06d8b5d17392d761195d 100644
--- a/src/plugins/wp/tests/wp_region/annot.i
+++ b/src/plugins/wp/tests/wp_region/annot.i
@@ -31,7 +31,7 @@ typedef struct Block {
   SN sum ;
 } FB ;
 
-//@ region *fb ;
+//@ \wp::region *fb ;
 void fb_ADD(FB *fb)
 {
   fb->out1->v = fb->out1->v + fb->out2->v ;
@@ -39,9 +39,9 @@ void fb_ADD(FB *fb)
 }
 
 /*@
-  region IN:   (fb->inp1 .. fb->inp3), \pattern{PMEM} ;
-  region OUT:  (fb->out1 .. fb->out3), \pattern{PVECTOR} ;
-  region IDX:  (fb->idx1 .. fb->idx3), \pattern{PVECTOR} ;
+  \wp::region IN:   (fb->inp1 .. fb->inp3), \pattern{PMEM} ;
+  \wp::region OUT:  (fb->out1 .. fb->out3), \pattern{PVECTOR} ;
+  \wp::region IDX:  (fb->idx1 .. fb->idx3), \pattern{PVECTOR} ;
  */
 void fb_SORT(FB *fb)
 {
diff --git a/src/plugins/wp/tests/wp_region/annot/a.i b/src/plugins/wp/tests/wp_region/annot/a.i
index 8289866c443bb5159d61152f513aeffe280e7aa7..e684198b0e99768b84e7c3cf7aa9135e77220c27 100644
--- a/src/plugins/wp/tests/wp_region/annot/a.i
+++ b/src/plugins/wp/tests/wp_region/annot/a.i
@@ -24,7 +24,7 @@ struct Block {
 };
 typedef struct Block FB;
 /*@ terminates \true;
-    region *fb; */
+    \wp::region *fb; */
 void fb_ADD(FB *fb)
 {
   (fb->out1)->v += (fb->out2)->v;
@@ -33,9 +33,9 @@ void fb_ADD(FB *fb)
 }
 
 /*@ terminates \true;
-    region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
-    region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
-    region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
+    \wp::region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
+    \wp::region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
+    \wp::region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
  */
 void fb_SORT(FB *fb)
 {
diff --git a/src/plugins/wp/tests/wp_region/annot/b.i b/src/plugins/wp/tests/wp_region/annot/b.i
index 8289866c443bb5159d61152f513aeffe280e7aa7..e684198b0e99768b84e7c3cf7aa9135e77220c27 100644
--- a/src/plugins/wp/tests/wp_region/annot/b.i
+++ b/src/plugins/wp/tests/wp_region/annot/b.i
@@ -24,7 +24,7 @@ struct Block {
 };
 typedef struct Block FB;
 /*@ terminates \true;
-    region *fb; */
+    \wp::region *fb; */
 void fb_ADD(FB *fb)
 {
   (fb->out1)->v += (fb->out2)->v;
@@ -33,9 +33,9 @@ void fb_ADD(FB *fb)
 }
 
 /*@ terminates \true;
-    region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
-    region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
-    region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
+    \wp::region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
+    \wp::region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
+    \wp::region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
  */
 void fb_SORT(FB *fb)
 {
diff --git a/src/plugins/wp/tests/wp_region/array1.i b/src/plugins/wp/tests/wp_region/array1.i
index eac00551a13634c34e79f284c7a0bebb362b0591..e7b235b05c2dae8fb2c2fc358b0b5a3b69461907 100644
--- a/src/plugins/wp/tests/wp_region/array1.i
+++ b/src/plugins/wp/tests/wp_region/array1.i
@@ -1,4 +1,4 @@
-//@ region *p, *q ;
+//@ \wp::region *p, *q ;
 int job( int n, int * p , int * q )
 {
   int s = 0 ;
diff --git a/src/plugins/wp/tests/wp_region/array2.i b/src/plugins/wp/tests/wp_region/array2.i
index 9b8ded175cb723b3fc41dede06d21632206f6e08..1bc2f1baac572e05e322c75b69d676f993d21501 100644
--- a/src/plugins/wp/tests/wp_region/array2.i
+++ b/src/plugins/wp/tests/wp_region/array2.i
@@ -1,4 +1,4 @@
-//@ region *p; region *q ;
+//@ \wp::region *p; \wp::region *q ;
 int job( int n, int * p , int * q )
 {
   int s = 0 ;
diff --git a/src/plugins/wp/tests/wp_region/fb_ADD.i b/src/plugins/wp/tests/wp_region/fb_ADD.i
index 3bab8bad0655f3fcce7b968520c2a3558895f45b..2c939c92e0be417532ac6033f0fa9de7dc04779f 100644
--- a/src/plugins/wp/tests/wp_region/fb_ADD.i
+++ b/src/plugins/wp/tests/wp_region/fb_ADD.i
@@ -16,7 +16,7 @@ typedef struct Block {
 } FB ;
 
 /*@
-  region A: fb ;
+  \wp::region A: fb ;
 */
 void job(FB *fb)
 {
diff --git a/src/plugins/wp/tests/wp_region/fb_SORT.i b/src/plugins/wp/tests/wp_region/fb_SORT.i
index b6289be1c9e2df06aad82783823a748864535063..f5a79d97a696e5ab2ffd3fa2afcb28cd44a2fa1c 100644
--- a/src/plugins/wp/tests/wp_region/fb_SORT.i
+++ b/src/plugins/wp/tests/wp_region/fb_SORT.i
@@ -16,10 +16,10 @@ typedef struct Block {
 } FB ;
 
 /*@
-  region Shared: *(fb->inp1 .. fb->inp3);
-  region IN:      (fb->inp1 .. fb->inp3);
-  region OUT:     (fb->out1 .. fb->out3);
-  region IDX:     (fb->idx1 .. fb->idx3);
+  \wp::region Shared: *(fb->inp1 .. fb->inp3);
+  \wp::region IN:      (fb->inp1 .. fb->inp3);
+  \wp::region OUT:     (fb->out1 .. fb->out3);
+  \wp::region IDX:     (fb->idx1 .. fb->idx3);
  */
 void job(FB *fb)
 {
diff --git a/src/plugins/wp/tests/wp_region/structarray1.i b/src/plugins/wp/tests/wp_region/structarray1.i
index d657867ad894507712c52647e6d164a7391f2683..474cab2dd54d19aa8f53bb0618ac98aaec6ec373 100644
--- a/src/plugins/wp/tests/wp_region/structarray1.i
+++ b/src/plugins/wp/tests/wp_region/structarray1.i
@@ -6,7 +6,7 @@ typedef struct Matrix {
   int coef[4][4];
 } * matrix ;
 
-//@ region *X , *R ;
+//@ \wp::region *X , *R ;
 void job( matrix M , vector X , vector R )
 {
   for (int i = 0; i < 4; i++) {
diff --git a/src/plugins/wp/tests/wp_tip/oracle/pp-trailing.c.out.c b/src/plugins/wp/tests/wp_tip/oracle/pp-trailing.c.out.c
index 8e61dec3534fb7d5dedb5776b2504ea90a2a225b..46604882efa274047cfde0b203756a3c68898879 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/pp-trailing.c.out.c
+++ b/src/plugins/wp/tests/wp_tip/oracle/pp-trailing.c.out.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
-/*@ strategy Prover: \prover("alt-ergo",0.1); */
+/*@ \wp::strategy Prover: \prover("alt-ergo",0.1); */
 /*@
-strategy Lazy:
+\wp::strategy Lazy:
   Prover,
   \tactic("Wp.overflow",
     \pattern(\target:\any(P(_, (..)), Q((..)))),
diff --git a/src/plugins/wp/tests/wp_tip/oracle/pp-trailing.c.reparse.c b/src/plugins/wp/tests/wp_tip/oracle/pp-trailing.c.reparse.c
index 8e61dec3534fb7d5dedb5776b2504ea90a2a225b..46604882efa274047cfde0b203756a3c68898879 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/pp-trailing.c.reparse.c
+++ b/src/plugins/wp/tests/wp_tip/oracle/pp-trailing.c.reparse.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
-/*@ strategy Prover: \prover("alt-ergo",0.1); */
+/*@ \wp::strategy Prover: \prover("alt-ergo",0.1); */
 /*@
-strategy Lazy:
+\wp::strategy Lazy:
   Prover,
   \tactic("Wp.overflow",
     \pattern(\target:\any(P(_, (..)), Q((..)))),
diff --git a/src/plugins/wp/tests/wp_tip/pp-trailing.c b/src/plugins/wp/tests/wp_tip/pp-trailing.c
index 187b6f10ddb332e4669b823fb103990d18c83a03..18687380d4c953932022dad8478d0b02343a4def 100644
--- a/src/plugins/wp/tests/wp_tip/pp-trailing.c
+++ b/src/plugins/wp/tests/wp_tip/pp-trailing.c
@@ -8,8 +8,8 @@
 */
 
 /*@
-  strategy Prover: \prover("alt-ergo",0.1);
-  strategy Lazy:
+  \wp::strategy Prover: \prover("alt-ergo",0.1);
+  \wp::strategy Lazy:
     Prover,
     \tactic("Wp.overflow"
       ,\pattern(\any(P(_, (..)),Q((..))))
diff --git a/src/plugins/wp/tests/wp_tip/proof.i b/src/plugins/wp/tests/wp_tip/proof.i
index 83b6f05d2aaae1a387ffdb8a9d128ca173efc6f7..e783f1dd816fc6541bdbe36c444ae912e51ab48b 100644
--- a/src/plugins/wp/tests/wp_tip/proof.i
+++ b/src/plugins/wp/tests/wp_tip/proof.i
@@ -9,8 +9,8 @@
 // Provers
 
 /*@
-  strategy P1: \prover("alt-ergo");
-  strategy P2: \prover(0.5);
-  strategy P3: \prover("alt-ergo",3.0);
-  strategy P4: P1, P2, P3, \default;
+  \wp::strategy P1: \prover("alt-ergo");
+  \wp::strategy P2: \prover(0.5);
+  \wp::strategy P3: \prover("alt-ergo",3.0);
+  \wp::strategy P4: P1, P2, P3, \default;
  */
diff --git a/src/plugins/wp/tests/wp_tip/strategy.c b/src/plugins/wp/tests/wp_tip/strategy.c
index 48535ecd7a7de5894e172116d7ef8b29294dc5b5..43e5a6669dad49d04bb5a62e79c09bd977c888e6 100644
--- a/src/plugins/wp/tests/wp_tip/strategy.c
+++ b/src/plugins/wp/tests/wp_tip/strategy.c
@@ -16,21 +16,21 @@
 */
 
 /*@
-  strategy Prover: \prover("alt-ergo",0.1);
+  \wp::strategy Prover: \prover("alt-ergo",0.1);
 
-  strategy Lazy:
+  \wp::strategy Lazy:
     Prover,
     \tactic("Wp.overflow"
       ,\pattern(\any(to_uint32(_),to_sint32(_)))
     );
 
-  strategy Eager:
+  \wp::strategy Eager:
     \tactic("Wp.overflow"
       ,\pattern(\any(to_uint32(_),to_sint32(_)))
     ),
     Prover;
 
-  strategy EagerRange:
+  \wp::strategy EagerRange:
     \tactic("Wp.overflow"
       ,\pattern(\any(to_uint32(_),to_sint32(_)))
       ,\child("In-Range",EagerRange)
diff --git a/tests/fc_script/find-fun.t/list-functions.c b/tests/fc_script/find-fun.t/list-functions.c
index a71c42a5419902342063bc2823348d09edf00df9..038b36e39baf38f08ae7aa9c5c4241504e34aa93 100644
--- a/tests/fc_script/find-fun.t/list-functions.c
+++ b/tests/fc_script/find-fun.t/list-functions.c
@@ -11,7 +11,7 @@ static int static_fun() {
 }
 
 void k() {
-  /*@ loop unroll 10; */ // Eva is not loaded, so we must ignore the annotation
+  /*@ loop \eva::unroll 10; */ // Eva is not loaded, so we must ignore the annotation
   for (int i = 0; i < 10; i++) {
     extf();
   }
diff --git a/tests/libc/pwd_c.c b/tests/libc/pwd_c.c
index d60731f7f1083760b046905442bf96b156a62413..d3d269045dba8edbfbe205b6c31fe42774ff9696 100644
--- a/tests/libc/pwd_c.c
+++ b/tests/libc/pwd_c.c
@@ -22,7 +22,7 @@ int main() {
     //@ assert valid_read_string(pwd_out.pw_dir);
     //@ assert valid_read_string(pwd_out.pw_shell);
   }
-  //@ slevel merge;
+  //@ \eva::slevel merge;
   struct passwd pwd_out2;
   res = getpwnam_r("root", &pwd_out2, buf, buflen, &result);
   if (result) {
diff --git a/tests/libc/stdlib_c.c b/tests/libc/stdlib_c.c
index 065ed34d5cfc5f024dd837451311dc1bae16123c..748849d1d76051bcac12cef42dede6bf5b3e8ff8 100644
--- a/tests/libc/stdlib_c.c
+++ b/tests/libc/stdlib_c.c
@@ -2,7 +2,7 @@
    STDOPT: #"-eva-no-builtins-auto -eva-slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-msg-key malloc"
    STDOPT: #"-eva-no-builtins-auto -eva-slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-no-alloc-returns-null -eva-msg-key malloc"
    STDOPT: #"-eva-no-builtins-auto"
-*/ // slevel is used to unroll loops
+*/ // \eva::slevel is used to \eva::unroll loops
 
 #define malloc(n) Frama_C_malloc(n)
 #include "stdlib.c"
diff --git a/tests/libc/string_c.c b/tests/libc/string_c.c
index 27a2aad0c9ca86ef90126fc3833ddef18e5ad929..eeb65f0a999d665bfa1f0619ffa0933ec4593658 100644
--- a/tests/libc/string_c.c
+++ b/tests/libc/string_c.c
@@ -1,6 +1,6 @@
 /* run.config
    STDOPT: #"-eva-no-builtins-auto -eva-slevel 1000 -eva-no-skip-stdlib-specs"
-*/ // slevel is used to unroll loops
+*/ // \eva::slevel is used to \eva::unroll loops
 
 #include "string.c"
 volatile int v;
diff --git a/tests/libc/string_h.c b/tests/libc/string_h.c
index 7c0194e1c5b093828ea3e7aad584741437004947..1cdf89a28bc5488ca46442dc38b95b78b6843fac 100644
--- a/tests/libc/string_h.c
+++ b/tests/libc/string_h.c
@@ -30,7 +30,7 @@ void test_strncat(void)
   char data[100];
   data[0] = '\0';
   char source[100];
-  //@ slevel 99;
+  //@ \eva::slevel 99;
   for (int i = 0; i < 99; i++) source[i] = 'Z';
   source[99] = '\0';
   strncat(data, source, 100);
@@ -46,7 +46,7 @@ struct s {
 void crashes_gcc() {
   struct s s;
   char *ss = "ABCDEFGHIJKLMNOPQRSTUVWXYZ012";
-  //@ slevel 30;
+  //@ \eva::slevel 30;
   for (int i = 0; i < 30; i++) s.s1[i] = ss[i];
   char *dest = s.s1+29;
   char *src = s.s1;
diff --git a/tests/libc/wchar_h.c b/tests/libc/wchar_h.c
index 3bde71c8dc721489453c79ddf683c6dbbba409c3..c0780e750592fb13d44b882251214dd8d1a7a096 100644
--- a/tests/libc/wchar_h.c
+++ b/tests/libc/wchar_h.c
@@ -58,7 +58,7 @@ int main() {
   wchar_t wdst2[20] = {0};
   wcsncat(wdst2, wsrc, 11); // no warning
   wcsncat(wdst2, wsrc, 10); // no warning (if wdst2 is precise)
-  //@ loop unroll 10;
+  //@ loop \eva::unroll 10;
   for (int i = 0; i < 10; i++)
     wdst2[i] = L'A';
   wdst2[10] = L'\0'; // wdst2 now has length 10
diff --git a/tests/spec/kw.c b/tests/spec/kw.c
index c780af02c9dc6fbc09f6badafd206db025676aa0..d9072d4d9043df72df8599cfb91da76e501cb64e 100644
--- a/tests/spec/kw.c
+++ b/tests/spec/kw.c
@@ -1,5 +1,5 @@
 /* run.config
-COMMENT: eva plugin is required for the slevel annotation
+COMMENT: eva plugin is required for the \eva::slevel annotation
 PLUGIN: eva
   STDOPT:
 */
@@ -15,7 +15,7 @@ assert behavior = 0;
     ensures behavior >= 0;
 */
 int main () {
-  //@ slevel 4;
+  //@ \eva::slevel 4;
   behavior++;
   struct custom { int reads, behaviors, label ; } writes;
   //@ assert custom: writes.reads + writes.behaviors <= \let global = writes.label; global;
@@ -50,4 +50,4 @@ int requires(volatile int*a, int v) { *a = v; return v; }
 
 int slevel = 1000000;
 
-//@ lemma bar: slevel >= 0;
+//@ lemma bar: \eva::slevel >= 0;
diff --git a/tests/syntax/inline_calls.i b/tests/syntax/inline_calls.i
index bd1ca99bc3dafedad78927da14261be279a3a3bf..ca6f2a2b7f68e2f45fe763a698022776051e7d18 100644
--- a/tests/syntax/inline_calls.i
+++ b/tests/syntax/inline_calls.i
@@ -76,7 +76,7 @@ void call_builtin_acsl () {
 }
 
 void f_slevel() {
-  //@ slevel 0;
+  //@ \eva::slevel 0;
   return;
 }
 
diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c
index 52e7e4433bd5c0a83f5b435fd18d3231a4e7a7c7..7a203185712a92c869d46f16732c07bfe07cc798 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -125,11 +125,11 @@ int ai4[] = {1, [7205759403792793] = 11};
 
 int main() {
 #ifdef EVA_UNROLL
-  //@ loop unroll (-9999999999999999999); // IntLimit
+  //@ loop \eva::unroll (-9999999999999999999); // IntLimit
   while (nondet);
-  //@ loop unroll too_large_integer; // ExpLimit
+  //@ loop \eva::unroll too_large_integer; // ExpLimit
   while (nondet);
-  //@ slevel 9999999999999999999;
+  //@ \eva::slevel 9999999999999999999;
   while (nondet);
 #endif
 #ifdef CABS_DOWHILE