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 e8f31d7d12c410b9fe704537bb36d02eeb706b05..37b9968d9332e932d18bd4d961fe0c8606140abc 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 6f35fd44384ee6713e2fcba2b8c8141febfdc79c..4c3791659969fb3fd12b879ac0ec78ad55269c7a 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 62b636da6ec0e8e6400496ef5ad8727ca0214cb0..d5aa249647d0f929f15b6ea15f3079409953728e 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 b0cac6b01b25d96355241a543e34d95d5818b2ca..6c033979bd1de21bc5c66b78abefa5fbbecd8e26 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 a721d8db11216ab7be3d6b63317fa08393df9473..f123a10ea1d4899ff824644d1c5a355cbde2c03f 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 f113e21eac4377c67da6c6c364e25564a3e778a5..bc1980f8dd6c6868c498af6df66a1fe4807b206b 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 694a3817026e82af27d0e838b2533c54dbc3baf6..923b8de4a8696df470651d5d6c41c73eb33aaa98 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 a5a1b263a40e8a838d4fe35a43b3b6cd12fce6f1..c813ffb28c36688e5a55a25d199070d18baa59e1 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 6f46969556260e169dd1f26d050cdae831719329..3e76cd392c78a6744e7ab6e97911684a0353a815 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 a52a7c7881ae98d4f7a8021ef0f28b85bc7b698f..d3769b352d33da71077733114223d69059d67c7a 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 34366aa9fd40d3c26130b980494067d8a27b055a..2f0e7ce8e84ab43d8cba663cecc7766c1d3d8f73 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 0c22ea3ad2c717deed55f7fd804d2d8cf012610d..1a40c608459f2eabd9189ba8c1374eb87f5663b3 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 df2ece4c7b586cdaf2e3dcf2220556efe75f4534..4e77b2b2d82c624882c4cf7e1996d96a3a3a53f2 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 4aa48e2ee5d7fa37f6d81627004ac5e7f4955b9d..9257d2c5d17a1376ece0f36e6266d24c35657853 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 260cb460abb1c282a351d5544b232ff3f342f913..7d8927d391b2e483f1aacb22b9387b8794098d3c 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 2d23df5c6afed4801e4a1526868dc0b631dc31f2..67b68e9ab8ce82621e6b83f8ddc7066482f4d57c 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 94078981b439ae01e7706cb954d299d2fe5d43d8..eb4fbb3195124e602785ea9f55efa0161e20105b 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 3caffe84fad47612be18e7e4c3fec7446a18c2c2..36fba5e9a2d04d52b622e0a3b0568d069c3e8b55 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 e2e3a4fe94ea87191bbb7caa3162cf0bc7f927e5..05170397e238edc619affe696d5404119fa60430 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 f83db815ae931852f8760e80e33016d64bfa76e4..7879583a70dd773cd54f39c03ff52d1251861310 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 b2f0a865f3d5c032ce7fbb3fca1f315091ada68d..4c0723689a86db3c32bfe5df30121f87991842ed 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 bae62a6316898061fab0f135c5d8568de8d0e381..b256e59ddb8d0654c2d0c6a2a794045b9ac22c13 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 bc811deb4c000e56efe88e9f6b1c96c59a0e234e..0b47507c6a2054e9e7352bfdce2a60e6174ba412 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 d6155c7faefc43a976157b9d44ee8eae1a3016e2..843d3f17a658bb06d8c331b1b18d58f9c03ef5a7 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 2b50360158fb85efec7991a9ae0405c2d4cf4af8..e59b671a435d7944dbe7c3aa9757b967206ebaad 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 460a3a7b4fc13a991b6bc77d4feb772e01258dba..da7359cdf61dccd1fcf9f8ce3f6696cc4032efb4 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 967ab213ada1147a808d7fe46b38741cbd42c446..4071686554d5628c250e63e0f5ae8ba494fb2903 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 c2fc72913e5f6c258e29064424942812828bf85e..e31ea6083264fd52bf1004dc3636195c6286f40f 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 59019d29de575c9d3c002abce06057b5d09f7361..6b1289c2a6d4bd4088ecc020cf530f9a0f6afbb1 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 1431fa716c3b4d91756d07526ea2c633f1174e1f..bc444e4bbcc155c9a6583fa490dc91905ea42ea4 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 56ba35bfc725a9e244a5be663abe9017446ccff9..429ca9bc1e86351a9db4ad2e0433457dd3de6063 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 8c9faad26773d78513719836e6856f9cfd4abbb8..58125fc6e68b3c1c0076f63159238ddf0660ea4e 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 c7e017d08d504c11ddbf2c410794c4ab96b2c667..84601f1f62169f47d3e5cd4cebb7a384a421f840 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 541b2c925a348a01a2ed36158f45f14207a5d55a..ecdc65fc67cbbff2acf74871a9420f36ed70efc1 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 7d5d9b9a27ffa3af3cfee2f8c7c4a62d0ad02977..c06fe39d324009a48386b8d03101495e7bc319c6 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 8b6bdc8c2cc9b20df7e9ad0f3a7725e26d9855f8..cdc7824e878babe57e329155cace996037d20b38 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