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/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 2ccf27969ed46fad6a08704b096a9ecf824fc026..2a0c7af021ac216b6eae8cea7f8315e3604f3ece 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -464,7 +464,7 @@ module Make_Dataflow
end;
(* Get vertex store *)
let store = get_vertex_store v in
- (* Join incoming s tates *)
+ (* Join incoming states *)
let flow = Partitioning.join sources store in
let flow =
match v.vertex_start_of with
diff --git a/src/plugins/eva/partitioning/partition.ml b/src/plugins/eva/partitioning/partition.ml
index f0b7663f535570ad0678aa5c6f3f4617de67430c..14723800087101c1b1049d3fd7a0b910ff631278 100644
--- a/src/plugins/eva/partitioning/partition.ml
+++ b/src/plugins/eva/partitioning/partition.ml
@@ -655,8 +655,8 @@ struct
in
List.fold_left transfer [] p
- let iter (f : state -> unit) (p : t) : unit =
- List.iter (fun (_k,x) -> f x) p
+ let iter (f : key -> state -> unit) (p : t) : unit =
+ List.iter (fun (k, x) -> f k x) p
let join_duplicate_keys (p : t) : t =
let cmp (k, _) (k', _) = Key.compare k k' in
diff --git a/src/plugins/eva/partitioning/partition.mli b/src/plugins/eva/partitioning/partition.mli
index e1f6d42ab427ffc10fd192ba905db7fb1737731d..caf4e08c2487c27dba54be9916b43945669c14d4 100644
--- a/src/plugins/eva/partitioning/partition.mli
+++ b/src/plugins/eva/partitioning/partition.mli
@@ -195,7 +195,7 @@ sig
val transfer : ((key * state) -> (key * state) list) -> t -> t
val transfer_keys : t -> action -> t
- val iter : (state -> unit) -> t -> unit
+ val iter : (key -> state -> unit) -> t -> unit
val filter_map: (key -> state -> state option) -> t -> t
val join_duplicate_keys: t -> t
diff --git a/src/plugins/eva/partitioning/trace_partitioning.ml b/src/plugins/eva/partitioning/trace_partitioning.ml
index 6e0868ccf242c011ba4763e2f0a5649a59eaae2f..2e38c548ff027ad0587432d265d6e0beaff02f6a 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.ml
+++ b/src/plugins/eva/partitioning/trace_partitioning.ml
@@ -42,8 +42,8 @@ struct
type state = Domain.t
type store = {
- rationing: Partition.rationing; (* slevel rationing at this point *)
flow_actions : action list; (* partitioning actions to be applied *)
+ rationing: bool; (* Is there a slevel rationing in above actions? *)
store_stmt : stmt option;
store_index : Index.t; (* Index of all states stored: used to quickly remove
new states that have already been propagated. *)
@@ -72,13 +72,27 @@ struct
(* Constructors *)
let empty_store ~(stmt : stmt option) : store =
- let limit, merge, flow_actions = match stmt with
- | None -> max_int, false, []
- | Some stmt -> slevel stmt, merge stmt, flow_actions stmt
+ let rationing_parameters, flow_actions = match stmt with
+ | None -> None, []
+ | Some stmt ->
+ let flow_actions = flow_actions stmt in
+ (* A skip statement is created on each split annotation: do not ration
+ states on them to avoid meddling in successive split directives. *)
+ if Cil.is_skip stmt.skind && flow_actions <> []
+ then None, flow_actions
+ else Some (slevel stmt, merge stmt), flow_actions
+ in
+ let rationing =
+ match rationing_parameters with
+ | None -> Partition.new_rationing ~limit:max_int ~merge:false
+ | Some (limit, merge) -> Partition.new_rationing ~limit ~merge
+ in
+ let flow_actions =
+ (Ration rationing) :: Update_dynamic_splits :: flow_actions
in
- let rationing = Partition.new_rationing ~limit ~merge in
{
- rationing; flow_actions;
+ flow_actions;
+ rationing = rationing_parameters <> None;
store_stmt = stmt;
store_index = Index.empty ();
store_partition = Partition.empty;
@@ -109,7 +123,7 @@ struct
Partition.iter (fun _key state -> Domain.pretty fmt state) s.store_partition
let pretty_flow (fmt : Format.formatter) (flow : flow) =
- Flow.iter (Domain.pretty fmt) flow
+ Flow.iter (fun _ -> Domain.pretty fmt) flow
(* Accessors *)
@@ -261,50 +275,49 @@ struct
let flow_states =
List.fold_left Flow.union Flow.empty sources_states
in
- (* Handle ration stamps *)
- dest.incoming_states <- dest.incoming_states + Flow.size flow_states;
- let rationing_action = Ration dest.rationing in
- (* Handle Split / Merge operations *)
- let flow_actions = Update_dynamic_splits :: dest.flow_actions in
(* Execute actions *)
- let actions = rationing_action :: flow_actions in
let flow_states =
- List.fold_left Flow.transfer_keys flow_states actions
+ List.fold_left Flow.transfer_keys flow_states dest.flow_actions
in
- (* Add states to the store but filter out already propagated states *)
- let update key current_state =
- (* Inclusion test *)
- let state =
- try
- let previous_state = Partition.find key dest.store_partition in
- if Domain.is_included current_state previous_state then
- (* The current state is included in the previous; stop *)
- None
- else begin
- (* Propagate the join of the two states *)
- if is_loop_head then
- Self.feedback ~level:1 ~once:true ~current:true
- "starting to merge loop iterations";
- Some (Domain.join previous_state current_state)
- end
- with
- (* There is no previous state, propagate normally *)
- Not_found -> Some current_state
- in
- (* Add the propagated state to the store *)
- let add s =
- dest.store_partition <- Partition.replace key s dest.store_partition;
- in
- Option.iter add state;
- (* Filter out already propagated states (only at statements). *)
- if dest.store_stmt = None
- then state
- else Extlib.opt_filter (fun s -> Index.add s dest.store_index) state
+ (* Add the propagated state to the store *)
+ let add_state key s =
+ dest.store_partition <- Partition.replace key s dest.store_partition;
in
- let flow = Flow.join_duplicate_keys flow_states in
- let flow = Flow.filter_map update flow in
- Option.iter (partitioning_feedback dest flow) dest.store_stmt;
- flow
+ if not (dest.rationing) then begin
+ Flow.iter add_state flow_states;
+ flow_states
+ end else begin
+ (* Handle ration stamps *)
+ dest.incoming_states <- dest.incoming_states + Flow.size flow_states;
+ (* Add states to the store but filter out already propagated states *)
+ let update key current_state =
+ (* Inclusion test *)
+ let state =
+ try
+ let previous_state = Partition.find key dest.store_partition in
+ if Domain.is_included current_state previous_state then
+ (* The current state is included in the previous; stop *)
+ None
+ else begin
+ (* Propagate the join of the two states *)
+ if is_loop_head then
+ Self.feedback ~level:1 ~once:true ~current:true
+ "starting to merge loop iterations";
+ Some (Domain.join previous_state current_state)
+ end
+ with
+ (* There is no previous state, propagate normally *)
+ Not_found -> Some current_state
+ in
+ Option.iter (add_state key) state;
+ (* Filter out already propagated states. *)
+ Extlib.opt_filter (fun s -> Index.add s dest.store_index) state
+ in
+ let flow = Flow.join_duplicate_keys flow_states in
+ let flow = Flow.filter_map update flow in
+ Option.iter (partitioning_feedback dest flow) dest.store_stmt;
+ flow
+ end
let widen (w : widening) (flow : flow) : flow =
let stmt = w.widening_stmt in
diff --git a/src/plugins/eva/utils/eva_annotations.ml b/src/plugins/eva/utils/eva_annotations.ml
index dc8a7b04de93c3339b11c2a6491735cc636c6c9f..8a626416fecf5ab947f5dd52142218fb32d3b535 100644
--- a/src/plugins/eva/utils/eva_annotations.ml
+++ b/src/plugins/eva/utils/eva_annotations.ml
@@ -62,12 +62,18 @@ type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
exception Parse_error
+(* Where an Eva directive is applied. *)
+type kind =
+ | Here (* The directive is applied when encountered. *)
+ | Stmt (* The directive has effect on the next statement. *)
+ | Loop (* The directive concerns a loop. *)
+
module type Annotation =
sig
type t
val name : string
- val is_loop_annot : bool
+ val kind : kind
val parse : typing_context:Logic_typing.typing_context -> lexpr list -> t
val export : t -> acsl_extension_kind
val import : acsl_extension_kind -> t
@@ -87,16 +93,19 @@ struct
print fmt (import lp)
let () =
- if is_loop_annot then
- Acsl_extension.register_code_annot_next_loop name typer ~printer false
- else
- Acsl_extension.register_code_annot_next_stmt name typer ~printer false
+ let register =
+ match kind with
+ | Here -> Acsl_extension.register_code_annot
+ | Stmt -> Acsl_extension.register_code_annot_next_stmt
+ | Loop -> Acsl_extension.register_code_annot_next_loop
+ in
+ register name typer ~printer false
let get stmt =
let filter_add _emitter annot acc =
match annot.annot_content with
- | Cil_types.AExtended (_, is_loop_annot', {ext_name=name'; ext_kind})
- when name' = name && is_loop_annot' = is_loop_annot ->
+ | Cil_types.AExtended (_, is_loop_annot, {ext_name=name'; ext_kind})
+ when name' = name && is_loop_annot = (kind = Loop) ->
import ext_kind :: acc
| _ -> acc
in
@@ -106,7 +115,7 @@ struct
let loc = Cil_datatype.Stmt.loc stmt in
let param = M.export annot in
let extension = Logic_const.new_acsl_extension name loc false param in
- let annot_node = Cil_types.AExtended ([], is_loop_annot, extension) in
+ let annot_node = Cil_types.AExtended ([], kind = Loop, extension) in
let code_annotation = Logic_const.new_code_annotation annot_node in
Annotations.add_code_annot emitter stmt code_annotation
end
@@ -116,7 +125,7 @@ module Slevel = Register (struct
type t = slevel_annotation
let name = "slevel"
- let is_loop_annot = false
+ let kind = Here
let parse ~typing_context:_ = function
| [{lexpr_node = PLvar "default"}] -> SlevelDefault
@@ -161,7 +170,7 @@ module Unroll = Register (struct
type t = unroll_annotation
let name = "unroll"
- let is_loop_annot = true
+ let kind = Loop
let parse ~typing_context = function
| [] -> UnrollFull
@@ -191,6 +200,8 @@ struct
when possible, to avoid changes due to its reconversion to a C term. *)
type t = split_term * Cil_types.term option
+ let kind = Here
+
let term_to_exp = Logic_to_c.term_to_exp ?result:None
let parse ~typing_context:context = function
@@ -231,19 +242,16 @@ end
module Split = Register (struct
include SplitTermAnnotation
let name = "split"
- let is_loop_annot = false
end)
module Merge = Register (struct
include SplitTermAnnotation
let name = "merge"
- let is_loop_annot = false
end)
module DynamicSplit = Register (struct
include SplitTermAnnotation
let name = "dynamic_split"
- let is_loop_annot = false
end)
let get_slevel_annot stmt =
@@ -275,7 +283,7 @@ let add_flow_annot ~emitter stmt flow_annotation =
module Subdivision = Register (struct
type t = int
let name = "subdivide"
- let is_loop_annot = false
+ let kind = Stmt
let parse ~typing_context:_ = function
| [{lexpr_node = PLconstant (IntConstant i)}] ->
@@ -316,7 +324,7 @@ module Allocation = struct
include Register (struct
type t = allocation_kind
let name = "eva_allocate"
- let is_loop_annot = false
+ let kind = Stmt
let parse ~typing_context:_ = function
| [{lexpr_node = PLvar s}] -> Extlib.the ~exn:Parse_error (of_string s)
@@ -356,7 +364,7 @@ let get_allocation = Allocation.get
module ArraySegmentation = Register (struct
type t = Cil_types.varinfo * Cil_types.offset * Cil_types.exp list
let name = "array_partition"
- let is_loop_annot = false
+ let kind = Here
let convert = function
| {term_node = TLval (TVar {lv_origin=Some vi}, toffset)} :: tbounds ->
@@ -402,7 +410,7 @@ let read_array_segmentation ext = ArraySegmentation.import ext.ext_kind
module DomainScope = Register (struct
type t = string * Cil_types.varinfo list
let name = "eva_domain_scope"
- let is_loop_annot = false
+ let kind = Here
let parse ~typing_context:context =
let parse_domain = function
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
diff --git a/tests/value/oracle/local_slevel.res.oracle b/tests/value/oracle/local_slevel.res.oracle
index ed3e146882954d10d8006e8bff555354f887b127..8dfd964a3ce6047ef3a8f0a901faa3d9209f784f 100644
--- a/tests/value/oracle/local_slevel.res.oracle
+++ b/tests/value/oracle/local_slevel.res.oracle
@@ -78,7 +78,7 @@
[eva] local_slevel.i:37: Frama_C_show_each: {47}
[eva] local_slevel.i:37: Frama_C_show_each: {48}
[eva] local_slevel.i:37: Frama_C_show_each: {49}
-[eva] local_slevel.i:43: Trace partitioning superposing up to 100 states
+[eva] local_slevel.i:42: Trace partitioning superposing up to 100 states
[eva] local_slevel.i:37: Frama_C_show_each: {50}
[eva] local_slevel.i:37: Frama_C_show_each: {51}
[eva] local_slevel.i:37: Frama_C_show_each: {52}
@@ -129,7 +129,7 @@
[eva] local_slevel.i:37: Frama_C_show_each: {97}
[eva] local_slevel.i:37: Frama_C_show_each: {98}
[eva] local_slevel.i:37: Frama_C_show_each: {99}
-[eva] local_slevel.i:43: Trace partitioning superposing up to 200 states
+[eva] local_slevel.i:42: Trace partitioning superposing up to 200 states
[eva] Recording results for main2
[eva] Done for function main2
[eva] Recording results for main
@@ -185,7 +185,7 @@ void main1(void)
while (i < 80) {
/*@ ensures \true;
assigns v; */
- /*@ slevel 50; */
+ /*@ slevel 50; */ ;
if (i % 2) v = 1; else v = -1;
Frama_C_show_each(v,i,r);
v *= v;
@@ -251,7 +251,7 @@ void main1(void)
while (i < 80) {
/*@ ensures \true;
assigns v; */
- /*@ slevel 50; */
+ /*@ slevel 50; */ ;
if (i % 2) v = 1; else v = -1;
Frama_C_show_each(v,i,r);
v *= v;
@@ -317,7 +317,7 @@ void main1(void)
while (i < 80) {
/*@ ensures \true;
assigns v; */
- /*@ slevel 50; */
+ /*@ slevel 50; */ ;
if (i % 2) v = 1; else v = -1;
Frama_C_show_each(v,i,r);
v *= v;
@@ -446,7 +446,7 @@ void main(void)
[eva] local_slevel.i:37: Frama_C_show_each: {47}
[eva] local_slevel.i:37: Frama_C_show_each: {48}
[eva] local_slevel.i:37: Frama_C_show_each: {49}
-[eva] local_slevel.i:43: Trace partitioning superposing up to 100 states
+[eva] local_slevel.i:42: Trace partitioning superposing up to 100 states
[eva] local_slevel.i:37: Frama_C_show_each: {50}
[eva] local_slevel.i:37: Frama_C_show_each: {51}
[eva] local_slevel.i:37: Frama_C_show_each: {52}
@@ -497,7 +497,7 @@ void main(void)
[eva] local_slevel.i:37: Frama_C_show_each: {97}
[eva] local_slevel.i:37: Frama_C_show_each: {98}
[eva] local_slevel.i:37: Frama_C_show_each: {99}
-[eva] local_slevel.i:43: Trace partitioning superposing up to 200 states
+[eva] local_slevel.i:42: Trace partitioning superposing up to 200 states
[eva] Recording results for main2
[eva] Done for function main2
[eva] Recording results for main
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index ef583a47f12fc77c9189539ef61777c459342e78..aa52873360db70044e939172e2cff1a5bba13fdb 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function test_slevel <- main.
- Called from partitioning-annots.c:223.
-[eva] partitioning-annots.c:188: starting to merge loop iterations
-[eva] partitioning-annots.c:193: starting to merge loop iterations
+ Called from partitioning-annots.c:278.
+[eva] partitioning-annots.c:243: starting to merge loop iterations
+[eva] partitioning-annots.c:248: starting to merge loop iterations
[eva] Recording results for test_slevel
[eva] Done for function test_slevel
[eva] computing for function test_unroll <- main.
- Called from partitioning-annots.c:224.
+ Called from partitioning-annots.c:279.
[eva:loop-unroll:partial] partitioning-annots.c:26: loop not completely unrolled
[eva] partitioning-annots.c:26: starting to merge loop iterations
[eva:loop-unroll:partial] partitioning-annots.c:34: loop not completely unrolled
@@ -25,7 +25,7 @@
[eva] Recording results for test_unroll
[eva] Done for function test_unroll
[eva] computing for function test_split <- main.
- Called from partitioning-annots.c:225.
+ Called from partitioning-annots.c:280.
[eva] computing for function Frama_C_interval <- test_split <- main.
Called from partitioning-annots.c:73.
[eva] using specification for function Frama_C_interval
@@ -65,7 +65,7 @@
[eva] Recording results for test_split
[eva] Done for function test_split
[eva] computing for function test_dynamic_split <- main.
- Called from partitioning-annots.c:226.
+ Called from partitioning-annots.c:281.
[eva] partitioning-annots.c:95: Warning:
this partitioning parameter cannot be evaluated safely on all states
[eva] computing for function Frama_C_interval <- test_dynamic_split <- main.
@@ -90,13 +90,44 @@
[eva] Recording results for test_dynamic_split
[eva] Done for function test_dynamic_split
[eva] computing for function test_dynamic_split_predicate <- main.
- Called from partitioning-annots.c:227.
+ Called from partitioning-annots.c:282.
[eva] partitioning-annots.c:124: starting to merge loop iterations
[eva] Recording results for test_dynamic_split_predicate
[eva] Done for function test_dynamic_split_predicate
+[eva] computing for function test_splits_post_call <- main.
+ Called from partitioning-annots.c:283.
+[eva] computing for function Frama_C_interval <- test_splits_post_call <- main.
+ Called from partitioning-annots.c:205.
+[eva] partitioning-annots.c:205:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function spec <- test_splits_post_call <- main.
+ Called from partitioning-annots.c:206.
+[eva] using specification for function spec
+[eva] Done for function spec
+[eva] partitioning-annots.c:211: Frama_C_show_each_spec: [-2147483648..-10], ⊥
+[eva] partitioning-annots.c:211: Frama_C_show_each_spec: [10..2147483647], ⊥
+[eva] partitioning-annots.c:211: Frama_C_show_each_spec: {-1}, [-1000..1000]
+[eva] computing for function body <- test_splits_post_call <- main.
+ Called from partitioning-annots.c:212.
+[eva] Recording results for body
+[eva] Done for function body
+[eva] partitioning-annots.c:212: Reusing old results for call to body
+[eva] partitioning-annots.c:212: Reusing old results for call to body
+[eva] partitioning-annots.c:217: Frama_C_show_each_body: [-510..-10], ⊥
+[eva] partitioning-annots.c:217: Frama_C_show_each_body: [10..510], ⊥
+[eva] partitioning-annots.c:217: Frama_C_show_each_body: {-1}, [-1000..1000]
+[eva] Recording results for test_splits_post_call
+[eva] Done for function test_splits_post_call
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function body:
+ i2 ∈ [-500..500]
+ absolute ∈ [0..500]
+ state ∈ {-1; 0; 1}
+ y ∈ [-1000..1000] or UNINITIALIZED
+ __retres ∈ [-510..510]
[eva:final-states] Values at end of function test_dynamic_split:
Frama_C_entropy_source ∈ [--..--]
a ∈ {0}
@@ -117,6 +148,13 @@
k ∈ {0; 1}
i ∈ {0; 1}
j ∈ {0; 1; 2}
+[eva:final-states] Values at end of function test_splits_post_call:
+ Frama_C_entropy_source ∈ [--..--]
+ x ∈ [-1000..1000] or UNINITIALIZED
+ y ∈ [-1000..1000] or UNINITIALIZED
+ error ∈ [-1000..1000] or UNINITIALIZED
+ i ∈ [-1000..1000]
+ r ∈ [-510..510]
[eva:final-states] Values at end of function test_unroll:
a[0..9] ∈ {42}
b[0..9] ∈ {42}
@@ -145,6 +183,8 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
k ∈ {0; 1}
+[from] Computing for function body
+[from] Done for function body
[from] Computing for function test_dynamic_split
[from] Computing for function Frama_C_interval <-test_dynamic_split
[from] Done for function Frama_C_interval
@@ -155,6 +195,10 @@
[from] Done for function test_slevel
[from] Computing for function test_split
[from] Done for function test_split
+[from] Computing for function test_splits_post_call
+[from] Computing for function spec <-test_splits_post_call
+[from] Done for function spec
+[from] Done for function test_splits_post_call
[from] Computing for function test_unroll
[from] Done for function test_unroll
[from] Computing for function main
@@ -164,6 +208,12 @@
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
+[from] Function body:
+ y FROM nondet; i; p (and SELF)
+ \result FROM nondet; i
+[from] Function spec:
+ x FROM i
+ \result FROM i
[from] Function test_dynamic_split:
Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
[from] Function test_dynamic_split_predicate:
@@ -173,12 +223,18 @@
[from] Function test_split:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
k FROM Frama_C_entropy_source
+[from] Function test_splits_post_call:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function test_unroll:
NO EFFECTS
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
k FROM Frama_C_entropy_source
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function body:
+ i2; absolute; tmp; state; y; __retres
+[inout] Inputs for function body:
+ nondet
[inout] Out (internal) for function test_dynamic_split:
Frama_C_entropy_source; a; b
[inout] Inputs for function test_dynamic_split:
@@ -195,6 +251,10 @@
Frama_C_entropy_source; k; i; j
[inout] Inputs for function test_split:
Frama_C_entropy_source; k
+[inout] Out (internal) for function test_splits_post_call:
+ Frama_C_entropy_source; x; y; error; i; r
+[inout] Inputs for function test_splits_post_call:
+ Frama_C_entropy_source; nondet
[inout] Out (internal) for function test_unroll:
a[0..9]; b[0..9]; c[0..19]; d[0..19]; e[0..9]; i; j; i_0; j_0; i_1;
i_2; i_3; j_1
diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle
index 3fe49f8ff9266240c18aac21e67f32978e3992ca..365ff709693100a98812f0b3ee71f2608624ab07 100644
--- a/tests/value/oracle/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle/partitioning-annots.3.res.oracle
@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function Frama_C_interval <- test_history.
- Called from partitioning-annots.c:167.
+ Called from partitioning-annots.c:222.
[eva] using specification for function Frama_C_interval
-[eva] partitioning-annots.c:167:
+[eva] partitioning-annots.c:222:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] partitioning-annots.c:173: Frama_C_show_each: {0; 1}, {0; 1}
-[eva:alarm] partitioning-annots.c:176: Warning:
+[eva] partitioning-annots.c:228: Frama_C_show_each: {0; 1}, {0; 1}
+[eva:alarm] partitioning-annots.c:231: Warning:
division by zero. assert j ≢ 0;
[eva] Recording results for test_history
[eva] done for function test_history
diff --git a/tests/value/oracle/partitioning-annots.4.res.oracle b/tests/value/oracle/partitioning-annots.4.res.oracle
index 793324f2603cfd3fb554a92a29803c88ae31e867..8ad2cdfc8afe43036525234351b1a5baebfff62c 100644
--- a/tests/value/oracle/partitioning-annots.4.res.oracle
+++ b/tests/value/oracle/partitioning-annots.4.res.oracle
@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function Frama_C_interval <- test_history.
- Called from partitioning-annots.c:167.
+ Called from partitioning-annots.c:222.
[eva] using specification for function Frama_C_interval
-[eva] partitioning-annots.c:167:
+[eva] partitioning-annots.c:222:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] partitioning-annots.c:173: Frama_C_show_each: {0}, {0}
-[eva] partitioning-annots.c:173: Frama_C_show_each: {1}, {1}
+[eva] partitioning-annots.c:228: Frama_C_show_each: {0}, {0}
+[eva] partitioning-annots.c:228: Frama_C_show_each: {1}, {1}
[eva] Recording results for test_history
[eva] done for function test_history
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle_apron/partitioning-annots.0.res.oracle b/tests/value/oracle_apron/partitioning-annots.0.res.oracle
index 94ed9ffca14931983ca8b0fcfd773dae01006fe7..68d268103b83832bb45759df2b7108b8ad474e1e 100644
--- a/tests/value/oracle_apron/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle_apron/partitioning-annots.0.res.oracle
@@ -1,4 +1,16 @@
-105,106c105,106
+115,116c115,122
+< [eva] partitioning-annots.c:212: Reusing old results for call to body
+< [eva] partitioning-annots.c:212: Reusing old results for call to body
+---
+> [eva] computing for function body <- test_splits_post_call <- main.
+> Called from partitioning-annots.c:212.
+> [eva] Recording results for body
+> [eva] Done for function body
+> [eva] computing for function body <- test_splits_post_call <- main.
+> Called from partitioning-annots.c:212.
+> [eva] Recording results for body
+> [eva] Done for function body
+136,137c142,143
< x ∈ [0..44]
< y ∈ [0..44]
---
diff --git a/tests/value/oracle_apron/partitioning-annots.3.res.oracle b/tests/value/oracle_apron/partitioning-annots.3.res.oracle
index d04cebfc945498812ebf2de1f658c5458442d6d8..5a8823d8cc9e5c5d07f57720b06f7c0917f9c17a 100644
--- a/tests/value/oracle_apron/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle_apron/partitioning-annots.3.res.oracle
@@ -1,3 +1,3 @@
15,16d14
-< [eva:alarm] partitioning-annots.c:176: Warning:
+< [eva:alarm] partitioning-annots.c:231: Warning:
< division by zero. assert j ≢ 0;
diff --git a/tests/value/oracle_octagon/partitioning-annots.0.res.oracle b/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
index cd64a1b908f4fcd56dac921a50c0bec490216e7e..141d3a1f322385d29fea8cd73951c79d349d8440 100644
--- a/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
@@ -1,4 +1,4 @@
-105,106c105,106
+136,137c136,137
< x ∈ [0..44]
< y ∈ [0..44]
---
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index d3ab58aaa5069ea02e5298ffff4abd6874bae81b..393b1fe4bbd3e01a353013158fd7fa781ec5b43c 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -162,6 +162,61 @@ void test_loop_split()
}
}
+/*@
+ assigns \result, *p \from i;
+ behavior error:
+ assumes nondet == 0;
+ assigns \result, *p \from i;
+ ensures \result == -1;
+ ensures \initialized(p) && *p == \old(i);
+ behavior positive:
+ assumes nondet > 0;
+ assigns \result \from i;
+ ensures \result >= 10;
+ behavior negative:
+ assumes nondet < 0;
+ assigns \result \from i;
+ ensures \result <= -10;
+ disjoint behaviors;
+ complete behaviors;
+*/
+int spec(int i, int* p);
+
+int body(int i, int *p) {
+ int i2 = i / 2;
+ int absolute = i2 < 0 ? -i2 : i2;
+ int state = nondet % 2;
+ //@ split state;
+ if (state < 0)
+ return - 10 - absolute;
+ if (state > 0)
+ return 10 + absolute;
+ *p = i;
+ return -1;
+}
+
+/* Tests the application of multiple splits according to the return value of a
+ call, to keep in the caller some state partitioning from the callee.
+ The splits must be defined after the call, so the state partitioning from the
+ callee must be kept until all splits are performed.
+ Tests this whether the function body or a specification is used. */
+void test_splits_post_call (void) {
+ int x, y, error;
+ int i = Frama_C_interval(-1000, 1000);
+ int r = spec(i, &x);
+ //@ split r < -1;
+ //@ split r > -1;
+ if (r == -1)
+ error = x; // There should be no alarm.
+ Frama_C_show_each_spec(r, x); // There should be three states.
+ r = body(i, &y);
+ //@ split r < -1;
+ //@ split r > -1;
+ if (r == -1)
+ error = y; // There should be no alarm.
+ Frama_C_show_each_body(r, y); // There should be three states.
+}
+
void test_history()
{
int i = Frama_C_interval(0,1);
@@ -225,4 +280,5 @@ void main(void)
test_split();
test_dynamic_split();
test_dynamic_split_predicate();
+ test_splits_post_call();
}