Update test oracles

8c5a2bb1 · Thibault Martin · Allan Blanchard · c9f05c24 · 8c5a2bb1 · 8c5a2bb1
Commit 8c5a2bb1 authored 1 year ago by Thibault Martin Committed by Allan Blanchard 11 months ago
--- a/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle
@@ -43,7 +43,7 @@ enum aorai_OpStatusList {
  {
    int S0_tmp;
    int S1_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -93,7 +93,7 @@ enum aorai_OpStatusList {
  {
    int S0_tmp;
    int S1_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
@@ -73,7 +73,7 @@ int X;
    int S_in_f_tmp;
    int Sf_tmp;
    int in_main_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -153,7 +153,7 @@ int X;
    int S_in_f_tmp;
    int Sf_tmp;
    int in_main_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -248,7 +248,7 @@ void f(void)
    int S_in_f_tmp;
    int Sf_tmp;
    int in_main_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -328,7 +328,7 @@ void f(void)
    int S_in_f_tmp;
    int Sf_tmp;
    int in_main_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -70,7 +70,7 @@ int X;
   @/
  void f_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -118,7 +118,7 @@ int X;
   @/
  void f_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -179,7 +179,7 @@ void f(void)
   @/
  void main_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -227,7 +227,7 @@ void f(void)
   @/
  void main_post_func(int res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
@@ -30,7 +30,7 @@ enum aorai_OpStatusList {
  void a_pre_func(void)
  {
    int S_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_a;
@@ -59,7 +59,7 @@ enum aorai_OpStatusList {
  void a_post_func(void)
  {
    int S_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_a;
@@ -99,7 +99,7 @@ void a(void)
  void main_pre_func(void)
  {
    int S_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -128,7 +128,7 @@ void a(void)
  void main_post_func(void)
  {
    int S_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -78,7 +78,7 @@ enum aorai_OpStatusList {
    int aorai_intermediate_state_tmp;
    int aorai_intermediate_state_0_tmp;
    int init_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_a;
@@ -166,7 +166,7 @@ enum aorai_OpStatusList {
    int aorai_intermediate_state_tmp;
    int aorai_intermediate_state_0_tmp;
    int init_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_a;
@@ -285,7 +285,7 @@ void a(void)
    int aorai_intermediate_state_tmp;
    int aorai_intermediate_state_0_tmp;
    int init_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -366,7 +366,7 @@ void a(void)
    int aorai_intermediate_state_tmp;
    int aorai_intermediate_state_0_tmp;
    int init_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -71,7 +71,7 @@ check lemma I_deterministic_trans{L}:
   @/
  void main_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -107,7 +107,7 @@ check lemma I_deterministic_trans{L}:
   @/
  void main_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -115,7 +115,7 @@ check lemma S0_deterministic_trans{L}:
   @/
  void g_pre_func(int x)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_g;
@@ -185,7 +185,7 @@ check lemma S0_deterministic_trans{L}:
   @/
  void g_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_g;
@@ -264,7 +264,7 @@ void g(int x)
   @/
  void f_pre_func(int x)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -323,7 +323,7 @@ void g(int x)
   @/
  void f_post_func(int res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -410,7 +410,7 @@ int f(int x)
   @/
  void real_main_pre_func(int c)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_real_main;
@@ -475,7 +475,7 @@ int f(int x)
   @/
  void real_main_post_func(int res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_real_main;
@@ -548,7 +548,7 @@ int real_main(int c)
   @/
  void main_pre_func(int c)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -605,7 +605,7 @@ int real_main(int c)
   @/
  void main_post_func(int res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
@@ -169,7 +169,7 @@ check lemma B_deterministic_trans{L}:
   @/
  void square_root_aux_pre_func(float x, float n)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_square_root_aux;
@@ -220,7 +220,7 @@ check lemma B_deterministic_trans{L}:
   @/
  void square_root_aux_post_func(float res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_square_root_aux;
@@ -299,7 +299,7 @@ float square_root_aux(float x, float n)
   @/
  void square_root_pre_func(float n)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_square_root;
@@ -347,7 +347,7 @@ float square_root_aux(float x, float n)
   @/
  void square_root_post_func(float res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_square_root;
@@ -409,7 +409,7 @@ float square_root(float n)
   @/
  void main_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -457,7 +457,7 @@ float square_root(float n)
   @/
  void main_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -138,7 +138,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
   @/
  void f_pre_func(int x)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -238,7 +238,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
   @/
  void f_post_func(int res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -395,7 +395,7 @@ int f(int x)
   @/
  void g_pre_func(int y)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_g;
@@ -476,7 +476,7 @@ int f(int x)
   @/
  void g_post_func(int res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_g;
@@ -578,7 +578,7 @@ int g(int y)
   @/
  void main_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -637,7 +637,7 @@ int g(int y)
   @/
  void main_post_func(int res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
@@ -120,7 +120,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
   @/
  void f_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -189,7 +189,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
   @/
  void f_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -276,7 +276,7 @@ void f(void)
   @/
  void g_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_g;
@@ -345,7 +345,7 @@ void f(void)
   @/
  void g_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_g;
@@ -427,7 +427,7 @@ void g(void)
   @/
  void main_pre_func(int c)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -487,7 +487,7 @@ void g(void)
   @/
  void main_post_func(int res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;
@@ -508,10 +508,10 @@ int main(int c)
  int __retres;
  /*@ ghost main_pre_func(c); */
  if (c) pf = & f; else pf = & g;
-  /*@ calls f, g; */
+  /*@ \kernel::calls f, g; */
  (*pf)();
  if (c) pf = & g; else pf = & f;
-  /*@ calls f, g; */
+  /*@ \kernel::calls f, g; */
  (*pf)();
  __retres = 0;
  /*@ ghost main_post_func(__retres); */

--- a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
@@ -33,7 +33,7 @@ enum aorai_OpStatusList {
  void main_pre_func(void)
  {
    int S_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -67,7 +67,7 @@ enum aorai_OpStatusList {
  void main_post_func(void)
  {
    int S_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -115,7 +115,7 @@ enum aorai_OpStatusList {
    int aorai_intermediate_state_1_tmp;
    int aorai_intermediate_state_2_tmp;
    int aorai_reject_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -244,7 +244,7 @@ enum aorai_OpStatusList {
    int aorai_intermediate_state_1_tmp;
    int aorai_intermediate_state_2_tmp;
    int aorai_reject_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -441,7 +441,7 @@ int main_bhv_bhv(int c); */
    int aorai_intermediate_state_1_tmp;
    int aorai_intermediate_state_2_tmp;
    int aorai_reject_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -586,7 +586,7 @@ int main_bhv_bhv(int c); */
    int aorai_intermediate_state_1_tmp;
    int aorai_intermediate_state_2_tmp;
    int aorai_reject_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -43,7 +43,7 @@ int f(void);
   @/
  void main_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -73,7 +73,7 @@ int f(void);
   @/
  void main_post_func(int res)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
@@ -35,7 +35,7 @@ enum aorai_OpStatusList {
  void f_pre_func(int x)
  {
    int I_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -77,7 +77,7 @@ enum aorai_OpStatusList {
  void f_post_func(void)
  {
    int I_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -125,7 +125,7 @@ void f(int x)
  void main_pre_func(int x)
  {
    int I_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -159,7 +159,7 @@ void f(int x)
  void main_post_func(void)
  {
    int I_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -128,7 +128,7 @@ enum aorai_OpStatusList {
    int aorai_intermediate_state_1_tmp;
    int aorai_intermediate_state_2_tmp;
    int aorai_intermediate_state_3_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -259,7 +259,7 @@ enum aorai_OpStatusList {
    int aorai_intermediate_state_1_tmp;
    int aorai_intermediate_state_2_tmp;
    int aorai_intermediate_state_3_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -416,7 +416,7 @@ void f(void)
    int aorai_intermediate_state_1_tmp;
    int aorai_intermediate_state_2_tmp;
    int aorai_intermediate_state_3_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_g;
@@ -540,7 +540,7 @@ void f(void)
    int aorai_intermediate_state_1_tmp;
    int aorai_intermediate_state_2_tmp;
    int aorai_intermediate_state_3_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_g;
@@ -683,7 +683,7 @@ void g(void)
    int aorai_intermediate_state_1_tmp;
    int aorai_intermediate_state_2_tmp;
    int aorai_intermediate_state_3_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -808,7 +808,7 @@ void g(void)
    int aorai_intermediate_state_1_tmp;
    int aorai_intermediate_state_2_tmp;
    int aorai_intermediate_state_3_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -119,7 +119,7 @@ check lemma e_deterministic_trans{L}:
   @/
  void f_pre_func(int x)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -183,7 +183,7 @@ check lemma e_deterministic_trans{L}:
   @/
  void f_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -261,7 +261,7 @@ void f(int x)
   @/
  void g_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_g;
@@ -321,7 +321,7 @@ void f(int x)
   @/
  void g_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_g;
@@ -394,7 +394,7 @@ void g(void)
   @/
  void h_pre_func(int x)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_h;
@@ -456,7 +456,7 @@ void g(void)
   @/
  void h_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_h;
@@ -529,7 +529,7 @@ void h(int x)
   @/
  void i_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_i;
@@ -600,7 +600,7 @@ void h(int x)
   @/
  void i_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_i;
@@ -682,7 +682,7 @@ void i(void)
   @/
  void main_pre_func(int t)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -742,7 +742,7 @@ void i(void)
   @/
  void main_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -68,7 +68,7 @@ check lemma Init_deterministic_trans{L}:
   @/
  void f_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -109,7 +109,7 @@ check lemma Init_deterministic_trans{L}:
   @/
  void f_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -161,7 +161,7 @@ void f(void)
   @/
  void main_pre_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -194,7 +194,7 @@ void f(void)
   @/
  void main_post_func(void)
  {
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;

--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -40,7 +40,7 @@ enum aorai_OpStatusList {
  {
    int S0_tmp;
    int Sf_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -84,7 +84,7 @@ enum aorai_OpStatusList {
  {
    int S0_tmp;
    int Sf_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;

--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -73,7 +73,7 @@ enum aorai_OpStatusList {
    int final_tmp;
    int first_step_tmp;
    int init_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -156,7 +156,7 @@ enum aorai_OpStatusList {
    int final_tmp;
    int first_step_tmp;
    int init_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -326,7 +326,7 @@ void g(void)
    int final_tmp;
    int first_step_tmp;
    int init_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_h;
@@ -409,7 +409,7 @@ void g(void)
    int final_tmp;
    int first_step_tmp;
    int init_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_h;

--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -69,7 +69,7 @@ int x = 0;
    int init_tmp;
    int last_tmp;
    int step1_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_f;
@@ -173,7 +173,7 @@ int x = 0;
    int init_tmp;
    int last_tmp;
    int step1_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_f;
@@ -341,7 +341,7 @@ void f(void)
    int init_tmp;
    int last_tmp;
    int step1_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_g;
@@ -445,7 +445,7 @@ void f(void)
    int init_tmp;
    int last_tmp;
    int step1_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_g;
@@ -600,7 +600,7 @@ void g(void)
    int init_tmp;
    int last_tmp;
    int step1_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Called;
    aorai_CurOperation = op_main;
@@ -675,7 +675,7 @@ void g(void)
    int init_tmp;
    int last_tmp;
    int step1_tmp;
-    /@ slevel full; @/
+    /@ \eva::slevel full; @/
    ;
    aorai_CurOpStatus = aorai_Terminated;
    aorai_CurOperation = op_main;