From 3433c2d06aa6920be0f4cd245c61b6530a500edc Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 20 Jan 2021 19:17:55 +0100
Subject: [PATCH] [aorai] update tests and oracles after rebase
---
src/plugins/aorai/tests/ya/aorai_ptr_field.i | 2 +-
.../aorai/tests/ya/oracle/aorai_ptr_field.res.oracle | 7 ++++---
.../tests/ya/oracle_prove/aorai_ptr_field.res.oracle | 1 -
src/plugins/aorai/tests/ya/serial.ya | 10 +++++-----
4 files changed, 10 insertions(+), 10 deletions(-)
diff --git a/src/plugins/aorai/tests/ya/aorai_ptr_field.i b/src/plugins/aorai/tests/ya/aorai_ptr_field.i
index 9f1316be55c..24c8ffc30a7 100644
--- a/src/plugins/aorai/tests/ya/aorai_ptr_field.i
+++ b/src/plugins/aorai/tests/ya/aorai_ptr_field.i
@@ -1,5 +1,5 @@
/* 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; };
diff --git a/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle b/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle
index b9750505021..d8cb4fbaee5 100644
--- a/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle
@@ -1,5 +1,4 @@
[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;
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle
index 5d9a38bc1e4..45a91772ac3 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle
@@ -1,4 +1,3 @@
[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
diff --git a/src/plugins/aorai/tests/ya/serial.ya b/src/plugins/aorai/tests/ya/serial.ya
index 8fde0de6e29..9f995d7f19f 100644
--- a/src/plugins/aorai/tests/ya/serial.ya
+++ b/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 :
--
GitLab