Merge branch 'fix/eva/split-annotations' into 'master'

[Eva] Better interpretation of successive split annotations

See merge request frama-c/frama-c!4164

src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle

@@ -44,6 +44,7 @@ enum aorai_OpStatusList {
     int S0_tmp;
     int S1_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     S0_tmp = S0;
@@ -93,6 +94,7 @@ enum aorai_OpStatusList {
     int S0_tmp;
     int S1_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     S0_tmp = S0;

src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle

@@ -74,6 +74,7 @@ int X;
     int Sf_tmp;
     int in_main_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     S1_tmp = S1;
@@ -153,6 +154,7 @@ int X;
     int Sf_tmp;
     int in_main_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     S1_tmp = S1;
@@ -247,6 +249,7 @@ void f(void)
     int Sf_tmp;
     int in_main_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     S1_tmp = S1;
@@ -326,6 +329,7 @@ void f(void)
     int Sf_tmp;
     int in_main_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     S1_tmp = S1;

src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle

@@ -71,6 +71,7 @@ int X;
   void f_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     if ((unsigned int)3 == aorai_CurStates) aorai_CurStates = S_in_f;
@@ -118,6 +119,7 @@ int X;
   void f_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = in_main;
@@ -178,6 +180,7 @@ void f(void)
   void main_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = Sf;
@@ -225,6 +228,7 @@ void f(void)
   void main_post_func(int res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     if ((unsigned int)5 == aorai_CurStates) aorai_CurStates = S2;

src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle

@@ -31,6 +31,7 @@ enum aorai_OpStatusList {
   {
     int S_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_a;
     S_tmp = S;
@@ -59,6 +60,7 @@ enum aorai_OpStatusList {
   {
     int S_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_a;
     S_tmp = S;
@@ -98,6 +100,7 @@ void a(void)
   {
     int S_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     S_tmp = S;
@@ -126,6 +129,7 @@ void a(void)
   {
     int S_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     S_tmp = S;

src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle

@@ -79,6 +79,7 @@ enum aorai_OpStatusList {
     int aorai_intermediate_state_0_tmp;
     int init_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_a;
     S_tmp = S;
@@ -166,6 +167,7 @@ enum aorai_OpStatusList {
     int aorai_intermediate_state_0_tmp;
     int init_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_a;
     S_tmp = S;
@@ -284,6 +286,7 @@ void a(void)
     int aorai_intermediate_state_0_tmp;
     int init_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     S_tmp = S;
@@ -364,6 +367,7 @@ void a(void)
     int aorai_intermediate_state_0_tmp;
     int init_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     S_tmp = S;

src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle

@@ -72,6 +72,7 @@ check lemma I_deterministic_trans{L}:
   void main_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = I;
@@ -107,6 +108,7 @@ check lemma I_deterministic_trans{L}:
   void main_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = I;

src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle

@@ -116,6 +116,7 @@ check lemma S0_deterministic_trans{L}:
   void g_pre_func(int x)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_g;
     if ((unsigned int)3 == aorai_CurStates) {
@@ -185,6 +186,7 @@ check lemma S0_deterministic_trans{L}:
   void g_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_g;
     if ((unsigned int)5 == aorai_CurStates) aorai_CurStates = S1;
@@ -263,6 +265,7 @@ void g(int x)
   void f_pre_func(int x)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     if ((unsigned int)1 == aorai_CurStates) 
@@ -321,6 +324,7 @@ void g(int x)
   void f_post_func(int res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     if ((unsigned int)1 == aorai_CurStates) 
@@ -407,6 +411,7 @@ int f(int x)
   void real_main_pre_func(int c)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_real_main;
     if ((unsigned int)0 == aorai_CurStates) {
@@ -471,6 +476,7 @@ int f(int x)
   void real_main_post_func(int res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_real_main;
     if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = Sf;
@@ -543,6 +549,7 @@ int real_main(int c)
   void main_pre_func(int c)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     if ((unsigned int)7 == aorai_CurStates) aorai_CurStates = S0;
@@ -599,6 +606,7 @@ int real_main(int c)
   void main_post_func(int res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     if ((unsigned int)6 == aorai_CurStates) aorai_CurStates = Sf;

src/plugins/aorai/tests/ya/oracle/floats.res.oracle

@@ -173,6 +173,7 @@ check lemma B_deterministic_trans{L}:
   void square_root_aux_pre_func(float x, float n)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_square_root_aux;
     if ((unsigned int)1 == aorai_CurStates) 
@@ -223,6 +224,7 @@ check lemma B_deterministic_trans{L}:
   void square_root_aux_post_func(float res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_square_root_aux;
     if ((unsigned int)1 == aorai_CurStates) aorai_CurStates = B;
@@ -301,6 +303,7 @@ float square_root_aux(float x, float n)
   void square_root_pre_func(float n)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_square_root;
     if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = B;
@@ -348,6 +351,7 @@ float square_root_aux(float x, float n)
   void square_root_post_func(float res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_square_root;
     if ((unsigned int)1 == aorai_CurStates) aorai_CurStates = C;
@@ -409,6 +413,7 @@ float square_root(float n)
   void main_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     if ((unsigned int)4 == aorai_CurStates) aorai_CurStates = A;
@@ -456,6 +461,7 @@ float square_root(float n)
   void main_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = E;

src/plugins/aorai/tests/ya/oracle/formals.res.oracle

@@ -139,6 +139,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
   void f_pre_func(int x)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     if ((unsigned int)7 == aorai_CurStates) {
@@ -238,6 +239,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
   void f_post_func(int res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     if ((unsigned int)4 == aorai_CurStates) {
@@ -394,6 +396,7 @@ int f(int x)
   void g_pre_func(int y)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_g;
     if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = OK;
@@ -474,6 +477,7 @@ int f(int x)
   void g_post_func(int res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_g;
     if ((unsigned int)3 == aorai_CurStates) {
@@ -575,6 +579,7 @@ int g(int y)
   void main_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     if ((unsigned int)6 == aorai_CurStates) aorai_CurStates = main_0;
@@ -633,6 +638,7 @@ int g(int y)
   void main_post_func(int res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = OK;

src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle

@@ -121,6 +121,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
   void f_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     if ((unsigned int)9 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state;
@@ -189,6 +190,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
   void f_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = f_called;
@@ -275,6 +277,7 @@ void f(void)
   void g_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_g;
     if ((unsigned int)9 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state_0;
@@ -343,6 +346,7 @@ void f(void)
   void g_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_g;
     if ((unsigned int)1 == aorai_CurStates) aorai_CurStates = g_called;
@@ -424,6 +428,7 @@ void g(void)
   void main_pre_func(int c)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     if ((unsigned int)7 == aorai_CurStates) aorai_CurStates = s1;
@@ -483,6 +488,7 @@ void g(void)
   void main_post_func(int res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     if ((unsigned int)8 == aorai_CurStates) aorai_CurStates = ok;

src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle

@@ -34,6 +34,7 @@ enum aorai_OpStatusList {
   {
     int S_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     S_tmp = S;
@@ -67,6 +68,7 @@ enum aorai_OpStatusList {
   {
     int S_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     S_tmp = S;

src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle

@@ -116,6 +116,7 @@ enum aorai_OpStatusList {
     int aorai_intermediate_state_2_tmp;
     int aorai_reject_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     S0_tmp = S0;
@@ -244,6 +245,7 @@ enum aorai_OpStatusList {
     int aorai_intermediate_state_2_tmp;
     int aorai_reject_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     S0_tmp = S0;
@@ -440,6 +442,7 @@ int main_bhv_bhv(int c); */
     int aorai_intermediate_state_2_tmp;
     int aorai_reject_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     S0_tmp = S0;
@@ -584,6 +587,7 @@ int main_bhv_bhv(int c); */
     int aorai_intermediate_state_2_tmp;
     int aorai_reject_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     S0_tmp = S0;

src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle

@@ -44,6 +44,7 @@ int f(void);
   void main_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     aorai_CurStates = aorai_reject;
@@ -73,6 +74,7 @@ int f(void);
   void main_post_func(int res)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     aorai_CurStates = aorai_reject;

src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle

@@ -36,6 +36,7 @@ enum aorai_OpStatusList {
   {
     int I_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     I_tmp = I;
@@ -77,6 +78,7 @@ enum aorai_OpStatusList {
   {
     int I_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     I_tmp = I;
@@ -124,6 +126,7 @@ void f(int x)
   {
     int I_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     I_tmp = I;
@@ -157,6 +160,7 @@ void f(int x)
   {
     int I_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     I_tmp = I;

src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle

@@ -129,6 +129,7 @@ enum aorai_OpStatusList {
     int aorai_intermediate_state_2_tmp;
     int aorai_intermediate_state_3_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     S0_tmp = S0;
@@ -259,6 +260,7 @@ enum aorai_OpStatusList {
     int aorai_intermediate_state_2_tmp;
     int aorai_intermediate_state_3_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     S0_tmp = S0;
@@ -415,6 +417,7 @@ void f(void)
     int aorai_intermediate_state_2_tmp;
     int aorai_intermediate_state_3_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_g;
     S0_tmp = S0;
@@ -538,6 +541,7 @@ void f(void)
     int aorai_intermediate_state_2_tmp;
     int aorai_intermediate_state_3_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_g;
     S0_tmp = S0;
@@ -680,6 +684,7 @@ void g(void)
     int aorai_intermediate_state_2_tmp;
     int aorai_intermediate_state_3_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     S0_tmp = S0;
@@ -804,6 +809,7 @@ void g(void)
     int aorai_intermediate_state_2_tmp;
     int aorai_intermediate_state_3_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     S0_tmp = S0;

src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle

@@ -120,6 +120,7 @@ check lemma e_deterministic_trans{L}:
   void f_pre_func(int x)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     if ((unsigned int)2 == aorai_CurStates) {
@@ -183,6 +184,7 @@ check lemma e_deterministic_trans{L}:
   void f_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     if ((unsigned int)3 == aorai_CurStates) aorai_CurStates = e;
@@ -260,6 +262,7 @@ void f(int x)
   void g_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_g;
     if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = d;
@@ -319,6 +322,7 @@ void f(int x)
   void g_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_g;
     if ((unsigned int)4 == aorai_CurStates) aorai_CurStates = g_0;
@@ -391,6 +395,7 @@ void g(void)
   void h_pre_func(int x)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_h;
     if ((unsigned int)5 == aorai_CurStates) 
@@ -452,6 +457,7 @@ void g(void)
   void h_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_h;
     if ((unsigned int)6 == aorai_CurStates) aorai_CurStates = g_0;
@@ -524,6 +530,7 @@ void h(int x)
   void i_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_i;
     if ((unsigned int)7 == aorai_CurStates) aorai_CurStates = h_0;
@@ -594,6 +601,7 @@ void h(int x)
   void i_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_i;
     if ((unsigned int)8 == aorai_CurStates) {
@@ -675,6 +683,7 @@ void i(void)
   void main_pre_func(int t)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = b;
@@ -734,6 +743,7 @@ void i(void)
   void main_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     if ((unsigned int)5 == aorai_CurStates) aorai_CurStates = i_0;

src/plugins/aorai/tests/ya/oracle/monostate.res.oracle

@@ -69,6 +69,7 @@ check lemma Init_deterministic_trans{L}:
   void f_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = aorai_reject;
@@ -109,6 +110,7 @@ check lemma Init_deterministic_trans{L}:
   void f_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = aorai_reject;
@@ -160,6 +162,7 @@ void f(void)
   void main_pre_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     aorai_CurStates = aorai_reject;
@@ -192,6 +195,7 @@ void f(void)
   void main_post_func(void)
   {
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     aorai_CurStates = aorai_reject;

src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle

@@ -41,6 +41,7 @@ enum aorai_OpStatusList {
     int S0_tmp;
     int Sf_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     S0_tmp = S0;
@@ -84,6 +85,7 @@ enum aorai_OpStatusList {
     int S0_tmp;
     int Sf_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     S0_tmp = S0;

src/plugins/aorai/tests/ya/oracle/observed.res.oracle

@@ -74,6 +74,7 @@ enum aorai_OpStatusList {
     int first_step_tmp;
     int init_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     aorai_intermediate_state_tmp = aorai_intermediate_state;
@@ -156,6 +157,7 @@ enum aorai_OpStatusList {
     int first_step_tmp;
     int init_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     aorai_intermediate_state_tmp = aorai_intermediate_state;
@@ -325,6 +327,7 @@ void g(void)
     int first_step_tmp;
     int init_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_h;
     aorai_intermediate_state_tmp = aorai_intermediate_state;
@@ -407,6 +410,7 @@ void g(void)
     int first_step_tmp;
     int init_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_h;
     aorai_intermediate_state_tmp = aorai_intermediate_state;

src/plugins/aorai/tests/ya/oracle/other.res.oracle

@@ -70,6 +70,7 @@ int x = 0;
     int last_tmp;
     int step1_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     init_tmp = init;
@@ -173,6 +174,7 @@ int x = 0;
     int last_tmp;
     int step1_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     init_tmp = init;
@@ -340,6 +342,7 @@ void f(void)
     int last_tmp;
     int step1_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_g;
     init_tmp = init;
@@ -443,6 +446,7 @@ void f(void)
     int last_tmp;
     int step1_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_g;
     init_tmp = init;
@@ -597,6 +601,7 @@ void g(void)
     int last_tmp;
     int step1_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     init_tmp = init;
@@ -671,6 +676,7 @@ void g(void)
     int last_tmp;
     int step1_tmp;
     /@ slevel full; @/
+    ;
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     init_tmp = init;