diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle index a1dde62c222737a8ba75bf5599a8fc7c642b7925..5f1197b44ca72486f0810f627d81a87e6e568c7a 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 8afcc7533fb16ccfc3726a32c5d95267a0f8a2bc..43d67d6540f64dea2e4b36b1dc03203095ec9694 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;