From c701391a453e0258715213fb9ddf50b7fc760953 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 19 Apr 2023 10:52:20 +0200
Subject: [PATCH] [Eva] Updates test oracles.
---
.../ya/oracle/aorai_ptr_field.res.oracle | 2 +
.../tests/ya/oracle/assigns.0.res.oracle | 4 ++
.../tests/ya/oracle/assigns.1.res.oracle | 4 ++
.../tests/ya/oracle/bts1289.0.res.oracle | 4 ++
.../tests/ya/oracle/bts1289.1.res.oracle | 4 ++
.../ya/oracle/declared_function.res.oracle | 2 +
.../tests/ya/oracle/deterministic.res.oracle | 8 ++++
.../aorai/tests/ya/oracle/floats.res.oracle | 6 +++
.../aorai/tests/ya/oracle/formals.res.oracle | 6 +++
.../tests/ya/oracle/function_ptr.res.oracle | 6 +++
.../generate_assigns_bts1290.res.oracle | 2 +
.../tests/ya/oracle/hoare_seq.res.oracle | 4 ++
.../tests/ya/oracle/incorrect.res.oracle | 2 +
.../ya/oracle/logical_operators.res.oracle | 4 ++
.../tests/ya/oracle/loop_bts1050.res.oracle | 6 +++
.../ya/oracle/metavariables-right.res.oracle | 10 +++++
.../tests/ya/oracle/monostate.res.oracle | 4 ++
.../aorai/tests/ya/oracle/not_prm.res.oracle | 2 +
.../aorai/tests/ya/oracle/observed.res.oracle | 4 ++
.../aorai/tests/ya/oracle/other.res.oracle | 6 +++
.../aorai/tests/ya/oracle/seq.res.oracle | 6 +++
.../aorai/tests/ya/oracle/seq_loop.res.oracle | 6 +++
.../tests/ya/oracle/seq_unlimited.res.oracle | 6 +++
.../aorai/tests/ya/oracle/serial.res.oracle | 40 +++++++++----------
.../tests/ya/oracle/single_call.res.oracle | 2 +
.../oracle/singleassignment-right.res.oracle | 2 +
.../aorai/tests/ya/oracle/stack.res.oracle | 6 +++
.../ya/oracle/test_acces_params.res.oracle | 6 +++
.../ya/oracle/test_acces_params2.res.oracle | 8 ++++
.../test_boucle_rechercheTableau.res.oracle | 6 +++
.../tests/ya/oracle/test_factorial.res.oracle | 6 +++
.../ya/oracle/test_recursion4.res.oracle | 6 +++
.../ya/oracle/test_recursion5.res.oracle | 8 ++++
.../tests/ya/oracle/test_struct.res.oracle | 4 ++
tests/libc/oracle/fc_libc.1.res.oracle | 4 +-
tests/spec/oracle/kw.res.oracle | 2 +-
36 files changed, 185 insertions(+), 23 deletions(-)
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 e8f31d7d12c..37b9968d933 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
@@ -44,6 +44,7 @@ enum aorai_OpStatusList {
int S0_tmp;
int S1_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -93,6 +94,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/assigns.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
index 6f35fd44384..4c379165996 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
@@ -74,6 +74,7 @@ int X;
int Sf_tmp;
int in_main_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S1_tmp = S1;
@@ -153,6 +154,7 @@ int X;
int Sf_tmp;
int in_main_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S1_tmp = S1;
@@ -247,6 +249,7 @@ void f(void)
int Sf_tmp;
int in_main_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -326,6 +329,7 @@ void f(void)
int Sf_tmp;
int in_main_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
index 62b636da6ec..d5aa249647d 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -71,6 +71,7 @@ int X;
void f_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if ((unsigned int)3 == aorai_CurStates) aorai_CurStates = S_in_f;
@@ -118,6 +119,7 @@ int X;
void f_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = in_main;
@@ -178,6 +180,7 @@ void f(void)
void main_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = Sf;
@@ -225,6 +228,7 @@ void f(void)
void main_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if ((unsigned int)5 == aorai_CurStates) aorai_CurStates = S2;
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
index b0cac6b01b2..6c033979bd1 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
@@ -31,6 +31,7 @@ enum aorai_OpStatusList {
{
int S_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_a;
S_tmp = S;
@@ -59,6 +60,7 @@ enum aorai_OpStatusList {
{
int S_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_a;
S_tmp = S;
@@ -98,6 +100,7 @@ void a(void)
{
int S_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S_tmp = S;
@@ -126,6 +129,7 @@ void a(void)
{
int S_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S_tmp = S;
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
index a721d8db112..f123a10ea1d 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -79,6 +79,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_0_tmp;
int init_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_a;
S_tmp = S;
@@ -166,6 +167,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_0_tmp;
int init_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_a;
S_tmp = S;
@@ -284,6 +286,7 @@ void a(void)
int aorai_intermediate_state_0_tmp;
int init_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S_tmp = S;
@@ -364,6 +367,7 @@ void a(void)
int aorai_intermediate_state_0_tmp;
int init_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S_tmp = S;
diff --git a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
index f113e21eac4..bc1980f8dd6 100644
--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -72,6 +72,7 @@ check lemma I_deterministic_trans{L}:
void main_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = I;
@@ -107,6 +108,7 @@ check lemma I_deterministic_trans{L}:
void main_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = I;
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 694a3817026..923b8de4a86 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -116,6 +116,7 @@ check lemma S0_deterministic_trans{L}:
void g_pre_func(int x)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
if ((unsigned int)3 == aorai_CurStates) {
@@ -185,6 +186,7 @@ check lemma S0_deterministic_trans{L}:
void g_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
if ((unsigned int)5 == aorai_CurStates) aorai_CurStates = S1;
@@ -263,6 +265,7 @@ void g(int x)
void f_pre_func(int x)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if ((unsigned int)1 == aorai_CurStates)
@@ -321,6 +324,7 @@ void g(int x)
void f_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if ((unsigned int)1 == aorai_CurStates)
@@ -407,6 +411,7 @@ int f(int x)
void real_main_pre_func(int c)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_real_main;
if ((unsigned int)0 == aorai_CurStates) {
@@ -471,6 +476,7 @@ int f(int x)
void real_main_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_real_main;
if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = Sf;
@@ -543,6 +549,7 @@ int real_main(int c)
void main_pre_func(int c)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if ((unsigned int)7 == aorai_CurStates) aorai_CurStates = S0;
@@ -599,6 +606,7 @@ int real_main(int c)
void main_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if ((unsigned int)6 == aorai_CurStates) aorai_CurStates = Sf;
diff --git a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
index a5a1b263a40..c813ffb28c3 100644
--- a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
@@ -173,6 +173,7 @@ check lemma B_deterministic_trans{L}:
void square_root_aux_pre_func(float x, float n)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_square_root_aux;
if ((unsigned int)1 == aorai_CurStates)
@@ -223,6 +224,7 @@ check lemma B_deterministic_trans{L}:
void square_root_aux_post_func(float res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_square_root_aux;
if ((unsigned int)1 == aorai_CurStates) aorai_CurStates = B;
@@ -301,6 +303,7 @@ float square_root_aux(float x, float n)
void square_root_pre_func(float n)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_square_root;
if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = B;
@@ -348,6 +351,7 @@ float square_root_aux(float x, float n)
void square_root_post_func(float res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_square_root;
if ((unsigned int)1 == aorai_CurStates) aorai_CurStates = C;
@@ -409,6 +413,7 @@ float square_root(float n)
void main_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if ((unsigned int)4 == aorai_CurStates) aorai_CurStates = A;
@@ -456,6 +461,7 @@ float square_root(float n)
void main_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = E;
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 6f469695562..3e76cd392c7 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -139,6 +139,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
void f_pre_func(int x)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if ((unsigned int)7 == aorai_CurStates) {
@@ -238,6 +239,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
void f_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if ((unsigned int)4 == aorai_CurStates) {
@@ -394,6 +396,7 @@ int f(int x)
void g_pre_func(int y)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = OK;
@@ -474,6 +477,7 @@ int f(int x)
void g_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
if ((unsigned int)3 == aorai_CurStates) {
@@ -575,6 +579,7 @@ int g(int y)
void main_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if ((unsigned int)6 == aorai_CurStates) aorai_CurStates = main_0;
@@ -633,6 +638,7 @@ int g(int y)
void main_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = OK;
diff --git a/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle b/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
index a52a7c7881a..d3769b352d3 100644
--- a/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
@@ -121,6 +121,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
void f_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if ((unsigned int)9 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state;
@@ -189,6 +190,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
void f_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = f_called;
@@ -275,6 +277,7 @@ void f(void)
void g_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
if ((unsigned int)9 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state_0;
@@ -343,6 +346,7 @@ void f(void)
void g_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
if ((unsigned int)1 == aorai_CurStates) aorai_CurStates = g_called;
@@ -424,6 +428,7 @@ void g(void)
void main_pre_func(int c)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if ((unsigned int)7 == aorai_CurStates) aorai_CurStates = s1;
@@ -483,6 +488,7 @@ void g(void)
void main_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if ((unsigned int)8 == aorai_CurStates) aorai_CurStates = ok;
diff --git a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
index 34366aa9fd4..2f0e7ce8e84 100644
--- a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
@@ -34,6 +34,7 @@ enum aorai_OpStatusList {
{
int S_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S_tmp = S;
@@ -67,6 +68,7 @@ enum aorai_OpStatusList {
{
int S_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S_tmp = S;
diff --git a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
index 0c22ea3ad2c..1a40c608459 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -116,6 +116,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_2_tmp;
int aorai_reject_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -244,6 +245,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_2_tmp;
int aorai_reject_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -440,6 +442,7 @@ int main_bhv_bhv(int c); */
int aorai_intermediate_state_2_tmp;
int aorai_reject_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -584,6 +587,7 @@ int main_bhv_bhv(int c); */
int aorai_intermediate_state_2_tmp;
int aorai_reject_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
index df2ece4c7b5..4e77b2b2d82 100644
--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -44,6 +44,7 @@ int f(void);
void main_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
aorai_CurStates = aorai_reject;
@@ -73,6 +74,7 @@ int f(void);
void main_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
aorai_CurStates = aorai_reject;
diff --git a/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle b/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
index 4aa48e2ee5d..9257d2c5d17 100644
--- a/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
@@ -36,6 +36,7 @@ enum aorai_OpStatusList {
{
int I_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
I_tmp = I;
@@ -77,6 +78,7 @@ enum aorai_OpStatusList {
{
int I_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
I_tmp = I;
@@ -124,6 +126,7 @@ void f(int x)
{
int I_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
I_tmp = I;
@@ -157,6 +160,7 @@ void f(int x)
{
int I_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
I_tmp = I;
diff --git a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
index 260cb460abb..7d8927d391b 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -129,6 +129,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -259,6 +260,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -415,6 +417,7 @@ void f(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -538,6 +541,7 @@ void f(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -680,6 +684,7 @@ void g(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -804,6 +809,7 @@ void g(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
index 2d23df5c6af..67b68e9ab8c 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -120,6 +120,7 @@ check lemma e_deterministic_trans{L}:
void f_pre_func(int x)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if ((unsigned int)2 == aorai_CurStates) {
@@ -183,6 +184,7 @@ check lemma e_deterministic_trans{L}:
void f_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if ((unsigned int)3 == aorai_CurStates) aorai_CurStates = e;
@@ -260,6 +262,7 @@ void f(int x)
void g_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = d;
@@ -319,6 +322,7 @@ void f(int x)
void g_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
if ((unsigned int)4 == aorai_CurStates) aorai_CurStates = g_0;
@@ -391,6 +395,7 @@ void g(void)
void h_pre_func(int x)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_h;
if ((unsigned int)5 == aorai_CurStates)
@@ -452,6 +457,7 @@ void g(void)
void h_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_h;
if ((unsigned int)6 == aorai_CurStates) aorai_CurStates = g_0;
@@ -524,6 +530,7 @@ void h(int x)
void i_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_i;
if ((unsigned int)7 == aorai_CurStates) aorai_CurStates = h_0;
@@ -594,6 +601,7 @@ void h(int x)
void i_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_i;
if ((unsigned int)8 == aorai_CurStates) {
@@ -675,6 +683,7 @@ void i(void)
void main_pre_func(int t)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = b;
@@ -734,6 +743,7 @@ void i(void)
void main_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if ((unsigned int)5 == aorai_CurStates) aorai_CurStates = i_0;
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index 94078981b43..eb4fbb31951 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -69,6 +69,7 @@ check lemma Init_deterministic_trans{L}:
void f_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = aorai_reject;
@@ -109,6 +110,7 @@ check lemma Init_deterministic_trans{L}:
void f_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = aorai_reject;
@@ -160,6 +162,7 @@ void f(void)
void main_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
aorai_CurStates = aorai_reject;
@@ -192,6 +195,7 @@ void f(void)
void main_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
aorai_CurStates = aorai_reject;
diff --git a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
index 3caffe84fad..36fba5e9a2d 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -41,6 +41,7 @@ enum aorai_OpStatusList {
int S0_tmp;
int Sf_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -84,6 +85,7 @@ enum aorai_OpStatusList {
int S0_tmp;
int Sf_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index e2e3a4fe94e..05170397e23 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -74,6 +74,7 @@ enum aorai_OpStatusList {
int first_step_tmp;
int init_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
aorai_intermediate_state_tmp = aorai_intermediate_state;
@@ -156,6 +157,7 @@ enum aorai_OpStatusList {
int first_step_tmp;
int init_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
aorai_intermediate_state_tmp = aorai_intermediate_state;
@@ -325,6 +327,7 @@ void g(void)
int first_step_tmp;
int init_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_h;
aorai_intermediate_state_tmp = aorai_intermediate_state;
@@ -407,6 +410,7 @@ void g(void)
int first_step_tmp;
int init_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_h;
aorai_intermediate_state_tmp = aorai_intermediate_state;
diff --git a/src/plugins/aorai/tests/ya/oracle/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
index f83db815ae9..7879583a70d 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -70,6 +70,7 @@ int x = 0;
int last_tmp;
int step1_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
init_tmp = init;
@@ -173,6 +174,7 @@ int x = 0;
int last_tmp;
int step1_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
init_tmp = init;
@@ -340,6 +342,7 @@ void f(void)
int last_tmp;
int step1_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
init_tmp = init;
@@ -443,6 +446,7 @@ void f(void)
int last_tmp;
int step1_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
init_tmp = init;
@@ -597,6 +601,7 @@ void g(void)
int last_tmp;
int step1_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
init_tmp = init;
@@ -671,6 +676,7 @@ void g(void)
int last_tmp;
int step1_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
init_tmp = init;
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index b2f0a865f3d..4c0723689a8 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -114,6 +114,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -237,6 +238,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -406,6 +408,7 @@ void f(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -539,6 +542,7 @@ void f(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -705,6 +709,7 @@ void g(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -829,6 +834,7 @@ void g(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
index bae62a63168..b256e59ddb8 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -129,6 +129,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -259,6 +260,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -415,6 +417,7 @@ void f(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -538,6 +541,7 @@ void f(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -680,6 +684,7 @@ void g(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -804,6 +809,7 @@ void g(void)
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
index bc811deb4c0..0b47507c6a2 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
@@ -93,6 +93,7 @@ check lemma aorai_intermediate_state_0_deterministic_trans{L}:
void init_pre_func(int *a, int n)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_init;
if ((unsigned int)4 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state;
@@ -146,6 +147,7 @@ check lemma aorai_intermediate_state_0_deterministic_trans{L}:
void init_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_init;
if ((unsigned int)0 == aorai_CurStates) aorai_CurStates = c;
@@ -235,6 +237,7 @@ void init(int *a, int n)
void find_pre_func(int *a, int n, int k)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_find;
if ((unsigned int)5 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state_1;
@@ -290,6 +293,7 @@ void init(int *a, int n)
void find_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_find;
if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state_0;
@@ -394,6 +398,7 @@ int find(int *a, int n, int k)
void main_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if ((unsigned int)6 == aorai_CurStates) aorai_CurStates = b;
@@ -447,6 +452,7 @@ int find(int *a, int n, int k)
void main_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if ((unsigned int)1 == aorai_CurStates) aorai_CurStates = ok;
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index d6155c7faef..843d3f17a65 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -20,28 +20,24 @@
[eva] using specification for function Frama_C_interval
[eva] serial.c:58: starting to merge loop iterations
[eva] serial.c:63: Trace partitioning superposing up to 100 states
-[eva] serial.c:63: Trace partitioning superposing up to 300 states
+[eva] serial.c:63: Trace partitioning superposing up to 200 states
[eva:alarm] serial.c:33: Warning:
assertion 'Aorai,aorai_smoke_test' got status invalid (stopping propagation).
[aorai] serial.c:92: Wait1 <- Wait1 <- Complete
-[aorai] serial.c:92: n in {5},x in [0..16383],y in [8192..16383]
-[aorai] serial.c:92: Wait1 <- Wait1 <- Complete
-[aorai] serial.c:92: n in {5},x in [0..16383],y in [0..8191]
-[eva] serial.c:63: Trace partitioning superposing up to 500 states
-[eva] serial.c:63: Trace partitioning superposing up to 700 states
+[aorai] serial.c:92: n in {5},x in [0..16383],y in [0..16383]
+[eva] serial.c:63: Trace partitioning superposing up to 400 states
+[eva] serial.c:63: Trace partitioning superposing up to 600 states
+[eva] serial.c:63: Trace partitioning superposing up to 800 states
[eva] serial.c:63: Trace partitioning superposing up to 900 states
-[eva] serial.c:63: Trace partitioning superposing up to 1200 states
-[eva] serial.c:63: Trace partitioning superposing up to 1400 states
-[eva] serial.c:63: Trace partitioning superposing up to 1500 states
-[eva] serial.c:63: Trace partitioning superposing up to 1600 states
-[eva] serial.c:63: Trace partitioning superposing up to 1700 states
+[eva] serial.c:63: Trace partitioning superposing up to 1000 states
+[eva] serial.c:63: Trace partitioning superposing up to 1100 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function input_data_post_func:
aorai_x1 ∈ [0..127]
aorai_x2 ∈ [0..127]
aorai_y1 ∈ [0..127]
- aorai_y2 ∈ [0..2147483647]
+ aorai_y2 ∈ [0..127]
aorai_CurOperation ∈ {op_input_data}
aorai_CurOpStatus ∈ {aorai_Terminated}
aorai_CurStates ∈ {Complete; Wait1; Wait2; Wait3; Wait4; Wait5}
@@ -59,7 +55,7 @@
aorai_x1 ∈ [0..127]
aorai_x2 ∈ [0..127]
aorai_y1 ∈ [0..127]
- aorai_y2 ∈ [0..2147483647]
+ aorai_y2 ∈ [0..127]
aorai_CurOperation ∈ {op_input_data}
aorai_CurOpStatus ∈ {aorai_Terminated}
aorai_CurStates ∈ {Complete; Wait1; Wait2; Wait3; Wait4; Wait5}
@@ -115,7 +111,7 @@
aorai_x1 ∈ [0..127]
aorai_x2 ∈ [0..127]
aorai_y1 ∈ [0..127]
- aorai_y2 ∈ [0..2147483647]
+ aorai_y2 ∈ [0..127]
aorai_CurOperation ∈ {op_input_status; op_input_data}
aorai_CurOpStatus ∈ {aorai_Terminated}
aorai_CurStates ∈ {Complete; Wait1; Wait2; Wait3; Wait4; Wait5}
@@ -124,13 +120,12 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
buffer[0] ∈ {0} ∪ [128..255]
- [1..2] ∈ [0..127]
- [3..4] ∈ [0..2147483647]
+ [1..4] ∈ [0..127]
n ∈ {0; 1; 2; 3; 4}
aorai_x1 ∈ [0..127]
aorai_x2 ∈ [0..127]
aorai_y1 ∈ [0..127]
- aorai_y2 ∈ [0..2147483647]
+ aorai_y2 ∈ [0..127]
aorai_CurOperation ∈ {op_output; op_input_status; op_input_data}
aorai_CurOpStatus ∈ {aorai_Called; aorai_Terminated}
aorai_CurStates ∈ {Complete; Wait1; Wait2; Wait3; Wait4; Wait5}
@@ -218,6 +213,7 @@ int n = 0;
void input_status_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_input_status;
aorai_StatesHistory_2 = aorai_StatesHistory_1;
@@ -257,6 +253,7 @@ int n = 0;
void input_status_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_input_status;
aorai_StatesHistory_2 = aorai_StatesHistory_1;
@@ -403,6 +400,7 @@ int input_status(void)
void input_data_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_input_data;
aorai_StatesHistory_2 = aorai_StatesHistory_1;
@@ -440,6 +438,7 @@ int input_status(void)
void input_data_post_func(int res)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_input_data;
aorai_StatesHistory_2 = aorai_StatesHistory_1;
@@ -584,6 +583,7 @@ int input_data(void)
void output_pre_func(int x, int y)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_output;
aorai_StatesHistory_2 = aorai_StatesHistory_1;
@@ -636,6 +636,7 @@ int input_data(void)
void output_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_output;
aorai_StatesHistory_2 = aorai_StatesHistory_1;
@@ -690,11 +691,10 @@ void main(void)
n = 0;
continue;
}
- }
- else {
/*@ split data & 0x40; */ ;
- if (n == 0) continue;
}
+ else
+ if (n == 0) continue;
tmp_0 = n;
n ++;
buffer[tmp_0] = data;
diff --git a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
index 2b50360158f..e59b671a435 100644
--- a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
@@ -55,6 +55,7 @@ enum aorai_OpStatusList {
int Sf_tmp;
int aorai_intermediate_state_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -114,6 +115,7 @@ enum aorai_OpStatusList {
int Sf_tmp;
int aorai_intermediate_state_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
index 460a3a7b4fc..da7359cdf61 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
@@ -70,6 +70,7 @@ enum aorai_OpStatusList {
void main_pre_func(int *x, int *y)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if ((unsigned int)0 == aorai_CurStates) {
@@ -126,6 +127,7 @@ enum aorai_OpStatusList {
void main_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if ((unsigned int)2 == aorai_CurStates) {
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index 967ab213ada..4071686554d 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -97,6 +97,7 @@ check lemma emptying_stack_deterministic_trans{L}:
void push_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_push;
if ((unsigned int)4 == aorai_CurStates) aorai_CurStates = filling_stack;
@@ -155,6 +156,7 @@ check lemma emptying_stack_deterministic_trans{L}:
void push_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_push;
if ((unsigned int)5 == aorai_CurStates) {
@@ -235,6 +237,7 @@ void push(void)
void pop_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_pop;
if ((unsigned int)4 == aorai_CurStates)
@@ -301,6 +304,7 @@ void push(void)
void pop_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_pop;
if ((unsigned int)3 == aorai_CurStates) {
@@ -398,6 +402,7 @@ void pop(void)
void main_pre_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if ((unsigned int)6 == aorai_CurStates) {
@@ -451,6 +456,7 @@ void pop(void)
void main_post_func(void)
{
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if ((unsigned int)2 == aorai_CurStates) aorai_CurStates = accept;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
index c2fc72913e5..e31ea608326 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
@@ -88,6 +88,7 @@ int rr = 1;
int SF_tmp;
int mainst_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opa;
S1_tmp = S1;
@@ -180,6 +181,7 @@ int rr = 1;
int SF_tmp;
int mainst_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opa;
S1_tmp = S1;
@@ -292,6 +294,7 @@ void opa(int i, int j)
int SF_tmp;
int mainst_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opb;
S1_tmp = S1;
@@ -383,6 +386,7 @@ void opa(int i, int j)
int SF_tmp;
int mainst_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opb;
S1_tmp = S1;
@@ -495,6 +499,7 @@ int opb(void)
int SF_tmp;
int mainst_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -585,6 +590,7 @@ int opb(void)
int SF_tmp;
int mainst_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
index 59019d29de5..6b1289c2a6d 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
@@ -96,6 +96,7 @@ int rr = 1;
int S6_tmp;
int S7_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opa;
S1_tmp = S1;
@@ -199,6 +200,7 @@ int rr = 1;
int S6_tmp;
int S7_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opa;
S1_tmp = S1;
@@ -326,6 +328,7 @@ int opa(int r)
int S6_tmp;
int S7_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opb;
S1_tmp = S1;
@@ -426,6 +429,7 @@ int opa(int r)
int S6_tmp;
int S7_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opb;
S1_tmp = S1;
@@ -541,6 +545,7 @@ void opb(void)
int S6_tmp;
int S7_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opc;
S1_tmp = S1;
@@ -634,6 +639,7 @@ void opb(void)
int S6_tmp;
int S7_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opc;
S1_tmp = S1;
@@ -768,6 +774,7 @@ void opc(void)
int S6_tmp;
int S7_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -868,6 +875,7 @@ void opc(void)
int S6_tmp;
int S7_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
index 1431fa716c3..bc444e4bbcc 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
@@ -55,6 +55,7 @@ enum aorai_OpStatusList {
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -113,6 +114,7 @@ enum aorai_OpStatusList {
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -225,6 +227,7 @@ int isPresent(int *t, int max, int val)
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -277,6 +280,7 @@ int isPresent(int *t, int max, int val)
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -342,6 +346,7 @@ void foo(void)
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
End_tmp = End;
@@ -394,6 +399,7 @@ void foo(void)
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
End_tmp = End;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
index 56ba35bfc72..429ca9bc1e8 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -49,6 +49,7 @@ enum aorai_OpStatusList {
int S2_tmp;
int main_0_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_decode_int;
S1_tmp = S1;
@@ -104,6 +105,7 @@ enum aorai_OpStatusList {
int S2_tmp;
int main_0_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_decode_int;
S1_tmp = S1;
@@ -234,6 +236,7 @@ int decode_int(char *s)
int S2_tmp;
int main_0_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_factorial;
S1_tmp = S1;
@@ -291,6 +294,7 @@ int decode_int(char *s)
int S2_tmp;
int main_0_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_factorial;
S1_tmp = S1;
@@ -372,6 +376,7 @@ int factorial(int value)
int S2_tmp;
int main_0_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -427,6 +432,7 @@ int factorial(int value)
int S2_tmp;
int main_0_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
index 8c9faad2677..58125fc6e68 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -52,6 +52,7 @@ enum aorai_OpStatusList {
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -116,6 +117,7 @@ enum aorai_OpStatusList {
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -231,6 +233,7 @@ int isPresent(int *t, int size, int val)
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -283,6 +286,7 @@ int isPresent(int *t, int size, int val)
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -348,6 +352,7 @@ void foo(void)
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
End_tmp = End;
@@ -400,6 +405,7 @@ void foo(void)
int Idle_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
End_tmp = End;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
index c7e017d08d5..84601f1f621 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -71,6 +71,7 @@ enum aorai_OpStatusList {
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_isPresentRec;
End_tmp = End;
@@ -154,6 +155,7 @@ enum aorai_OpStatusList {
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_isPresentRec;
End_tmp = End;
@@ -285,6 +287,7 @@ int isPresentRec(int *t, int i, int max, int val)
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -361,6 +364,7 @@ int isPresentRec(int *t, int i, int max, int val)
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -463,6 +467,7 @@ int isPresent(int *t, int max, int val)
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -532,6 +537,7 @@ int isPresent(int *t, int max, int val)
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -615,6 +621,7 @@ void foo(void)
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
End_tmp = End;
@@ -684,6 +691,7 @@ void foo(void)
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
End_tmp = End;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
index 541b2c925a3..ecdc65fc67c 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -50,6 +50,7 @@ int myAge = 0;
int S1_tmp;
int main_0_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_increment;
S1_tmp = S1;
@@ -96,6 +97,7 @@ int myAge = 0;
int S1_tmp;
int main_0_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_increment;
S1_tmp = S1;
@@ -159,6 +161,7 @@ void increment(void)
int S1_tmp;
int main_0_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -205,6 +208,7 @@ void increment(void)
int S1_tmp;
int main_0_tmp;
/@ slevel full; @/
+ ;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 7d5d9b9a27f..c06fe39d324 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4553,7 +4553,7 @@ int getaddrinfo(char const * restrict nodename,
}
tmp_3 = Frama_C_interval(0,43);
sa->sa_family = (sa_family_t)tmp_3;
- /*@ slevel 15; */
+ /*@ slevel 15; */ ;
{
int i = 0;
while (i < 14) {
@@ -4565,7 +4565,7 @@ int getaddrinfo(char const * restrict nodename,
i ++;
}
}
- /*@ slevel default; */
+ /*@ slevel default; */ ;
ai->ai_flags = 0;
ai->ai_family = (int)sa->sa_family;
ai->ai_socktype = Frama_C_interval(0,5);
diff --git a/tests/spec/oracle/kw.res.oracle b/tests/spec/oracle/kw.res.oracle
index 8b6bdc8c2cc..cdc7824e878 100644
--- a/tests/spec/oracle/kw.res.oracle
+++ b/tests/spec/oracle/kw.res.oracle
@@ -30,7 +30,7 @@ int main(void)
struct custom writes;
struct at include;
struct loop assert;
- /*@ slevel 4; */
+ /*@ slevel 4; */ ;
behavior ++;
/*@
assert
--
GitLab