From 60de7eb71b846ea26c34cd084e4a5c6d02d51a21 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 12 Jan 2021 13:15:55 +0100
Subject: [PATCH] [aorai] update test to check full behavior of
Frama_C_show_aorai_state
---
src/plugins/aorai/tests/ya/oracle/serial.res.oracle | 10 +++++++++-
src/plugins/aorai/tests/ya/serial.c | 2 +-
2 files changed, 10 insertions(+), 2 deletions(-)
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index a1dde62c222..5f1197b44ca 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -23,11 +23,17 @@
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 100 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 300 states
[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 500 states
[eva:alarm] tests/ya/serial.c:52: Warning:
accessing uninitialized left-value. assert \initialized(&status);
@@ -36,7 +42,9 @@
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1200 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1500 states
[aorai] tests/ya/serial.c:79: Error <- Error <- Error
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
[aorai] tests/ya/serial.c:79: Error <- Error <- Error
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1700 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1900 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2000 states
@@ -675,7 +683,7 @@ void main(void)
int x = buffer[1] + 0x80 * buffer[2];
int y = buffer[3] + 0x80 * buffer[4];
output(x,y);
- Frama_C_show_aorai_state();
+ Frama_C_show_aorai_state(n,x,y);
}
n = 0;
}
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 8afcc7533fb..43d67d6540f 100644
--- a/src/plugins/aorai/tests/ya/serial.c
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -76,7 +76,7 @@ void main(void)
output(x, y);
/* "Error" state should show up as, for now, it is hard to prove
the metavariable équation in the input automaton */
- Frama_C_show_aorai_state();
+ Frama_C_show_aorai_state(n,x,y);
}
n = 0;
--
GitLab