[aorai] update tests and oracles after rebase

src/plugins/aorai/tests/ya/aorai_ptr_field.i

 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 struct S { int x; };

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

 [kernel] Parsing tests/ya/aorai_ptr_field.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_aorai_ptr_field_0.i (no preprocessing)
 /* Generated by Frama-C */
 struct S {
@@ -12,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S0 = 1; */
 /*@ ghost int S1 = 0; */
 /*@ ghost
@@ -38,6 +37,7 @@ enum aorai_OpStatusList {
   {
     int S0_tmp;
     int S1_tmp;
+    /@ slevel full; @/
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     S0_tmp = S0;
@@ -73,6 +73,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_prove/aorai_ptr_field.res.oracle

 [kernel] Parsing tests/ya/aorai_ptr_field.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_aorai_ptr_field_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards

src/plugins/aorai/tests/ya/serial.ya

@@ -7,7 +7,7 @@ $x2 : int;
 $y1 : int;
 $y2 : int;
 
-Error : { 0 } -> Error;
+Error : { false } -> Error;
 
 Wait1 :
   { CALL(input_status) } -> StatusReq1
@@ -129,25 +129,25 @@ DataReq1 :
 DataReq2 :
   { input_data().\result & 192 == 128 } -> Wait2
 | { input_data().\result & 192 == 192 } -> Wait1
-| { input_data().\result & 128 == 0 } $x1 := \result -> Wait3
+| { input_data().\result & 128 == 0 } $x1 := \result; -> Wait3
 ;
 
 DataReq3 :
   { input_data().\result & 192 == 128 } -> Wait2
 | { input_data().\result & 192 == 192 } -> Wait1
-| { input_data().\result & 128 == 0 } $x2 := \result -> Wait4
+| { input_data().\result & 128 == 0 } $x2 := \result; -> Wait4
 ;
 
 DataReq4 :
   { input_data().\result & 192 == 128 } -> Wait2
 | { input_data().\result & 192 == 192 } -> Wait1
-| { input_data().\result & 128 == 0 } $y1 := \result -> Wait5
+| { input_data().\result & 128 == 0 } $y1 := \result; -> Wait5
 ;
 
 DataReq5 :
   { input_data().\result & 192 == 128 } -> Wait2
 | { input_data().\result & 192 == 192 } -> Wait1
-| { input_data().\result & 128 == 0 } $y2 := \result -> Complete
+| { input_data().\result & 128 == 0 } $y2 := \result; -> Complete
 ;
 
 Complete :