From 8e67886ed13ae6eeddbc8dd753484234d0bd4183 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 21 Jan 2021 19:23:21 +0100
Subject: [PATCH] [aorai] update serial test to have more WP-friendly guards
---
.../tests/ya/oracle_prove/serial.res.oracle | 12 +-
src/plugins/aorai/tests/ya/serial.c | 20 ++-
src/plugins/aorai/tests/ya/serial.ya | 2 +-
src/plugins/aorai/tests/ya/serial_wp.ya | 159 ++++++++++++++++++
4 files changed, 179 insertions(+), 14 deletions(-)
create mode 100644 src/plugins/aorai/tests/ya/serial_wp.ya
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
index a9b85468c53..23c84d0e899 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,13 +1,9 @@
[kernel] Parsing tests/ya/serial.c (with preprocessing)
-[aorai] tests/ya/serial.c:79: Warning:
- Call to output not conforming to automaton (post-cond). Assuming it is on a dead path
-[aorai] tests/ya/serial.c:25: Warning:
- Call to output not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
-[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:98: Warning:
+[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:1359: Warning:
Calling undeclared function Frama_C_interval. Old style K&R code?
-[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:125: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:851: Warning:
Neither code nor specification for function Frama_C_interval, generating default assigns from the prototype
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:125: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:851: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 7073942e7e1..3bf7ab6cfac 100644
--- a/src/plugins/aorai/tests/ya/serial.c
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -2,11 +2,21 @@
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
*/
/* run.config_prove
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance @PROVE_OPTIONS@
+OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata @PTEST_DIR@/@PTEST_NAME@_wp.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance @PROVE_OPTIONS@
*/
#include "__fc_builtin.h"
+#ifndef FOR_WP
+#define BW_AND &
+#define BW_AND2 &
+#define BW_AND3 &
+#else
+#define BW_AND ==
+#define BW_AND2 >=
+#define BW_AND3 <=
+#endif
+
/*@ assigns \result \from \nothing;
ensures 0 <= \result < 0x100; */
int input_status(void) {
@@ -29,8 +39,8 @@ int read(int *status)
{
int s = input_status();
- if (s & 0x01) {
- *status = s & 0x0e;
+ if (s BW_AND2 0x01) {
+ *status = s BW_AND 0x0e;
return input_data();
}
@@ -56,7 +66,7 @@ void main(void)
n = 0;
continue;
}
- if (data & 0x80) { // status received
+ if (data BW_AND3 0x80) { // status received
if (n != 0) { // but data was expected
n = 0;
continue;
@@ -72,7 +82,7 @@ void main(void)
buffer[n++] = data;
if (n == 5) { // the packet is completely read
- if ((buffer[0] & 0x40) == 0) // it is a release action
+ if ((buffer[0] BW_AND 0x40) == 0) // it is a release action
{
int x = buffer[1] + 0x80 * buffer[2];
int y = buffer[3] + 0x80 * buffer[4];
diff --git a/src/plugins/aorai/tests/ya/serial.ya b/src/plugins/aorai/tests/ya/serial.ya
index 9f995d7f19f..fed4f5cf370 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 : { false } -> Error;
+Error : { true } -> Error;
Wait1 :
{ CALL(input_status) } -> StatusReq1
diff --git a/src/plugins/aorai/tests/ya/serial_wp.ya b/src/plugins/aorai/tests/ya/serial_wp.ya
new file mode 100644
index 00000000000..a796279cdbd
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/serial_wp.ya
@@ -0,0 +1,159 @@
+%init : Wait1;
+%deterministic;
+%observables: input_status, input_data, output;
+
+$x1 : int;
+$x2 : int;
+$y1 : int;
+$y2 : int;
+
+Error : { true } -> Error;
+
+Wait1 :
+ { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait1
+;
+
+Wait2 :
+ { CALL(input_status) } -> StatusReq2
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait2
+;
+
+Wait3 :
+ { CALL(input_status) } -> StatusReq3
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait3
+;
+
+Wait4 :
+ { CALL(input_status) } -> StatusReq4
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait4
+;
+
+Wait5 :
+ { CALL(input_status) } -> StatusReq5
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait5
+;
+
+StatusReq1 :
+ { input_status().\result < 1 } -> Wait1
+| { input_status().\result == 14 } -> StatusOk1
+| other -> StatusError
+;
+
+StatusReq2 :
+ { input_status().\result < 1 } -> Wait2
+| { input_status().\result == 14 } -> StatusOk2
+| other -> StatusError
+;
+
+StatusReq3 :
+ { input_status().\result < 1 } -> Wait3
+| { input_status().\result == 14 } -> StatusOk3
+| other -> StatusError
+;
+
+StatusReq4 :
+ { input_status().\result < 1 } -> Wait4
+| { input_status().\result == 14 } -> StatusOk4
+| other -> StatusError
+;
+
+StatusReq5 :
+ { input_status().\result < 1 } -> Wait5
+| { input_status().\result == 14 } -> StatusOk5
+| other -> StatusError
+;
+
+StatusError :
+ { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> DataReqE
+| { CALL(output) } -> Error
+| other -> StatusError
+;
+
+StatusOk1 :
+ { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> DataReq1
+| { CALL(output) } -> Error
+| other -> StatusOk1
+;
+
+StatusOk2 :
+ { CALL(input_status) } -> StatusReq2
+| { CALL(input_data) } -> DataReq2
+| { CALL(output) } -> Error
+| other -> StatusOk2
+;
+
+StatusOk3 :
+ { CALL(input_status) } -> StatusReq3
+| { CALL(input_data) } -> DataReq3
+| { CALL(output) } -> Error
+| other -> StatusOk3
+;
+
+StatusOk4 :
+ { CALL(input_status) } -> StatusReq4
+| { CALL(input_data) } -> DataReq4
+| { CALL(output) } -> Error
+| other -> StatusOk4
+;
+
+StatusOk5 :
+ { CALL(input_status) } -> StatusReq5
+| { CALL(input_data) } -> DataReq5
+| { CALL(output) } -> Error
+| other -> StatusOk5
+;
+
+DataReqE :
+ { RETURN(input_data) } -> Wait1
+;
+
+DataReq1 :
+ { input_data().\result <= 128 && input_data().\result != 64 } -> Wait2
+| { input_data().\result == 64 } -> Wait1
+| { input_data().\result > 128 } -> Wait1
+;
+
+DataReq2 :
+ { input_data().\result <= 128 && input_data().\result != 64 } -> Wait2
+| { input_data().\result == 64 } -> Wait1
+| { input_data().\result > 128 } $x1 := \result; -> Wait3
+;
+
+DataReq3 :
+ { input_data().\result <= 128 && input_data().\result != 64 } -> Wait2
+| { input_data().\result == 64 } -> Wait1
+| { input_data().\result > 128 } $x2 := \result; -> Wait4
+;
+
+DataReq4 :
+ { input_data().\result <= 128 && input_data().\result != 64 } -> Wait2
+| { input_data().\result == 64 } -> Wait1
+| { input_data().\result > 128 } $y1 := \result; -> Wait5
+;
+
+DataReq5 :
+ { input_data().\result <= 128 && input_data().\result != 64 } -> Wait2
+| { input_data().\result == 64 } -> Wait1
+| { input_data().\result > 128 } $y2 := \result; -> Complete
+;
+
+Complete :
+ { CALL(output) && output().x == $x1 + 128 * $x2 && output().y == $y1 + 128 * $y2 } -> Wait1
+| { CALL(output) && (output().x != $x1 + 128 * $x2 || output().y != $y1 + 128 * $y2) } -> Error
+| { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> Error
+| other -> Complete
+;
--
GitLab