From a39cccbd17688721f190f525bb017bf611d998a8 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 14 Nov 2022 15:27:52 +0100
Subject: [PATCH] [aorai] update oracles
---
.../ya/oracle/aorai_ptr_field.res.oracle | 12 +
.../tests/ya/oracle/assigns.0.res.oracle | 84 ++++++
.../tests/ya/oracle/assigns.1.res.oracle | 24 ++
.../tests/ya/oracle/bts1289.0.res.oracle | 20 ++
.../tests/ya/oracle/bts1289.1.res.oracle | 84 ++++++
.../ya/oracle/declared_function.res.oracle | 12 +
.../tests/ya/oracle/deterministic.res.oracle | 48 ++++
.../aorai/tests/ya/oracle/formals.res.oracle | 49 +++-
.../tests/ya/oracle/function_ptr.res.oracle | 36 +++
.../generate_assigns_bts1290.res.oracle | 10 +
.../tests/ya/oracle/hoare_seq.res.oracle | 180 ++++++++++++
.../tests/ya/oracle/incorrect.res.oracle | 12 +
.../ya/oracle/logical_operators.res.oracle | 20 ++
.../tests/ya/oracle/loop_bts1050.res.oracle | 270 ++++++++++++++++++
.../ya/oracle/metavariables-right.res.oracle | 60 ++++
.../tests/ya/oracle/monostate.res.oracle | 24 ++
.../aorai/tests/ya/oracle/not_prm.res.oracle | 12 +
.../aorai/tests/ya/oracle/observed.res.oracle | 84 ++++++
.../aorai/tests/ya/oracle/other.res.oracle | 60 ++++
.../aorai/tests/ya/oracle/seq.res.oracle | 270 ++++++++++++++++++
.../aorai/tests/ya/oracle/seq_loop.res.oracle | 270 ++++++++++++++++++
.../tests/ya/oracle/seq_unlimited.res.oracle | 36 +++
.../tests/ya/oracle/single_call.res.oracle | 30 ++
.../oracle/singleassignment-right.res.oracle | 12 +
.../aorai/tests/ya/oracle/stack.res.oracle | 36 +++
.../ya/oracle/test_acces_params.res.oracle | 144 ++++++++++
.../ya/oracle/test_acces_params2.res.oracle | 216 ++++++++++++++
.../test_boucle_rechercheTableau.res.oracle | 60 ++++
.../tests/ya/oracle/test_factorial.res.oracle | 48 ++++
.../ya/oracle/test_recursion4.res.oracle | 60 ++++
.../ya/oracle/test_recursion5.res.oracle | 144 ++++++++++
.../tests/ya/oracle/test_struct.res.oracle | 32 +++
.../oracle_prove/declared_function.res.oracle | 2 +-
.../ya/oracle_prove/incorrect.res.oracle | 2 +-
.../tests/ya/oracle_prove/serial.res.oracle | 2 +-
35 files changed, 2459 insertions(+), 6 deletions(-)
diff --git a/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle b/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle
index 2a20447f879..e8f31d7d12c 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
@@ -21,6 +21,12 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, S1, s->x, s;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, S1, s->x, s;
+ assigns S0 \from aorai_CurOpStatus, aorai_CurOperation, S0, S1, s->x, s;
+ assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S0, S1, s->x, s;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -64,6 +70,12 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+ assigns S0 \from aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+ assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S0, S1;
behavior buch_state_S0_out:
ensures 0 ≡ 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 e65c2a8ed2e..6f35fd44384 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
@@ -24,6 +24,27 @@ int X;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S_in_f
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns in_main
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -82,6 +103,27 @@ int X;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S_in_f
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns in_main
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -155,6 +197,27 @@ void f(void)
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S_in_f
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns in_main
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -213,6 +276,27 @@ void f(void)
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns S_in_f
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
+ assigns in_main
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
behavior buch_state_S1_out:
ensures 0 ≡ 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 e01339d6178..27d4f623014 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -38,6 +38,12 @@ int X;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_S1_out:
ensures aorai_CurStates ≢ S1;
@@ -79,6 +85,12 @@ int X;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_S1_out:
ensures aorai_CurStates ≢ S1;
@@ -133,6 +145,12 @@ void f(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_S1_out:
ensures aorai_CurStates ≢ S1;
@@ -174,6 +192,12 @@ void f(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_S1_out:
ensures aorai_CurStates ≢ S1;
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 8241b35201e..b0cac6b01b2 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
@@ -18,6 +18,11 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_a;
assigns aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
behavior buch_state_S_out:
ensures 0 ≡ S;
@@ -41,6 +46,11 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_a;
assigns aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
behavior buch_state_S_out:
ensures 0 ≡ S;
@@ -75,6 +85,11 @@ void a(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
behavior buch_state_S_out:
ensures 0 ≡ S;
@@ -98,6 +113,11 @@ void a(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
behavior buch_state_S_out:
ensures 0 ≡ 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 ad209874b35..a721d8db112 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -24,6 +24,27 @@ enum aorai_OpStatusList {
ensures aorai_CurOperation ≡ op_a;
assigns aorai_CurOpStatus, aorai_CurOperation, S, T,
aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns S
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns T
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
behavior buch_state_S_out:
ensures 0 ≡ S;
@@ -90,6 +111,27 @@ enum aorai_OpStatusList {
ensures aorai_CurOperation ≡ op_a;
assigns aorai_CurOpStatus, aorai_CurOperation, S, T,
aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns S
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns T
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
behavior buch_state_S_in:
assumes 1 ≡ aorai_intermediate_state_0;
@@ -192,6 +234,27 @@ void a(void)
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S, T,
aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns S
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns T
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
behavior buch_state_S_in:
assumes 1 ≡ init;
@@ -251,6 +314,27 @@ void a(void)
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S, T,
aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns S
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns T
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+ aorai_intermediate_state, aorai_intermediate_state_0, init;
behavior buch_state_S_in:
assumes 1 ≡ 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 f2bea78fd12..8f274a98c57 100644
--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -51,6 +51,12 @@ check lemma I_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_I_in:
assumes aorai_CurStates ≡ I;
@@ -80,6 +86,12 @@ check lemma I_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_I_in:
assumes 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 84e8253a128..8ad803dbd22 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -69,6 +69,12 @@ check lemma S0_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
behavior buch_state_S0_out:
ensures aorai_CurStates ≢ S0;
@@ -132,6 +138,12 @@ check lemma S0_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_S0_out:
ensures aorai_CurStates ≢ S0;
@@ -209,6 +221,12 @@ void g(int x)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
behavior buch_state_S0_out:
ensures aorai_CurStates ≢ S0;
@@ -261,6 +279,12 @@ void g(int x)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, res, X;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, res, X;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, res, X;
behavior buch_state_S0_out:
ensures aorai_CurStates ≢ S0;
@@ -336,6 +360,12 @@ int f(int x)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_real_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, c;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, c;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, c;
behavior buch_state_S0_out:
ensures aorai_CurStates ≢ S0;
@@ -399,6 +429,12 @@ int f(int x)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_real_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_S0_out:
ensures aorai_CurStates ≢ S0;
@@ -465,6 +501,12 @@ int real_main(int c)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_S0_in:
assumes aorai_CurStates ≡ Si;
@@ -515,6 +557,12 @@ int real_main(int c)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_S0_out:
ensures aorai_CurStates ≢ S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 614d489a97d..c37d669f422 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -52,7 +52,9 @@ check lemma aorai_intermediate_state_2_deterministic_trans{L}:
\at(aorai_x_0,L) ≡ 3 ∧
(¬(\at(aorai_CurOperation,L) ≡ op_f ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated) ∨
- \at(aorai_x_0,L) ≢ 3));
+ (\at(aorai_CurOperation,L) ≡ op_f ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
+ \at(aorai_x_0,L) ≢ 3)));
*/
/*@ ghost int aorai_y = 0; */
/*@
@@ -62,7 +64,8 @@ check lemma aorai_intermediate_state_1_deterministic_trans{L}:
\at(aorai_y,L) ≡ 2 ∧
(¬(\at(aorai_CurOperation,L) ≡ op_g ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated) ∨
- \at(aorai_y,L) ≢ 2));
+ (\at(aorai_CurOperation,L) ≡ op_g ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ \at(aorai_y,L) ≢ 2)));
*/
/*@ ghost int aorai_x = 0; */
/*@
@@ -72,7 +75,8 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
\at(aorai_x,L) ≡ 1 ∧
(¬(\at(aorai_CurOperation,L) ≡ op_f ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated) ∨
- \at(aorai_x,L) ≢ 1));
+ (\at(aorai_CurOperation,L) ≡ op_f ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ \at(aorai_x,L) ≢ 1)));
*/
/*@ ghost
/@ requires aorai_CurStates ≡ main_0;
@@ -81,6 +85,12 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
ensures aorai_CurOperation ≡ op_f;
assigns aorai_x_0, aorai_x, aorai_CurOpStatus, aorai_CurOperation,
aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
behavior buch_state_OK_out:
ensures aorai_CurStates ≢ OK;
@@ -166,6 +176,15 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates,
+ aorai_x_0, aorai_x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates,
+ aorai_x_0, aorai_x;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates,
+ aorai_x_0, aorai_x;
behavior buch_state_OK_in:
assumes
@@ -321,6 +340,12 @@ int f(int x)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_y, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_OK_in:
assumes aorai_CurStates ≡ OK;
@@ -395,6 +420,12 @@ int f(int x)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_y;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_y;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_y;
behavior buch_state_OK_in:
assumes
@@ -505,6 +536,12 @@ int g(int y)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_OK_out:
ensures aorai_CurStates ≢ OK;
@@ -552,6 +589,12 @@ int g(int y)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_OK_in:
assumes 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 b6ef4dfe2f3..16e5de830ac 100644
--- a/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
@@ -71,6 +71,12 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_in:
assumes aorai_CurStates ≡ s1;
@@ -133,6 +139,12 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -213,6 +225,12 @@ void f(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -275,6 +293,12 @@ void f(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -355,6 +379,12 @@ void g(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -408,6 +438,12 @@ void g(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
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 1ac4f7dfe67..34366aa9fd4 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
@@ -16,6 +16,11 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
behavior buch_state_S_in:
assumes 1 ≡ S;
@@ -44,6 +49,11 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S;
+ assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
behavior buch_state_S_in:
assumes 1 ≡ 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 b89d3366d30..0c22ea3ad2c 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -29,6 +29,51 @@ enum aorai_OpStatusList {
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_reject;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_reject
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -112,6 +157,51 @@ enum aorai_OpStatusList {
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_reject;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
+ assigns aorai_reject
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -262,6 +352,51 @@ int main_bhv_bhv(int c); */
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_reject;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, c;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, c;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, c;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, c;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, c;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, c;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, c;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, c;
+ assigns aorai_reject
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, c;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -352,6 +487,51 @@ int main_bhv_bhv(int c); */
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_reject;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, res;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, res;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, res;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, res;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, res;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, res;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, res;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, res;
+ assigns aorai_reject
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_reject, res;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
index 8cf4803c645..e69f85f246c 100644
--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -28,6 +28,12 @@ int f(void);
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_reject_out:
ensures aorai_CurStates ≢ aorai_reject;
@@ -51,6 +57,12 @@ int f(void);
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_reject_out:
ensures 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 ab0d4e67329..4aa48e2ee5d 100644
--- a/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
@@ -18,6 +18,11 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, I;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, I, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, I, x;
+ assigns I \from aorai_CurOpStatus, aorai_CurOperation, I, x;
behavior buch_state_I_in:
assumes 1 ≡ I ∧ (x ≡ 1 ∨ x ≢ 1);
@@ -54,6 +59,11 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, I;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, I;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, I;
+ assigns I \from aorai_CurOpStatus, aorai_CurOperation, I;
behavior buch_state_I_in:
assumes 1 ≡ I;
@@ -96,6 +106,11 @@ void f(int x)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, I;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, I;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, I;
+ assigns I \from aorai_CurOpStatus, aorai_CurOperation, I;
behavior buch_state_I_in:
assumes 1 ≡ I;
@@ -124,6 +139,11 @@ void f(int x)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, I;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, I;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, I;
+ assigns I \from aorai_CurOpStatus, aorai_CurOperation, I;
behavior buch_state_I_in:
assumes 1 ≡ 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 82b0886cf1f..260cb460abb 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -34,6 +34,51 @@ enum aorai_OpStatusList {
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -132,6 +177,51 @@ enum aorai_OpStatusList {
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -243,6 +333,51 @@ void f(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -321,6 +456,51 @@ void f(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -418,6 +598,51 @@ void g(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -495,6 +720,51 @@ void g(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ 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 04818b8989e..c09d6701135 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -65,6 +65,12 @@ check lemma e_deterministic_trans{L}:
ensures aorai_CurOperation ≡ op_f;
assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation,
aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
@@ -132,6 +138,12 @@ check lemma e_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
@@ -203,6 +215,12 @@ void f(int x)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
@@ -256,6 +274,12 @@ void f(int x)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
@@ -322,6 +346,12 @@ void g(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_h;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_x;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_x;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
@@ -377,6 +407,12 @@ void g(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_h;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
@@ -443,6 +479,12 @@ void h(int x)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_i;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
@@ -497,6 +539,12 @@ void h(int x)
ensures aorai_CurOperation ≡ op_i;
assigns aorai_y, aorai_x, aorai_CurOpStatus, aorai_CurOperation,
aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
@@ -582,6 +630,12 @@ void i(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
@@ -635,6 +689,12 @@ void i(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index a9b448b9b7e..925e912d1ae 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -41,6 +41,12 @@ check lemma Init_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_Init_out:
ensures aorai_CurStates ≢ Init;
@@ -79,6 +85,12 @@ check lemma Init_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_Init_out:
ensures aorai_CurStates ≢ Init;
@@ -129,6 +141,12 @@ void f(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_Init_out:
ensures aorai_CurStates ≢ Init;
@@ -155,6 +173,12 @@ void f(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_Init_out:
ensures aorai_CurStates ≢ Init;
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 3dedd28abb5..3caffe84fad 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -18,6 +18,12 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf, x;
+ assigns S0 \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf, x;
+ assigns Sf \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf, x;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -55,6 +61,12 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
+ assigns S0 \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
+ assigns Sf \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index 85dd02e85b7..e2e3a4fe94e 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -24,6 +24,27 @@ enum aorai_OpStatusList {
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns final
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns first_step
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
behavior buch_state_aorai_intermediate_state_in:
assumes 1 ≡ init;
@@ -85,6 +106,27 @@ enum aorai_OpStatusList {
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns final
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns first_step
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
behavior buch_state_aorai_intermediate_state_out:
ensures 0 ≡ aorai_intermediate_state;
@@ -233,6 +275,27 @@ void g(void)
ensures aorai_CurOperation ≡ op_h;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns final
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns first_step
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
behavior buch_state_aorai_intermediate_state_out:
ensures 0 ≡ aorai_intermediate_state;
@@ -294,6 +357,27 @@ void g(void)
ensures aorai_CurOperation ≡ op_h;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns final
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns first_step
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+ aorai_intermediate_state_0, final, first_step, init;
behavior buch_state_aorai_intermediate_state_out:
ensures 0 ≡ 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 af246c4f01e..f83db815ae9 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -22,6 +22,16 @@ int x = 0;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns last
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns step1
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
behavior buch_state_init_in:
assumes (1 ≡ last ∧ x ≡ 4) ∨ (1 ≡ init ∧ x ≢ 3);
@@ -115,6 +125,16 @@ int x = 0;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns last
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns step1
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
behavior buch_state_init_in:
assumes (1 ≡ last ∧ x ≡ 4) ∨ (1 ≡ init ∧ x ≢ 3);
@@ -272,6 +292,16 @@ void f(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns last
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns step1
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
behavior buch_state_init_in:
assumes (1 ≡ last ∧ x ≡ 4) ∨ (1 ≡ init ∧ x ≢ 3);
@@ -365,6 +395,16 @@ void f(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns last
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns step1
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
behavior buch_state_init_in:
assumes (1 ≡ last ∧ x ≡ 4) ∨ (1 ≡ init ∧ x ≢ 3);
@@ -521,6 +561,16 @@ void g(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns last
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns step1
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
behavior buch_state_init_in:
assumes 1 ≡ init ∧ x ≢ 3;
@@ -573,6 +623,16 @@ void g(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns init
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns last
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+ assigns step1
+ \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
behavior buch_state_init_in:
assumes (1 ≡ last ∧ x ≡ 4) ∨ (1 ≡ init ∧ x ≢ 3);
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index 8e4a913ae4b..b2f0a865f3d 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -32,6 +32,51 @@ enum aorai_OpStatusList {
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -110,6 +155,51 @@ enum aorai_OpStatusList {
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -215,6 +305,51 @@ void f(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -322,6 +457,51 @@ void f(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -443,6 +623,51 @@ void g(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -522,6 +747,51 @@ void g(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ 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 1a827b61513..bae62a63168 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -34,6 +34,51 @@ enum aorai_OpStatusList {
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -132,6 +177,51 @@ enum aorai_OpStatusList {
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -243,6 +333,51 @@ void f(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -321,6 +456,51 @@ void f(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -418,6 +598,51 @@ void g(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -495,6 +720,51 @@ void g(void)
aorai_intermediate_state, aorai_intermediate_state_0,
aorai_intermediate_state_1, aorai_intermediate_state_2,
aorai_intermediate_state_3;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_1
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_2
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
+ assigns aorai_intermediate_state_3
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state, aorai_intermediate_state_0,
+ aorai_intermediate_state_1, aorai_intermediate_state_2,
+ aorai_intermediate_state_3, aorai_counter;
behavior buch_state_S0_out:
ensures 0 ≡ 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 34b512d7005..db603fa1ec6 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
@@ -54,6 +54,12 @@ check lemma aorai_intermediate_state_0_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_init;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_in:
assumes aorai_CurStates ≡ b;
@@ -101,6 +107,12 @@ check lemma aorai_intermediate_state_0_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_init;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -180,6 +192,12 @@ void init(int *a, int n)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_find;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -233,6 +251,12 @@ void init(int *a, int n)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_find;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -331,6 +355,12 @@ int find(int *a, int n, int k)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -378,6 +408,12 @@ int find(int *a, int n, int k)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_aorai_intermediate_state_out:
ensures aorai_CurStates ≢ aorai_intermediate_state;
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 d9c12479a3b..2b50360158f 100644
--- a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
@@ -19,6 +19,21 @@ enum aorai_OpStatusList {
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
aorai_intermediate_state;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state;
behavior buch_state_S0_out:
ensures 0 ≡ S0;
@@ -63,6 +78,21 @@ enum aorai_OpStatusList {
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
aorai_intermediate_state;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state;
+ assigns S0
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state;
+ assigns Sf
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state;
+ assigns aorai_intermediate_state
+ \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+ aorai_intermediate_state;
behavior buch_state_S0_out:
ensures 0 ≡ 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 380fab90eaa..d717c70ab7b 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
@@ -33,6 +33,12 @@ enum aorai_OpStatusList {
ensures aorai_CurOperation ≡ op_main;
assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation,
aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
@@ -83,6 +89,12 @@ enum aorai_OpStatusList {
ensures aorai_CurOperation ≡ op_main;
assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation,
aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index db9b5c07770..cb79a5bd6d3 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -59,6 +59,12 @@ check lemma emptying_stack_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_push;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
@@ -107,6 +113,12 @@ check lemma emptying_stack_deterministic_trans{L}:
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_push;
assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
@@ -187,6 +199,12 @@ void push(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_pop;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
@@ -235,6 +253,12 @@ void push(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_pop;
assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
@@ -333,6 +357,12 @@ void pop(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
@@ -385,6 +415,12 @@ void pop(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ assigns aorai_CurStates
+ \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_in:
assumes aorai_CurStates ≡ empty_stack;
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 6099fd70578..c2fc72913e5 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
@@ -31,6 +31,30 @@ int rr = 1;
ensures aorai_CurOperation ≡ op_opa;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
mainst;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, i;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, i;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, i;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, i;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, i;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, i;
+ assigns SF
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, i;
+ assigns mainst
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, i;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -99,6 +123,30 @@ int rr = 1;
ensures aorai_CurOperation ≡ op_opa;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
mainst;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns SF
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns mainst
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -187,6 +235,30 @@ void opa(int i, int j)
ensures aorai_CurOperation ≡ op_opb;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
mainst;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns SF
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns mainst
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -254,6 +326,30 @@ void opa(int i, int j)
ensures aorai_CurOperation ≡ op_opb;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
mainst;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, res;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, res;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, res;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, res;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, res;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, res;
+ assigns SF
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, res;
+ assigns mainst
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst, res;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -342,6 +438,30 @@ int opb(void)
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
mainst;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns SF
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns mainst
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
behavior buch_state_S1_in:
assumes 1 ≡ mainst;
@@ -408,6 +528,30 @@ int opb(void)
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
mainst;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns SF
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
+ assigns mainst
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+ mainst;
behavior buch_state_S1_out:
ensures 0 ≡ 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 b46e121b4fa..59019d29de5 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
@@ -32,6 +32,33 @@ int rr = 1;
ensures aorai_CurOperation ≡ op_opa;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
S7;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, r;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, r;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, r;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, r;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, r;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, r;
+ assigns S5
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, r;
+ assigns S6
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, r;
+ assigns S7
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, r;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -108,6 +135,33 @@ int rr = 1;
ensures aorai_CurOperation ≡ op_opa;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
S7;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, res;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, res;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, res;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, res;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, res;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, res;
+ assigns S5
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, res;
+ assigns S6
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, res;
+ assigns S7
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7, res;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -208,6 +262,33 @@ int opa(int r)
ensures aorai_CurOperation ≡ op_opb;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
S7;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S5
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S6
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S7
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -281,6 +362,33 @@ int opa(int r)
ensures aorai_CurOperation ≡ op_opb;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
S7;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S5
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S6
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S7
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -374,6 +482,33 @@ void opb(void)
ensures aorai_CurOperation ≡ op_opc;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
S7;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S5
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S6
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S7
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -440,6 +575,33 @@ void opb(void)
ensures aorai_CurOperation ≡ op_opc;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
S7;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S5
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S6
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S7
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -542,6 +704,33 @@ void opc(void)
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
S7;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S5
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S6
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S7
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -615,6 +804,33 @@ void opc(void)
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
S7;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S2
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S3
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S4
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S5
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S6
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
+ assigns S7
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+ S7;
behavior buch_state_S1_out:
ensures 0 ≡ 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 f767063f9aa..1431fa716c3 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
@@ -24,6 +24,16 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_isPresent;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
behavior buch_state_End_out:
ensures 0 ≡ End;
@@ -67,6 +77,16 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_isPresent;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
behavior buch_state_End_in:
assumes 1 ≡ Idle ∧ res ≢ -1;
@@ -174,6 +194,16 @@ int isPresent(int *t, int max, int val)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_foo;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
behavior buch_state_End_in:
assumes 1 ≡ WillDoFoo;
@@ -216,6 +246,16 @@ int isPresent(int *t, int max, int val)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_foo;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
behavior buch_state_End_in:
assumes 1 ≡ End;
@@ -271,6 +311,16 @@ void foo(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
behavior buch_state_End_out:
ensures 0 ≡ End;
@@ -313,6 +363,16 @@ void foo(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
behavior buch_state_End_in:
assumes 1 ≡ 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 20877ef3efb..56ba35bfc72 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -20,6 +20,14 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_decode_int;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns main_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
behavior buch_state_S1_in:
assumes 1 ≡ S1;
@@ -62,6 +70,14 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_decode_int;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns main_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
behavior buch_state_S1_in:
assumes 1 ≡ S1;
@@ -189,6 +205,14 @@ int decode_int(char *s)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_factorial;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns main_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
@@ -233,6 +257,14 @@ int decode_int(char *s)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_factorial;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns main_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
behavior buch_state_S1_in:
assumes 1 ≡ S2 ∨ 1 ≡ S1;
@@ -311,6 +343,14 @@ int factorial(int value)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns main_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
behavior buch_state_S1_in:
assumes 1 ≡ main_0;
@@ -353,6 +393,14 @@ int factorial(int value)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+ assigns main_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
behavior buch_state_S1_in:
assumes 1 ≡ 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 1bdb8e21ade..8c9faad2677 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -21,6 +21,16 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_isPresent;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
behavior buch_state_End_out:
ensures 0 ≡ End;
@@ -66,6 +76,16 @@ enum aorai_OpStatusList {
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_isPresent;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
behavior buch_state_End_in:
assumes (1 ≡ Idle ∧ res ≢ -1) ∨ (1 ≡ End ∧ res ≢ -1);
@@ -180,6 +200,16 @@ int isPresent(int *t, int size, int val)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_foo;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
behavior buch_state_End_in:
assumes 1 ≡ WillDoFoo;
@@ -222,6 +252,16 @@ int isPresent(int *t, int size, int val)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_foo;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
behavior buch_state_End_in:
assumes 1 ≡ End;
@@ -277,6 +317,16 @@ void foo(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
behavior buch_state_End_out:
ensures 0 ≡ End;
@@ -319,6 +369,16 @@ void foo(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
behavior buch_state_End_in:
assumes 1 ≡ 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 c6931e9735d..c7e017d08d5 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -28,6 +28,24 @@ enum aorai_OpStatusList {
ensures aorai_CurOperation ≡ op_isPresentRec;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns IgnoreFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
behavior buch_state_End_out:
ensures 0 ≡ End;
@@ -82,6 +100,24 @@ enum aorai_OpStatusList {
ensures aorai_CurOperation ≡ op_isPresentRec;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
+ assigns IgnoreFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
behavior buch_state_End_out:
ensures 0 ≡ End;
@@ -206,6 +242,24 @@ int isPresentRec(int *t, int i, int max, int val)
ensures aorai_CurOperation ≡ op_isPresent;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns IgnoreFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
behavior buch_state_End_out:
ensures 0 ≡ End;
@@ -259,6 +313,24 @@ int isPresentRec(int *t, int i, int max, int val)
ensures aorai_CurOperation ≡ op_isPresent;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
+ assigns IgnoreFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo, res;
behavior buch_state_End_in:
assumes 1 ≡ IgnoreFoo ∧ res ≢ -1;
@@ -348,6 +420,24 @@ int isPresent(int *t, int max, int val)
ensures aorai_CurOperation ≡ op_foo;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns IgnoreFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
behavior buch_state_End_in:
assumes 1 ≡ WillDoFoo;
@@ -399,6 +489,24 @@ int isPresent(int *t, int max, int val)
ensures aorai_CurOperation ≡ op_foo;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns IgnoreFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
behavior buch_state_End_in:
assumes 1 ≡ End;
@@ -464,6 +572,24 @@ void foo(void)
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns IgnoreFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
behavior buch_state_End_out:
ensures 0 ≡ End;
@@ -515,6 +641,24 @@ void foo(void)
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
WillDoFoo;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns End
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns Idle
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns IgnoreFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
+ assigns WillDoFoo
+ \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+ WillDoFoo;
behavior buch_state_End_in:
assumes 1 ≡ 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 dd49304a158..541b2c925a3 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -25,6 +25,14 @@ int myAge = 0;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_increment;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, main_0;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns main_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
behavior buch_state_S1_in:
assumes 1 ≡ S1 ∧ nobody.Age ≡ 1;
@@ -63,6 +71,14 @@ int myAge = 0;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_increment;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, main_0;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns main_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
behavior buch_state_S1_in:
assumes 1 ≡ S1 ∧ nobody.Age ≡ 1;
@@ -118,6 +134,14 @@ void increment(void)
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, main_0;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns main_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
behavior buch_state_S1_in:
assumes 1 ≡ main_0 ∧ nobody.Age ≡ 0;
@@ -156,6 +180,14 @@ void increment(void)
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, main_0;
+ assigns aorai_CurOpStatus
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns aorai_CurOperation
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns S1
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+ assigns main_0
+ \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
behavior buch_state_S1_in:
assumes 1 ≡ S1 ∧ nobody.Age ≡ 1;
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
index 3a6d4d2a8b0..c2f8fbb2a85 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing declared_function.i (no preprocessing)
[kernel] Parsing TMPDIR/aorai_declared_function_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0_prove.i:105: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0_prove.i:112: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
index 9978b066020..58a818caca4 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
@@ -2,5 +2,5 @@
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_incorrect_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0_prove.i:70: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0_prove.i:77: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
index 80915856615..60bf5507e20 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing serial.c (with preprocessing)
[kernel] Parsing TMPDIR/aorai_serial_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0_prove.i:1273: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0_prove.i:1291: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
--
GitLab