diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index dd533767fdd535a18e210bab631c394adf7946af..7f82b59785afe69677c1c8ab78cbf79ac6056e26 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1982,8 +1982,45 @@ let mk_transitions_stmt generated_kf loc f st res trans =
trans
([],[],Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc, [])
+let mk_goto loc b =
+ let ghost = true in
+ match b.bstmts with
+ | [] -> Cil.mkBlock []
+ | [ { skind = Instr i } ] ->
+ let s = mkStmtOneInstr ~ghost i in
+ Cil.mkBlock [s]
+ | [ { skind = Goto (s,_) }] ->
+ let s' = mkStmt ~ghost (Goto (ref !s,loc)) in
+ Cil.mkBlock [s']
+ | s::_ ->
+ s.labels <-
+ (Label(Data_for_aorai.get_fresh "__aorai_label",loc,false)):: s.labels;
+ let s' = mkStmt ~ghost (Goto (ref s,loc)) in
+ Cil.mkBlock [s']
+
+let normalize_condition loc cond block1 block2 =
+ let rec aux cond b1 b2 =
+ match cond.enode with
+ | UnOp(LNot,e,_) -> aux e b2 b1
+ | BinOp(LAnd,e1,e2,_) ->
+ let b2' = mk_goto loc b2 in
+ let b1'= Cil.mkBlock [aux e2 b1 b2'] in
+ aux e1 b1' b2
+ | BinOp(LOr,e1,e2,_) ->
+ let b1' = mk_goto loc b1 in
+ let b2' = Cil.mkBlock [aux e2 b1' b2] in
+ aux e1 b1 b2'
+ | _ ->
+ Cil.mkStmt ~ghost:true (If(cond,b1,b2,loc))
+ in
+ aux cond block1 block2
+
let mkIfStmt loc exp1 block1 block2 =
- Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
+ if Kernel.LogicalOperators.get() then
+ Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
+ else
+ normalize_condition loc exp1 block1 block2
+
let mk_deterministic_stmt
generated_kf loc auto f fst status ret state
diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index 2e55921a891feb5ab63598f1d24a2778f5210587..5a1e9fb9bc0c7402697be6f1d92c3e6ad0155ca9 100644
--- a/src/plugins/aorai/tests/Aorai_test.ml
+++ b/src/plugins/aorai/tests/Aorai_test.ml
@@ -111,6 +111,8 @@ let extend () =
if ProveAuxSpec.get () then begin
if InternalWpShare.is_set() then
Wp.Wp_parameters.Share.set (InternalWpShare.get());
+ Wp.Wp_parameters.Split.on();
+ Wp.Wp_parameters.SplitMax.set 32;
Wp.Wp_parameters.Verbose.set 0;
Globals.Functions.iter check_auto_func;
end else begin
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
index 04174d4018a865d5e854376f9bd0a5aca035c5fe..c73da4393f558e64393afa9a6454a8f4abfb7f73 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
@@ -52,8 +52,9 @@ extern int call_to_an_undefined_function(void);
T0_S2_tmp = T0_S2;
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
- if (T0_S2 == 1 || accept_S1 == 1) accept_S1_tmp = 1;
- else accept_S1_tmp = 0;
+ if (T0_S2 == 1) accept_S1_tmp = 1;
+ else
+ if (accept_S1 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
T0_init_tmp = 0;
T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
@@ -160,7 +161,9 @@ int a(void)
accept_S1_tmp = accept_S1;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1 || accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1) T0_S2_tmp = 1;
+ else
+ if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
index aed1c6cbbf0e5f8c0333d3b2038f72c2d1e6412f..380098d2be6df47bfad67f24d8de850dee8dfae4 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
@@ -274,10 +274,12 @@ int commit_trans(void)
accept_S4_tmp = accept_S4;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
- if (accept_S2 == 1 && status != 0) accept_S4_tmp = 1;
+ if (accept_S2 == 1)
+ if (status != 0) accept_S4_tmp = 1; else accept_S4_tmp = 0;
else accept_S4_tmp = 0;
accept_S3_tmp = 0;
- if (accept_S2 == 1 && status == 0) accept_S2_tmp = 1;
+ if (accept_S2 == 1)
+ if (status == 0) accept_S2_tmp = 1; else accept_S2_tmp = 0;
else accept_S2_tmp = 0;
accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
index 9ab4d87d9cc4fec37cb7161c6985fbba348376e2..53bd6b3751c7e1c995c8b53d2f12fa3a9776191e 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
@@ -145,7 +145,9 @@ int rr = 1;
accept_all_tmp = 0;
accept_S5_tmp = 0;
accept_S4_tmp = 0;
- if (T0_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
+ if (T0_S2 == 1)
+ if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
+ else accept_S3_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
index 8b2d1dbb5f25e9a5e7ce4f93d939320ceff7e03c..3a2a6c4f72338186ea42486373370530ef384072 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
@@ -238,7 +238,9 @@ void opa(void)
accept_S3_tmp = accept_S3;
accept_all_tmp = accept_all;
accept_all_tmp = 0;
- if (T1_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
+ if (T1_S2 == 1)
+ if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
+ else accept_S3_tmp = 0;
T1_S2_tmp = 0;
T0_init_tmp = 0;
T0_S4_tmp = 0;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
index 4a0a9031b26157edb32bc4646da67494a4734c6d..12e9c8f60dc291511217340bc30fafb366f2f3fb 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
@@ -219,8 +219,9 @@ int decode_int(char *s)
accept_S2_tmp = accept_S2;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
- if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
- else accept_S2_tmp = 0;
+ if (accept_S1 == 1) accept_S2_tmp = 1;
+ else
+ if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
accept_S2 = accept_S2_tmp;
@@ -268,10 +269,12 @@ int decode_int(char *s)
accept_S2_tmp = accept_S2;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
- if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
- else accept_S2_tmp = 0;
- if (accept_S1 == 1 || accept_S2 == 1) accept_S1_tmp = 1;
- else accept_S1_tmp = 0;
+ if (accept_S1 == 1) accept_S2_tmp = 1;
+ else
+ if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+ if (accept_S1 == 1) accept_S1_tmp = 1;
+ else
+ if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
accept_S2 = accept_S2_tmp;
accept_init = accept_init_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
index 6dda5c9d85b5c4ff6209a1347863c8efd0b1838b..472c3f9634c29c43ec8273961105b4c878899557 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
@@ -106,7 +106,11 @@ int global_argc = 0;
accept_T2_tmp = 0;
T1_tmp = 0;
T0_init_tmp = 0;
- if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
+ if (S1 == 1) S1_tmp = 1;
+ else
+ if (T1 == 1)
+ if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
+ else S1_tmp = 0;
S1 = S1_tmp;
T0_init = T0_init_tmp;
T1 = T1_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
index aabed966d5a0f114ae66bb87c5b263bab35d8e27..e2146d41412e9144e1265cbb91f6f41e68582095 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
@@ -106,7 +106,11 @@ int global_argc = 0;
accept_T2_tmp = 0;
T1_tmp = 0;
T0_init_tmp = 0;
- if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
+ if (S1 == 1) S1_tmp = 1;
+ else
+ if (T1 == 1)
+ if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
+ else S1_tmp = 0;
S1 = S1_tmp;
T0_init = T0_init_tmp;
T1 = T1_tmp;
@@ -420,7 +424,9 @@ int sumOne(char *t, int length)
T0_init_tmp = T0_init;
T1_tmp = T1;
accept_T2_tmp = accept_T2;
- if (T1 == 1 && res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
+ if (T1 == 1)
+ if (res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
+ else accept_T2_tmp = 0;
if (T1 == 1) T1_tmp = 1; else T1_tmp = 0;
T0_init_tmp = 0;
S1_tmp = 0;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
index 3b0822025db85b3f78f088c4147467d42c4385fc..5d44a348df90c22551cf1d62388fede7e482438b 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
@@ -58,7 +58,9 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1) T0_S2_tmp = 1;
+ else
+ if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
@@ -250,10 +252,14 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
- if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
- else accept_S2_tmp = 0;
- if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
- else accept_S1_tmp = 0;
+ if (T0_S2 == 1) accept_S2_tmp = 1;
+ else
+ if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+ if (T0_S2 == 1) accept_S1_tmp = 1;
+ else
+ if (accept_S1 == 1) accept_S1_tmp = 1;
+ else
+ if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
index 74f48874eb313e191b4918e670f2126e8843de58..64fcb6cad31a3fd1d0edcfd1e41dc6472e8e270e 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
@@ -58,7 +58,9 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1) T0_S2_tmp = 1;
+ else
+ if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
@@ -248,10 +250,14 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
- if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
- else accept_S2_tmp = 0;
- if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
- else accept_S1_tmp = 0;
+ if (T0_S2 == 1) accept_S2_tmp = 1;
+ else
+ if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+ if (T0_S2 == 1) accept_S1_tmp = 1;
+ else
+ if (accept_S1 == 1) accept_S1_tmp = 1;
+ else
+ if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
index e4f973d66d554a0ac72c98aca30e5600442a4cc3..e3db4bca9bbca6c70ccb238ce9743beef46f94f4 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
@@ -58,7 +58,9 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1) T0_S2_tmp = 1;
+ else
+ if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
@@ -255,10 +257,14 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
- if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
- else accept_S2_tmp = 0;
- if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
- else accept_S1_tmp = 0;
+ if (T0_S2 == 1) accept_S2_tmp = 1;
+ else
+ if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+ if (T0_S2 == 1) accept_S1_tmp = 1;
+ else
+ if (accept_S1 == 1) accept_S1_tmp = 1;
+ else
+ if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
index e3d5ec00773c630fcd03a506eaec86aa0b0777ee..db979fdb7c87c7b1d15c858c8fe51e570b729a72 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
@@ -3,5 +3,5 @@
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
[kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:86: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:87: Warning:
Neither code nor specification for function call_to_an_undefined_function, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/logical_operators.i b/src/plugins/aorai/tests/ya/logical_operators.i
new file mode 100644
index 0000000000000000000000000000000000000000..1dcbba59346f608a433691d0d549058a6d6a22f8
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/logical_operators.i
@@ -0,0 +1,9 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+void f(int x) {}
+
+void main(int x) {
+ f(x);
+}
diff --git a/src/plugins/aorai/tests/ya/logical_operators.ya b/src/plugins/aorai/tests/ya/logical_operators.ya
new file mode 100644
index 0000000000000000000000000000000000000000..5baf089d910caa355d0abaecda90f3ea3fd1410e
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/logical_operators.ya
@@ -0,0 +1,3 @@
+%init : I;
+
+I: { f().x == 1 } -> I | other -> I;
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 d8cb4fbaee53d3fb52af093090ef0d12c43002b7..1c1744e5f85a9dd5177e9d97d6bab2884fdbce64 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
@@ -42,8 +42,15 @@ enum aorai_OpStatusList {
aorai_CurOperation = op_main;
S0_tmp = S0;
S1_tmp = S1;
- if (S0 == 1 && s->x >= 0 || S0 == 1 && s->x < 0) S1_tmp = 1;
- else S1_tmp = 0;
+ if (S0 == 1) {
+ if (s->x >= 0) S1_tmp = 1; else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (S0 == 1)
+ if (s->x < 0) S1_tmp = 1; else S1_tmp = 0;
+ else S1_tmp = 0;
+ }
S0_tmp = 0;
S0 = S0_tmp;
S1 = S1_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 7982cfe7c164fba8bf8e9d1f82290612f4c4ac4c..a48b55abef97f7cbdafffbffb7101d900aa056e5 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -112,10 +112,16 @@ check lemma S0_deterministic_trans{L}:
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
- if (3 == aorai_CurStates && x == 4) aorai_CurStates = S4;
- else
- if (3 == aorai_CurStates && x == 5) aorai_CurStates = S5;
+ if (3 == aorai_CurStates) {
+ if (x == 4) aorai_CurStates = S4; else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (3 == aorai_CurStates)
+ if (x == 5) aorai_CurStates = S5;
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
+ }
return;
}
@@ -241,7 +247,8 @@ void g(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- if (1 == aorai_CurStates && x == 4) aorai_CurStates = S3;
+ if (1 == aorai_CurStates)
+ if (x == 4) aorai_CurStates = S3; else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
return;
}
@@ -292,7 +299,11 @@ void g(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- if (1 == aorai_CurStates && (res == 0 && X == 5)) aorai_CurStates = S2;
+ if (1 == aorai_CurStates)
+ if (res == 0)
+ if (X == 5) aorai_CurStates = S2;
+ else aorai_CurStates = aorai_reject;
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
return;
}
@@ -368,10 +379,16 @@ int f(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_real_main;
- if (0 == aorai_CurStates && c != 0) aorai_CurStates = S1;
- else
- if (0 == aorai_CurStates && c == 0) aorai_CurStates = S2;
+ if (0 == aorai_CurStates) {
+ if (c != 0) aorai_CurStates = S1; else goto __aorai_label_0;
+ }
+ else {
+ __aorai_label_0: ;
+ if (0 == aorai_CurStates)
+ if (c == 0) aorai_CurStates = S2;
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
+ }
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 2d0f4d7bd8a2b0705c729447d09852dccb1f85e3..7e1393cfc29594234a1d203fb323b5cdd1906330 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -131,16 +131,23 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- if (7 == aorai_CurStates && x == 1) {
- aorai_CurStates = aorai_intermediate_state;
- aorai_x = x;
- }
- else
- if (7 == aorai_CurStates && x == 3) {
- aorai_CurStates = aorai_intermediate_state_2;
- aorai_x_0 = x;
+ if (7 == aorai_CurStates) {
+ if (x == 1) {
+ aorai_CurStates = aorai_intermediate_state;
+ aorai_x = x;
}
+ else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (7 == aorai_CurStates)
+ if (x == 3) {
+ aorai_CurStates = aorai_intermediate_state_2;
+ aorai_x_0 = x;
+ }
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
+ }
return;
}
@@ -214,14 +221,30 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- if (4 == aorai_CurStates && aorai_x_0 == 3) aorai_CurStates = OK;
- else
- if (1 == aorai_CurStates && aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
- else
- if (4 == aorai_CurStates && aorai_x_0 != 3) aorai_CurStates = aorai_reject;
- else
- if (1 == aorai_CurStates && aorai_x != 1) aorai_CurStates = aorai_reject;
+ if (4 == aorai_CurStates) {
+ if (aorai_x_0 == 3) aorai_CurStates = OK; else goto __aorai_label_2;
+ }
+ else {
+ __aorai_label_2: ;
+ if (1 == aorai_CurStates) {
+ if (aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
+ else goto __aorai_label_1;
+ }
+ else {
+ __aorai_label_1: ;
+ if (4 == aorai_CurStates) {
+ if (aorai_x_0 != 3) aorai_CurStates = aorai_reject;
+ else goto __aorai_label_0;
+ }
+ else {
+ __aorai_label_0: ;
+ if (1 == aorai_CurStates)
+ if (aorai_x != 1) aorai_CurStates = aorai_reject;
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
+ }
+ }
+ }
return;
}
@@ -422,14 +445,20 @@ int f(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
- if (3 == aorai_CurStates && aorai_y == 2) aorai_CurStates = OK;
- else
+ if (3 == aorai_CurStates) {
+ if (aorai_y == 2) aorai_CurStates = OK; else goto __aorai_label_3;
+ }
+ else {
+ __aorai_label_3: ;
if (0 == aorai_CurStates) aorai_CurStates = OK;
else
if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
else
- if (3 == aorai_CurStates && aorai_y != 2) aorai_CurStates = aorai_reject;
+ if (3 == aorai_CurStates)
+ if (aorai_y != 2) aorai_CurStates = aorai_reject;
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
+ }
return;
}
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 29ffb1ff422b6b31e10952122c05b1f1ff1d650c..e12c959752873c4d604e10d17aab160fa76caab2 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -317,10 +317,14 @@ int main_bhv_bhv(int c); */
aorai_reject_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
aorai_intermediate_state_1_tmp = 0;
- if (S0 == 1 && c <= 0) aorai_intermediate_state_0_tmp = 1;
+ if (S0 == 1)
+ if (c <= 0) aorai_intermediate_state_0_tmp = 1;
+ else aorai_intermediate_state_0_tmp = 0;
else aorai_intermediate_state_0_tmp = 0;
bhv_aux = main_bhv_bhv(c);
- if (S0 == 1 && bhv_aux) aorai_intermediate_state_tmp = 1;
+ if (S0 == 1)
+ if (bhv_aux) aorai_intermediate_state_tmp = 1;
+ else aorai_intermediate_state_tmp = 0;
else aorai_intermediate_state_tmp = 0;
Sf_tmp = 0;
S0_tmp = 0;
@@ -409,17 +413,25 @@ int main_bhv_bhv(int c); */
aorai_intermediate_state_1_tmp = aorai_intermediate_state_1;
aorai_intermediate_state_2_tmp = aorai_intermediate_state_2;
aorai_reject_tmp = aorai_reject;
- if ((aorai_intermediate_state_0 == 1 || aorai_intermediate_state_2 == 1 &&
- res != 0) || aorai_reject == 1)
- aorai_reject_tmp = 1;
- else aorai_reject_tmp = 0;
+ if (aorai_intermediate_state_0 == 1) aorai_reject_tmp = 1;
+ else
+ if (aorai_intermediate_state_2 == 1) {
+ if (res != 0) aorai_reject_tmp = 1; else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (aorai_reject == 1) aorai_reject_tmp = 1;
+ else aorai_reject_tmp = 0;
+ }
aorai_intermediate_state_2_tmp = 0;
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
- if (aorai_intermediate_state == 1 || aorai_intermediate_state_2 == 1 &&
- res == 0) Sf_tmp = 1;
- else Sf_tmp = 0;
+ if (aorai_intermediate_state == 1) Sf_tmp = 1;
+ else
+ if (aorai_intermediate_state_2 == 1)
+ if (res == 0) Sf_tmp = 1; else Sf_tmp = 0;
+ else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle b/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ceb4a227b1d51c000271a29f18529f2f427b3e0b
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
@@ -0,0 +1,164 @@
+[kernel] Parsing tests/ya/logical_operators.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_logical_operators_0.i (no preprocessing)
+/* Generated by Frama-C */
+enum aorai_ListOper {
+ op_f = 1,
+ op_main = 0
+};
+enum aorai_OpStatusList {
+ aorai_Terminated = 1,
+ aorai_Called = 0
+};
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
+/*@ ghost int I = 1; */
+/*@ ghost
+ /@ requires 1 ≡ I;
+ requires 1 ≡ I ⇒ x ≡ 1 ∨ x ≢ 1;
+ ensures aorai_CurOpStatus ≡ aorai_Called;
+ ensures aorai_CurOperation ≡ op_f;
+ assigns aorai_CurOpStatus, aorai_CurOperation, I;
+
+ behavior buch_state_I_in:
+ assumes 1 ≡ I ∧ (x ≡ 1 ∨ x ≢ 1);
+ ensures 1 ≡ I;
+
+ behavior buch_state_I_out:
+ assumes 0 ≡ I ∨ (¬(x ≡ 1) ∧ ¬(x ≢ 1));
+ ensures 0 ≡ I;
+ @/
+ void f_pre_func(int x)
+ {
+ int I_tmp;
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Called;
+ aorai_CurOperation = op_f;
+ I_tmp = I;
+ if (I == 1) {
+ if (x != 1) I_tmp = 1; else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (I == 1)
+ if (x == 1) I_tmp = 1; else I_tmp = 0;
+ else I_tmp = 0;
+ }
+ I = I_tmp;
+ return;
+ }
+
+*/
+
+/*@ ghost
+ /@ requires 1 ≡ I;
+ ensures aorai_CurOpStatus ≡ aorai_Terminated;
+ ensures aorai_CurOperation ≡ op_f;
+ assigns aorai_CurOpStatus, aorai_CurOperation, I;
+
+ behavior buch_state_I_in:
+ assumes 1 ≡ I;
+ ensures 1 ≡ I;
+
+ behavior buch_state_I_out:
+ assumes 0 ≡ I;
+ ensures 0 ≡ I;
+ @/
+ void f_post_func(void)
+ {
+ int I_tmp;
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Terminated;
+ aorai_CurOperation = op_f;
+ I_tmp = I;
+ if (I == 1) I_tmp = 1; else I_tmp = 0;
+ I = I_tmp;
+ return;
+ }
+
+*/
+
+/*@ requires 1 ≡ I;
+ requires 1 ≡ I ⇒ x ≡ 1 ∨ x ≢ 1;
+
+ behavior Buchi_property_behavior:
+ ensures \true;
+ ensures 1 ≡ I;
+ */
+void f(int x)
+{
+ /*@ ghost f_pre_func(x); */
+ /*@ ghost f_post_func(); */
+ return;
+}
+
+/*@ ghost
+ /@ requires 1 ≡ I;
+ ensures aorai_CurOpStatus ≡ aorai_Called;
+ ensures aorai_CurOperation ≡ op_main;
+ assigns aorai_CurOpStatus, aorai_CurOperation, I;
+
+ behavior buch_state_I_in:
+ assumes 1 ≡ I;
+ ensures 1 ≡ I;
+
+ behavior buch_state_I_out:
+ assumes 0 ≡ I;
+ ensures 0 ≡ I;
+ @/
+ void main_pre_func(int x)
+ {
+ int I_tmp;
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Called;
+ aorai_CurOperation = op_main;
+ I_tmp = I;
+ if (I == 1) I_tmp = 1; else I_tmp = 0;
+ I = I_tmp;
+ return;
+ }
+
+*/
+
+/*@ ghost
+ /@ requires 1 ≡ I;
+ ensures aorai_CurOpStatus ≡ aorai_Terminated;
+ ensures aorai_CurOperation ≡ op_main;
+ assigns aorai_CurOpStatus, aorai_CurOperation, I;
+
+ behavior buch_state_I_in:
+ assumes 1 ≡ I;
+ ensures 1 ≡ I;
+
+ behavior buch_state_I_out:
+ assumes 0 ≡ I;
+ ensures 0 ≡ I;
+ @/
+ void main_post_func(void)
+ {
+ int I_tmp;
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Terminated;
+ aorai_CurOperation = op_main;
+ I_tmp = I;
+ if (I == 1) I_tmp = 1; else I_tmp = 0;
+ I = I_tmp;
+ return;
+ }
+
+*/
+
+/*@ requires 1 ≡ I;
+
+ behavior Buchi_property_behavior:
+ ensures \true;
+ ensures 1 ≡ I;
+ */
+void main(int x)
+{
+ /*@ ghost main_pre_func(x); */
+ f(x);
+ /*@ ghost main_post_func(); */
+ return;
+}
+
+
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 6569b67175a8280471a8c3cb305840c14053e5e4..a841b2ae6cb354b8356ef6085aed341366e607fb 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -95,10 +95,14 @@ enum aorai_OpStatusList {
aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
aorai_intermediate_state_3_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
- if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1 &&
- aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
- else aorai_intermediate_state_1_tmp = 0;
- if (aorai_intermediate_state_0 == 1 && aorai_counter < 5) aorai_counter ++;
+ if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1;
+ else
+ if (aorai_intermediate_state_0 == 1)
+ if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
+ else aorai_intermediate_state_1_tmp = 0;
+ else aorai_intermediate_state_1_tmp = 0;
+ if (aorai_intermediate_state_0 == 1)
+ if (aorai_counter < 5) aorai_counter ++;
if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
@@ -544,9 +548,9 @@ void g(void)
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
- if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1)
- Sf_tmp = 1;
- else Sf_tmp = 0;
+ if (aorai_intermediate_state == 1) Sf_tmp = 1;
+ else
+ if (aorai_intermediate_state_0 == 1) Sf_tmp = 1; else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
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 1ad02912fd111f3df968455278a5dfbb2ae8e8f7..e0f52649ef1a85e9ed3156cee2d3546c0a0834b6 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -363,7 +363,9 @@ void g(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_h;
- if (5 == aorai_CurStates && aorai_x > 0) aorai_CurStates = f_0;
+ if (5 == aorai_CurStates)
+ if (aorai_x > 0) aorai_CurStates = f_0;
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
return;
}
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 79d8cc18058df72e85381c46d1d59f80ff09f81d..e730bc38477b677a248a6e25f010b818ccb37633 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -39,7 +39,9 @@ enum aorai_OpStatusList {
aorai_CurOperation = op_f;
S0_tmp = S0;
Sf_tmp = Sf;
- if (S0 == 1 && x >= 4) Sf_tmp = 1; else Sf_tmp = 0;
+ if (S0 == 1)
+ if (x >= 4) Sf_tmp = 1; else Sf_tmp = 0;
+ else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
index d7146144fdf2901adb66b6a09f4c2a019c0cd8fb..2e3147482222b4e9f67b5b2e832507fa156434cc 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -65,13 +65,42 @@ int x = 0;
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
- step1_tmp = 1;
- else step1_tmp = 0;
- if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
- else last_tmp = 0;
- if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
- else init_tmp = 0;
+ if (init == 1) {
+ if (x == 3) step1_tmp = 1; else goto __aorai_label_2;
+ }
+ else {
+ __aorai_label_2: ;
+ if (last == 1) {
+ if (x == 3) step1_tmp = 1; else goto __aorai_label_1;
+ }
+ else {
+ __aorai_label_1: ;
+ if (step1 == 1)
+ if (x != 4) step1_tmp = 1; else step1_tmp = 0;
+ else step1_tmp = 0;
+ }
+ }
+ if (last == 1) {
+ if (x != 4) {
+ if (x != 3) last_tmp = 1; else goto __aorai_label_0;
+ }
+ else goto __aorai_label_0;
+ }
+ else {
+ __aorai_label_0: ;
+ if (step1 == 1)
+ if (x == 4) last_tmp = 1; else last_tmp = 0;
+ else last_tmp = 0;
+ }
+ if (init == 1) {
+ if (x != 3) init_tmp = 1; else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (last == 1)
+ if (x == 4) init_tmp = 1; else init_tmp = 0;
+ else init_tmp = 0;
+ }
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -129,13 +158,42 @@ int x = 0;
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
- step1_tmp = 1;
- else step1_tmp = 0;
- if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
- else last_tmp = 0;
- if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
- else init_tmp = 0;
+ if (init == 1) {
+ if (x == 3) step1_tmp = 1; else goto __aorai_label_6;
+ }
+ else {
+ __aorai_label_6: ;
+ if (last == 1) {
+ if (x == 3) step1_tmp = 1; else goto __aorai_label_5;
+ }
+ else {
+ __aorai_label_5: ;
+ if (step1 == 1)
+ if (x != 4) step1_tmp = 1; else step1_tmp = 0;
+ else step1_tmp = 0;
+ }
+ }
+ if (last == 1) {
+ if (x != 4) {
+ if (x != 3) last_tmp = 1; else goto __aorai_label_4;
+ }
+ else goto __aorai_label_4;
+ }
+ else {
+ __aorai_label_4: ;
+ if (step1 == 1)
+ if (x == 4) last_tmp = 1; else last_tmp = 0;
+ else last_tmp = 0;
+ }
+ if (init == 1) {
+ if (x != 3) init_tmp = 1; else goto __aorai_label_3;
+ }
+ else {
+ __aorai_label_3: ;
+ if (last == 1)
+ if (x == 4) init_tmp = 1; else init_tmp = 0;
+ else init_tmp = 0;
+ }
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -257,13 +315,42 @@ void f(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
- step1_tmp = 1;
- else step1_tmp = 0;
- if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
- else last_tmp = 0;
- if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
- else init_tmp = 0;
+ if (init == 1) {
+ if (x == 3) step1_tmp = 1; else goto __aorai_label_10;
+ }
+ else {
+ __aorai_label_10: ;
+ if (last == 1) {
+ if (x == 3) step1_tmp = 1; else goto __aorai_label_9;
+ }
+ else {
+ __aorai_label_9: ;
+ if (step1 == 1)
+ if (x != 4) step1_tmp = 1; else step1_tmp = 0;
+ else step1_tmp = 0;
+ }
+ }
+ if (last == 1) {
+ if (x != 4) {
+ if (x != 3) last_tmp = 1; else goto __aorai_label_8;
+ }
+ else goto __aorai_label_8;
+ }
+ else {
+ __aorai_label_8: ;
+ if (step1 == 1)
+ if (x == 4) last_tmp = 1; else last_tmp = 0;
+ else last_tmp = 0;
+ }
+ if (init == 1) {
+ if (x != 3) init_tmp = 1; else goto __aorai_label_7;
+ }
+ else {
+ __aorai_label_7: ;
+ if (last == 1)
+ if (x == 4) init_tmp = 1; else init_tmp = 0;
+ else init_tmp = 0;
+ }
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -321,13 +408,42 @@ void f(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
- step1_tmp = 1;
- else step1_tmp = 0;
- if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
- else last_tmp = 0;
- if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
- else init_tmp = 0;
+ if (init == 1) {
+ if (x == 3) step1_tmp = 1; else goto __aorai_label_14;
+ }
+ else {
+ __aorai_label_14: ;
+ if (last == 1) {
+ if (x == 3) step1_tmp = 1; else goto __aorai_label_13;
+ }
+ else {
+ __aorai_label_13: ;
+ if (step1 == 1)
+ if (x != 4) step1_tmp = 1; else step1_tmp = 0;
+ else step1_tmp = 0;
+ }
+ }
+ if (last == 1) {
+ if (x != 4) {
+ if (x != 3) last_tmp = 1; else goto __aorai_label_12;
+ }
+ else goto __aorai_label_12;
+ }
+ else {
+ __aorai_label_12: ;
+ if (step1 == 1)
+ if (x == 4) last_tmp = 1; else last_tmp = 0;
+ else last_tmp = 0;
+ }
+ if (init == 1) {
+ if (x != 3) init_tmp = 1; else goto __aorai_label_11;
+ }
+ else {
+ __aorai_label_11: ;
+ if (last == 1)
+ if (x == 4) init_tmp = 1; else init_tmp = 0;
+ else init_tmp = 0;
+ }
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -436,9 +552,13 @@ void g(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1 && x == 3) step1_tmp = 1; else step1_tmp = 0;
+ if (init == 1)
+ if (x == 3) step1_tmp = 1; else step1_tmp = 0;
+ else step1_tmp = 0;
last_tmp = 0;
- if (init == 1 && x != 3) init_tmp = 1; else init_tmp = 0;
+ if (init == 1)
+ if (x != 3) init_tmp = 1; else init_tmp = 0;
+ else init_tmp = 0;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -496,13 +616,42 @@ void g(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
- step1_tmp = 1;
- else step1_tmp = 0;
- if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
- else last_tmp = 0;
- if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
- else init_tmp = 0;
+ if (init == 1) {
+ if (x == 3) step1_tmp = 1; else goto __aorai_label_18;
+ }
+ else {
+ __aorai_label_18: ;
+ if (last == 1) {
+ if (x == 3) step1_tmp = 1; else goto __aorai_label_17;
+ }
+ else {
+ __aorai_label_17: ;
+ if (step1 == 1)
+ if (x != 4) step1_tmp = 1; else step1_tmp = 0;
+ else step1_tmp = 0;
+ }
+ }
+ if (last == 1) {
+ if (x != 4) {
+ if (x != 3) last_tmp = 1; else goto __aorai_label_16;
+ }
+ else goto __aorai_label_16;
+ }
+ else {
+ __aorai_label_16: ;
+ if (step1 == 1)
+ if (x == 4) last_tmp = 1; else last_tmp = 0;
+ else last_tmp = 0;
+ }
+ if (init == 1) {
+ if (x != 3) init_tmp = 1; else goto __aorai_label_15;
+ }
+ else {
+ __aorai_label_15: ;
+ if (last == 1)
+ if (x == 4) init_tmp = 1; else init_tmp = 0;
+ else init_tmp = 0;
+ }
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index 92b8136c6f9ff6db57d75f729389cec00afcbff5..f138130a17043ef5c0dfc68304ce9c0e1c1a03ba 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -280,10 +280,16 @@ void f(void)
aorai_intermediate_state_1_tmp = aorai_intermediate_state_1;
aorai_intermediate_state_2_tmp = aorai_intermediate_state_2;
aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
- if ((aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1) ||
- aorai_intermediate_state_2 == 1 && aorai_counter < 2) aorai_intermediate_state_3_tmp = 1;
- else aorai_intermediate_state_3_tmp = 0;
- if (aorai_intermediate_state_2 == 1 && aorai_counter < 2) aorai_counter ++;
+ if (aorai_intermediate_state == 1) aorai_intermediate_state_3_tmp = 1;
+ else
+ if (aorai_intermediate_state_0 == 1) aorai_intermediate_state_3_tmp = 1;
+ else
+ if (aorai_intermediate_state_2 == 1)
+ if (aorai_counter < 2) aorai_intermediate_state_3_tmp = 1;
+ else aorai_intermediate_state_3_tmp = 0;
+ else aorai_intermediate_state_3_tmp = 0;
+ if (aorai_intermediate_state_2 == 1)
+ if (aorai_counter < 2) aorai_counter ++;
if (aorai_intermediate_state_0 == 1) aorai_counter = 1;
if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_2_tmp = 0;
@@ -567,7 +573,8 @@ void g(void)
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
- if (aorai_intermediate_state_2 == 1 && 1 <= aorai_counter) Sf_tmp = 1;
+ if (aorai_intermediate_state_2 == 1)
+ if (1 <= aorai_counter) Sf_tmp = 1; else Sf_tmp = 0;
else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
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 ea66b1d2bf754868b2a05efbd8b9c8dc413a61bc..eca76ebee16395bc7760001c98e2c849a29754b6 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -95,10 +95,14 @@ enum aorai_OpStatusList {
aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
aorai_intermediate_state_3_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
- if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1 &&
- aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
- else aorai_intermediate_state_1_tmp = 0;
- if (aorai_intermediate_state_0 == 1 && aorai_counter < 5) aorai_counter ++;
+ if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1;
+ else
+ if (aorai_intermediate_state_0 == 1)
+ if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
+ else aorai_intermediate_state_1_tmp = 0;
+ else aorai_intermediate_state_1_tmp = 0;
+ if (aorai_intermediate_state_0 == 1)
+ if (aorai_counter < 5) aorai_counter ++;
if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
@@ -544,9 +548,9 @@ void g(void)
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
- if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1)
- Sf_tmp = 1;
- else Sf_tmp = 0;
+ if (aorai_intermediate_state == 1) Sf_tmp = 1;
+ else
+ if (aorai_intermediate_state_0 == 1) Sf_tmp = 1; else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index dbf366abac3bc1121b9765732ddf45aecf90f3e7..8d2600bdb03f86874f050d4b8a2b1d5dc568afbd 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -276,7 +276,7 @@
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
11 functions analyzed (out of 11): 100% coverage.
- In these functions, 206 statements reached (out of 261): 78% coverage.
+ In these functions, 273 statements reached (out of 339): 80% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 0 warnings
@@ -576,46 +576,123 @@ int n = 0;
aorai_CurOperation = op_input_status;
aorai_StatesHistory_2 = aorai_StatesHistory_1;
aorai_StatesHistory_1 = aorai_CurStates;
- if (18 == aorai_CurStates && ((res & 15) != 1 && (res & 1) != 0))
- aorai_CurStates = StatusError;
- else
- if (17 == aorai_CurStates && ((res & 15) != 1 && (res & 1) != 0))
- aorai_CurStates = StatusError;
- else
- if (16 == aorai_CurStates && ((res & 15) != 1 && (res & 1) != 0))
- aorai_CurStates = StatusError;
- else
- if (15 == aorai_CurStates && ((res & 15) != 1 && (res & 1) != 0))
- aorai_CurStates = StatusError;
- else
- if (14 == aorai_CurStates && ((res & 15) != 1 && (res & 1) != 0))
- aorai_CurStates = StatusError;
- else
- if (14 == aorai_CurStates && (res & 15) == 1) aorai_CurStates = StatusOk1;
- else
- if (15 == aorai_CurStates && (res & 15) == 1) aorai_CurStates = StatusOk2;
- else
- if (16 == aorai_CurStates && (res & 15) == 1) aorai_CurStates = StatusOk3;
- else
- if (17 == aorai_CurStates && (res & 15) == 1) aorai_CurStates = StatusOk4;
- else
- if (18 == aorai_CurStates && (res & 15) == 1) aorai_CurStates = StatusOk5;
- else
- if (14 == aorai_CurStates && (res & 1) == 0)
- aorai_CurStates = Wait1;
- else
- if (15 == aorai_CurStates && (res & 1) == 0)
- aorai_CurStates = Wait2;
- else
- if (16 == aorai_CurStates && (res & 1) == 0)
- aorai_CurStates = Wait3;
- else
- if (17 == aorai_CurStates && (res & 1) == 0)
- aorai_CurStates = Wait4;
- else
- if (18 == aorai_CurStates && (res & 1) == 0)
- aorai_CurStates = Wait5;
+ if (18 == aorai_CurStates) {
+ if ((res & 15) != 1) {
+ if ((res & 1) != 0) aorai_CurStates = StatusError;
+ else goto __aorai_label_12;
+ }
+ else goto __aorai_label_12;
+ }
+ else {
+ __aorai_label_12: ;
+ if (17 == aorai_CurStates) {
+ if ((res & 15) != 1) {
+ if ((res & 1) != 0) aorai_CurStates = StatusError;
+ else goto __aorai_label_11;
+ }
+ else goto __aorai_label_11;
+ }
+ else {
+ __aorai_label_11: ;
+ if (16 == aorai_CurStates) {
+ if ((res & 15) != 1) {
+ if ((res & 1) != 0) aorai_CurStates = StatusError;
+ else goto __aorai_label_10;
+ }
+ else goto __aorai_label_10;
+ }
+ else {
+ __aorai_label_10: ;
+ if (15 == aorai_CurStates) {
+ if ((res & 15) != 1) {
+ if ((res & 1) != 0) aorai_CurStates = StatusError;
+ else goto __aorai_label_9;
+ }
+ else goto __aorai_label_9;
+ }
+ else {
+ __aorai_label_9: ;
+ if (14 == aorai_CurStates) {
+ if ((res & 15) != 1) {
+ if ((res & 1) != 0) aorai_CurStates = StatusError;
+ else goto __aorai_label_8;
+ }
+ else goto __aorai_label_8;
+ }
+ else {
+ __aorai_label_8: ;
+ if (14 == aorai_CurStates) {
+ if ((res & 15) == 1) aorai_CurStates = StatusOk1;
+ else goto __aorai_label_7;
+ }
+ else {
+ __aorai_label_7: ;
+ if (15 == aorai_CurStates) {
+ if ((res & 15) == 1) aorai_CurStates = StatusOk2;
+ else goto __aorai_label_6;
+ }
+ else {
+ __aorai_label_6: ;
+ if (16 == aorai_CurStates) {
+ if ((res & 15) == 1) aorai_CurStates = StatusOk3;
+ else goto __aorai_label_5;
+ }
+ else {
+ __aorai_label_5: ;
+ if (17 == aorai_CurStates) {
+ if ((res & 15) == 1) aorai_CurStates = StatusOk4;
+ else goto __aorai_label_4;
+ }
+ else {
+ __aorai_label_4: ;
+ if (18 == aorai_CurStates) {
+ if ((res & 15) == 1) aorai_CurStates = StatusOk5;
+ else goto __aorai_label_3;
+ }
+ else {
+ __aorai_label_3: ;
+ if (14 == aorai_CurStates) {
+ if ((res & 1) == 0) aorai_CurStates = Wait1;
+ else goto __aorai_label_2;
+ }
+ else {
+ __aorai_label_2: ;
+ if (15 == aorai_CurStates) {
+ if ((res & 1) == 0) aorai_CurStates = Wait2;
+ else goto __aorai_label_1;
+ }
+ else {
+ __aorai_label_1: ;
+ if (16 == aorai_CurStates) {
+ if ((res & 1) == 0) aorai_CurStates = Wait3;
+ else goto __aorai_label_0;
+ }
+ else {
+ __aorai_label_0: ;
+ if (17 == aorai_CurStates) {
+ if ((res & 1) == 0) aorai_CurStates = Wait4;
+ else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (18 == aorai_CurStates)
+ if ((res & 1) == 0) aorai_CurStates = Wait5;
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
/@ assert Aorai: aorai_smoke_test: aorai_CurStates ≢ aorai_reject; @/
;
return;
@@ -682,54 +759,121 @@ int input_status(void)
aorai_CurOperation = op_input_data;
aorai_StatesHistory_2 = aorai_StatesHistory_1;
aorai_StatesHistory_1 = aorai_CurStates;
- if (5 == aorai_CurStates && (res & 128) == 0) {
- aorai_CurStates = Complete;
- aorai_y2 = res;
+ if (5 == aorai_CurStates) {
+ if ((res & 128) == 0) {
+ aorai_CurStates = Complete;
+ aorai_y2 = res;
+ }
+ else goto __aorai_label_26;
}
else
+ __aorai_label_26:
if (6 == aorai_CurStates) aorai_CurStates = Wait1;
else
- if (5 == aorai_CurStates && (res & 192) == 192) aorai_CurStates = Wait1;
- else
- if (4 == aorai_CurStates && (res & 192) == 192) aorai_CurStates = Wait1;
- else
- if (3 == aorai_CurStates && (res & 192) == 192) aorai_CurStates = Wait1;
- else
- if (2 == aorai_CurStates && (res & 192) == 192) aorai_CurStates = Wait1;
- else
- if (1 == aorai_CurStates && (res & 128) == 0) aorai_CurStates = Wait1;
- else
- if (1 == aorai_CurStates && (res & 192) == 192) aorai_CurStates = Wait1;
- else
- if (5 == aorai_CurStates && (res & 192) == 128) aorai_CurStates = Wait2;
- else
- if (4 == aorai_CurStates && (res & 192) == 128)
- aorai_CurStates = Wait2;
- else
- if (3 == aorai_CurStates && (res & 192) == 128)
- aorai_CurStates = Wait2;
- else
- if (2 == aorai_CurStates && (res & 192) == 128)
- aorai_CurStates = Wait2;
- else
- if (1 == aorai_CurStates && (res & 192) == 128)
- aorai_CurStates = Wait2;
- else
- if (2 == aorai_CurStates && (res & 128) == 0) {
- aorai_CurStates = Wait3;
- aorai_x1 = res;
- }
- else
- if (3 == aorai_CurStates && (res & 128) == 0) {
- aorai_CurStates = Wait4;
- aorai_x2 = res;
+ if (5 == aorai_CurStates) {
+ if ((res & 192) == 192) aorai_CurStates = Wait1;
+ else goto __aorai_label_25;
+ }
+ else {
+ __aorai_label_25: ;
+ if (4 == aorai_CurStates) {
+ if ((res & 192) == 192) aorai_CurStates = Wait1;
+ else goto __aorai_label_24;
+ }
+ else {
+ __aorai_label_24: ;
+ if (3 == aorai_CurStates) {
+ if ((res & 192) == 192) aorai_CurStates = Wait1;
+ else goto __aorai_label_23;
+ }
+ else {
+ __aorai_label_23: ;
+ if (2 == aorai_CurStates) {
+ if ((res & 192) == 192) aorai_CurStates = Wait1;
+ else goto __aorai_label_22;
+ }
+ else {
+ __aorai_label_22: ;
+ if (1 == aorai_CurStates) {
+ if ((res & 128) == 0) aorai_CurStates = Wait1;
+ else goto __aorai_label_21;
+ }
+ else {
+ __aorai_label_21: ;
+ if (1 == aorai_CurStates) {
+ if ((res & 192) == 192) aorai_CurStates = Wait1;
+ else goto __aorai_label_20;
+ }
+ else {
+ __aorai_label_20: ;
+ if (5 == aorai_CurStates) {
+ if ((res & 192) == 128) aorai_CurStates = Wait2;
+ else goto __aorai_label_19;
+ }
+ else {
+ __aorai_label_19: ;
+ if (4 == aorai_CurStates) {
+ if ((res & 192) == 128) aorai_CurStates = Wait2;
+ else goto __aorai_label_18;
+ }
+ else {
+ __aorai_label_18: ;
+ if (3 == aorai_CurStates) {
+ if ((res & 192) == 128) aorai_CurStates = Wait2;
+ else goto __aorai_label_17;
+ }
+ else {
+ __aorai_label_17: ;
+ if (2 == aorai_CurStates) {
+ if ((res & 192) == 128) aorai_CurStates = Wait2;
+ else goto __aorai_label_16;
+ }
+ else {
+ __aorai_label_16: ;
+ if (1 == aorai_CurStates) {
+ if ((res & 192) == 128) aorai_CurStates = Wait2;
+ else goto __aorai_label_15;
+ }
+ else {
+ __aorai_label_15: ;
+ if (2 == aorai_CurStates) {
+ if ((res & 128) == 0) {
+ aorai_CurStates = Wait3;
+ aorai_x1 = res;
}
- else
- if (4 == aorai_CurStates && (res & 128) == 0) {
- aorai_CurStates = Wait5;
- aorai_y1 = res;
+ else goto __aorai_label_14;
+ }
+ else {
+ __aorai_label_14: ;
+ if (3 == aorai_CurStates) {
+ if ((res & 128) == 0) {
+ aorai_CurStates = Wait4;
+ aorai_x2 = res;
}
+ else goto __aorai_label_13;
+ }
+ else {
+ __aorai_label_13: ;
+ if (4 == aorai_CurStates)
+ if ((res & 128) == 0) {
+ aorai_CurStates = Wait5;
+ aorai_y1 = res;
+ }
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
/@ assert Aorai: aorai_smoke_test: aorai_CurStates ≢ aorai_reject; @/
;
return;
@@ -781,18 +925,21 @@ int input_data(void)
else
if (8 == aorai_CurStates) aorai_CurStates = Error;
else
- if (0 == aorai_CurStates && (y != aorai_y1 +
- 128 * aorai_y2 ||
- x != aorai_x1 +
- 128 * aorai_x2))
- aorai_CurStates = Error;
- else
- if (0 == aorai_CurStates && (x == aorai_x1 +
- 128 * aorai_x2 &&
- y == aorai_y1 +
- 128 * aorai_y2))
- aorai_CurStates = Wait1;
+ if (0 == aorai_CurStates) {
+ if (y != aorai_y1 + 128 * aorai_y2) aorai_CurStates = Error;
+ else
+ if (x != aorai_x1 + 128 * aorai_x2) aorai_CurStates = Error;
+ else goto __aorai_label_27;
+ }
+ else {
+ __aorai_label_27: ;
+ if (0 == aorai_CurStates)
+ if (x == aorai_x1 + 128 * aorai_x2)
+ if (y == aorai_y1 + 128 * aorai_y2) aorai_CurStates = Wait1;
+ else aorai_CurStates = aorai_reject;
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
+ }
/@ assert Aorai: aorai_smoke_test: aorai_CurStates ≢ aorai_reject; @/
;
return;
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index 1c87bd335767554b3c662d504f66f15913c08133..07be92bb84c1e913883720f6526540093c92c847 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -219,7 +219,9 @@ void push(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_pop;
- if (4 == aorai_CurStates && aorai_n > 0) aorai_CurStates = emptying_stack;
+ if (4 == aorai_CurStates)
+ if (aorai_n > 0) aorai_CurStates = emptying_stack;
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
return;
}
@@ -277,16 +279,23 @@ void push(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_pop;
- if (3 == aorai_CurStates && aorai_n == 1) {
- aorai_CurStates = empty_stack;
- aorai_n --;
- }
- else
- if (3 == aorai_CurStates && aorai_n > 1) {
- aorai_CurStates = filled_stack;
+ if (3 == aorai_CurStates) {
+ if (aorai_n == 1) {
+ aorai_CurStates = empty_stack;
aorai_n --;
}
+ else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (3 == aorai_CurStates)
+ if (aorai_n > 1) {
+ aorai_CurStates = filled_stack;
+ aorai_n --;
+ }
+ else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
+ }
return;
}
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 72d1dbd1b7087f20168713e8811b6529fe5047c3..612b29ad3f47dd7c69c00b06d430c8e92ce23b48 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
@@ -76,7 +76,9 @@ int rr = 1;
SF_tmp = 0;
S4_tmp = 0;
S3_tmp = 0;
- if (S1 == 1 && i >= 0) S2_tmp = 1; else S2_tmp = 0;
+ if (S1 == 1)
+ if (i >= 0) S2_tmp = 1; else S2_tmp = 0;
+ else S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
@@ -294,7 +296,9 @@ void opa(int i, int j)
SF_tmp = SF;
mainst_tmp = mainst;
mainst_tmp = 0;
- if (S4 == 1 && res > 0) SF_tmp = 1; else SF_tmp = 0;
+ if (S4 == 1)
+ if (res > 0) SF_tmp = 1; else SF_tmp = 0;
+ else SF_tmp = 0;
S4_tmp = 0;
S3_tmp = 0;
S2_tmp = 0;
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 f20db94ee5b3eb2af611286e49d3866b42e02735..af3a83362234cacdf672489228e7892abb9b8502 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
@@ -82,7 +82,9 @@ int rr = 1;
S6_tmp = 0;
S5_tmp = 0;
S4_tmp = 0;
- if (S2 == 1 && r >= 0) S3_tmp = 1; else S3_tmp = 0;
+ if (S2 == 1)
+ if (r >= 0) S3_tmp = 1; else S3_tmp = 0;
+ else S3_tmp = 0;
S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
@@ -155,7 +157,9 @@ int rr = 1;
S7_tmp = 0;
S6_tmp = 0;
S5_tmp = 0;
- if (S3 == 1 && res <= 5000) S4_tmp = 1; else S4_tmp = 0;
+ if (S3 == 1)
+ if (res <= 5000) S4_tmp = 1; else S4_tmp = 0;
+ else S4_tmp = 0;
S3_tmp = 0;
S2_tmp = 0;
S1_tmp = 0;
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 d9e7db7f8036d21031746b26ee84b19aa5ffcf14..028e81110750d6e5129071ba1589b3f81fc73a1c 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
@@ -98,9 +98,13 @@ enum aorai_OpStatusList {
End_tmp = End;
Idle_tmp = Idle;
WillDoFoo_tmp = WillDoFoo;
- if (Idle == 1 && res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
+ if (Idle == 1)
+ if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
+ else WillDoFoo_tmp = 0;
Idle_tmp = 0;
- if (Idle == 1 && res != -1) End_tmp = 1; else End_tmp = 0;
+ if (Idle == 1)
+ if (res != -1) End_tmp = 1; else End_tmp = 0;
+ else End_tmp = 0;
End = End_tmp;
Idle = Idle_tmp;
WillDoFoo = WillDoFoo_tmp;
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 ed5f20033adfc02c42e59041a6d3fc7548e8ef8d..b174e49f3f32ad748fe314886ba421d842fcdaaa 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -216,7 +216,9 @@ int decode_int(char *s)
S2_tmp = S2;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1 || S2 == 1) S2_tmp = 1; else S2_tmp = 0;
+ if (S1 == 1) S2_tmp = 1;
+ else
+ if (S2 == 1) S2_tmp = 1; else S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
@@ -263,8 +265,12 @@ int decode_int(char *s)
S2_tmp = S2;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1 || S2 == 1) S2_tmp = 1; else S2_tmp = 0;
- if (S1 == 1 || S2 == 1) S1_tmp = 1; else S1_tmp = 0;
+ if (S1 == 1) S2_tmp = 1;
+ else
+ if (S2 == 1) S2_tmp = 1; else S2_tmp = 0;
+ if (S1 == 1) S1_tmp = 1;
+ else
+ if (S2 == 1) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
main_0 = main_0_tmp;
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 3f9a007d77696b6178c88a55def1baf568004e5c..650a1625271f495e71a3d1411bb69d151e7a8410 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -101,11 +101,25 @@ enum aorai_OpStatusList {
End_tmp = End;
Idle_tmp = Idle;
WillDoFoo_tmp = WillDoFoo;
- if (Idle == 1 && res == -1 || WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1;
- else WillDoFoo_tmp = 0;
+ if (Idle == 1) {
+ if (res == -1) WillDoFoo_tmp = 1; else goto __aorai_label_0;
+ }
+ else {
+ __aorai_label_0: ;
+ if (WillDoFoo == 1)
+ if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
+ else WillDoFoo_tmp = 0;
+ }
Idle_tmp = 0;
- if (End == 1 && res != -1 || Idle == 1 && res != -1) End_tmp = 1;
- else End_tmp = 0;
+ if (End == 1) {
+ if (res != -1) End_tmp = 1; else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (Idle == 1)
+ if (res != -1) End_tmp = 1; else End_tmp = 0;
+ else End_tmp = 0;
+ }
End = End_tmp;
Idle = Idle_tmp;
WillDoFoo = WillDoFoo_tmp;
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 b3d197570e702e04d0d7730ca993dd6fa5d6faa1..c4af634f2defb5bcdfac58923933c684aba9f991 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -124,10 +124,24 @@ enum aorai_OpStatusList {
Idle_tmp = Idle;
IgnoreFoo_tmp = IgnoreFoo;
WillDoFoo_tmp = WillDoFoo;
- if (Idle == 1 && res == -1 || WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1;
- else WillDoFoo_tmp = 0;
- if (Idle == 1 && res != -1 || IgnoreFoo == 1 && res != -1) IgnoreFoo_tmp = 1;
- else IgnoreFoo_tmp = 0;
+ if (Idle == 1) {
+ if (res == -1) WillDoFoo_tmp = 1; else goto __aorai_label_0;
+ }
+ else {
+ __aorai_label_0: ;
+ if (WillDoFoo == 1)
+ if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
+ else WillDoFoo_tmp = 0;
+ }
+ if (Idle == 1) {
+ if (res != -1) IgnoreFoo_tmp = 1; else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (IgnoreFoo == 1)
+ if (res != -1) IgnoreFoo_tmp = 1; else IgnoreFoo_tmp = 0;
+ else IgnoreFoo_tmp = 0;
+ }
Idle_tmp = 0;
End_tmp = 0;
End = End_tmp;
@@ -281,11 +295,14 @@ int isPresentRec(int *t, int i, int max, int val)
Idle_tmp = Idle;
IgnoreFoo_tmp = IgnoreFoo;
WillDoFoo_tmp = WillDoFoo;
- if (WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1;
+ if (WillDoFoo == 1)
+ if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
else WillDoFoo_tmp = 0;
IgnoreFoo_tmp = 0;
Idle_tmp = 0;
- if (IgnoreFoo == 1 && res != -1) End_tmp = 1; else End_tmp = 0;
+ if (IgnoreFoo == 1)
+ if (res != -1) End_tmp = 1; else End_tmp = 0;
+ else End_tmp = 0;
End = End_tmp;
Idle = Idle_tmp;
IgnoreFoo = IgnoreFoo_tmp;
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 fa0bb669fc7a5d68255e8ce6fc8d1bd8aabd11f6..3ba01477c274e77bf5488bd24ffe34cfe08e8fb4 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -47,7 +47,9 @@ int myAge = 0;
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
+ if (S1 == 1)
+ if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
+ else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
@@ -83,7 +85,9 @@ int myAge = 0;
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
+ if (S1 == 1)
+ if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
+ else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
@@ -136,7 +140,9 @@ void increment(void)
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (main_0 == 1 && nobody.Age == 0) S1_tmp = 1; else S1_tmp = 0;
+ if (main_0 == 1)
+ if (nobody.Age == 0) S1_tmp = 1; else S1_tmp = 0;
+ else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
@@ -172,7 +178,9 @@ void increment(void)
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
+ if (S1 == 1)
+ if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
+ else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6168c618fe79e2e0da7ebe5b8b2167825f84ce8d
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing tests/ya/logical_operators.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_logical_operators_0.i (no preprocessing)
+[wp] Warning: Missing RTE guards