From 32202fd3872e9f86341fb30eee602e28bbb6b3dc Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 12 Oct 2020 17:48:48 +0200
Subject: [PATCH] prettier oracles
---
src/plugins/aorai/tests/Aorai_test.ml | 39 +--
.../tests/ltl/oracle/test_boucle.res.oracle | 9 +-
.../tests/ltl/oracle/test_boucle1.res.oracle | 6 +-
.../tests/ltl/oracle/test_boucle2.res.oracle | 4 +-
.../tests/ltl/oracle/test_boucle3.res.oracle | 4 +-
.../ltl/oracle/test_factorial.res.oracle | 15 +-
.../ltl/oracle/test_recursion2.0.res.oracle | 6 +-
.../ltl/oracle/test_recursion2.1.res.oracle | 10 +-
.../tests/ltl/oracle/test_switch3.res.oracle | 16 +-
.../ltl/oracle/test_switch3_if.res.oracle | 16 +-
.../ltl/oracle/test_switch3_return.res.oracle | 16 +-
.../tests/ya/oracle/deterministic.res.oracle | 29 +--
.../aorai/tests/ya/oracle/formals.res.oracle | 62 ++---
.../tests/ya/oracle/hoare_seq.res.oracle | 30 +--
.../tests/ya/oracle/loop_bts1050.res.oracle | 18 +-
.../ya/oracle/metavariables-right.res.oracle | 3 +-
.../aorai/tests/ya/oracle/not_prm.res.oracle | 4 +-
.../aorai/tests/ya/oracle/other.res.oracle | 223 +++---------------
.../aorai/tests/ya/oracle/seq.res.oracle | 17 +-
.../aorai/tests/ya/oracle/seq_loop.res.oracle | 18 +-
.../aorai/tests/ya/oracle/stack.res.oracle | 23 +-
.../ya/oracle/test_acces_params.res.oracle | 8 +-
.../ya/oracle/test_acces_params2.res.oracle | 8 +-
.../test_boucle_rechercheTableau.res.oracle | 8 +-
.../tests/ya/oracle/test_factorial.res.oracle | 12 +-
.../ya/oracle/test_recursion4.res.oracle | 22 +-
.../ya/oracle/test_recursion5.res.oracle | 29 +--
.../tests/ya/oracle/test_struct.res.oracle | 16 +-
28 files changed, 175 insertions(+), 496 deletions(-)
diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index b559eeb411c..7807773dd16 100644
--- a/src/plugins/aorai/tests/Aorai_test.ml
+++ b/src/plugins/aorai/tests/Aorai_test.ml
@@ -1,15 +1,15 @@
(* Small script to test that the code generated by aorai can be parsed again
* by frama-c.
- *)
+*)
open Kernel
module P = Plugin.Register
-(struct
- let name = "aorai testing module"
- let shortname = "aorai-test"
- let help = "utility script for aorai regtests"
- end)
+ (struct
+ let name = "aorai testing module"
+ let shortname = "aorai-test"
+ let help = "utility script for aorai regtests"
+ end)
module TestNumber =
P.Zero
@@ -17,25 +17,25 @@ module TestNumber =
let option_name = "-aorai-test-number"
let help = "test number when multiple tests are run over the same file"
let arg_name = "n"
- end)
+ end)
module InternalWpShare =
P.Filepath(
- struct
- let option_name = "-aorai-test-wp-share"
- let help = "use custom wp share dir (when in internal plugin mode)"
- let arg_name = "dir"
- let existence = Filepath.Must_exist
- let file_kind = "wp share directory"
- end)
+ struct
+ let option_name = "-aorai-test-wp-share"
+ let help = "use custom wp share dir (when in internal plugin mode)"
+ let arg_name = "dir"
+ let existence = Filepath.Must_exist
+ let file_kind = "wp share directory"
+ end)
module ProveAuxSpec =
P.False(
- struct
- let option_name = "-aorai-test-prove-aux-spec"
- let help = "use WP + alt-ergo to prove that generated spec and body \
- of auxiliary automata functions match"
- end)
+ struct
+ let option_name = "-aorai-test-prove-aux-spec"
+ let help = "use WP + alt-ergo to prove that generated spec and body \
+ of auxiliary automata functions match"
+ end)
let ok = ref false
@@ -95,6 +95,7 @@ let extend () =
Project.set_current my_project;
Kernel.SymbolicPath.add ("TMPDIR:"^Filename.get_temp_dir_name());
Files.append_after [ Filepath.Normalized.of_string tmpfile ];
+ Kernel.LogicalOperators.on ();
Constfold.off ();
Ast.compute();
if ProveAuxSpec.get () then 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 43f443e26e9..af9bc71a2b3 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
@@ -52,9 +52,8 @@ 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_tmp = 1;
- else
- if (accept_S1 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
+ if (T0_S2 == 1 || 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;
@@ -159,9 +158,7 @@ int a(void)
accept_S1_tmp = accept_S1;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1) T0_S2_tmp = 1;
- else
- if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1 || 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 31031e82bb4..9da27b6622e 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
@@ -271,12 +271,10 @@ int commit_trans(void)
accept_S4_tmp = accept_S4;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
- if (accept_S2 == 1)
- if (status != 0) accept_S4_tmp = 1; else accept_S4_tmp = 0;
+ if (accept_S2 == 1 && status != 0) accept_S4_tmp = 1;
else accept_S4_tmp = 0;
accept_S3_tmp = 0;
- if (accept_S2 == 1)
- if (status == 0) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+ if (accept_S2 == 1 && status == 0) accept_S2_tmp = 1;
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 e2122593e23..3b6f510bb85 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
@@ -144,9 +144,7 @@ int rr = 1;
accept_all_tmp = 0;
accept_S5_tmp = 0;
accept_S4_tmp = 0;
- if (T0_S2 == 1)
- if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
- else accept_S3_tmp = 0;
+ if (T0_S2 == 1 && rr == 51) accept_S3_tmp = 1; 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 44c7d11061b..0e2861364d6 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
@@ -236,9 +236,7 @@ void opa(void)
accept_S3_tmp = accept_S3;
accept_all_tmp = accept_all;
accept_all_tmp = 0;
- if (T1_S2 == 1)
- if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
- else accept_S3_tmp = 0;
+ if (T1_S2 == 1 && rr == 51) accept_S3_tmp = 1; 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 41a681dcff8..384591685af 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
@@ -217,9 +217,8 @@ 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_tmp = 1;
- else
- if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+ if (accept_S1 == 1 || 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;
@@ -266,12 +265,10 @@ 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_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;
+ 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;
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 2a45f6df9a0..fd43837e998 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,11 +106,7 @@ int global_argc = 0;
accept_T2_tmp = 0;
T1_tmp = 0;
T0_init_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;
+ if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; 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 741ab2d5228..a40a3eae304 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,11 +106,7 @@ int global_argc = 0;
accept_T2_tmp = 0;
T1_tmp = 0;
T0_init_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;
+ if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
T0_init = T0_init_tmp;
T1 = T1_tmp;
@@ -419,9 +415,7 @@ int sumOne(char *t, int length)
T0_init_tmp = T0_init;
T1_tmp = T1;
accept_T2_tmp = accept_T2;
- if (T1 == 1)
- if (res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
- else accept_T2_tmp = 0;
+ if (T1 == 1 && res == 1) accept_T2_tmp = 1; 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 98fef42772d..d81509eb536 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
@@ -58,9 +58,7 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1) T0_S2_tmp = 1;
- else
- if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1 || 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;
@@ -249,14 +247,10 @@ 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_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;
+ 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;
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 4666520a57e..5cc019fcad4 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,9 +58,7 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1) T0_S2_tmp = 1;
- else
- if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1 || 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;
@@ -247,14 +245,10 @@ 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_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;
+ 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;
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 95252b378b3..0fb781bb704 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,9 +58,7 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1) T0_S2_tmp = 1;
- else
- if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1 || 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;
@@ -254,14 +252,10 @@ 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_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;
+ 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;
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/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 8e648b2ea61..6b9c9095bc9 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -107,14 +107,9 @@ check lemma S0_deterministic_trans{L}:
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
- if (3 == aorai_CurStates) {
- if (x == 4) aorai_CurStates = S4; else goto _LAND;
- }
- else {
- _LAND: ;
- if (3 == aorai_CurStates)
- if (x == 5) aorai_CurStates = S5;
- }
+ if (3 == aorai_CurStates && x == 4) aorai_CurStates = S4;
+ else
+ if (3 == aorai_CurStates && x == 5) aorai_CurStates = S5;
return;
}
@@ -231,8 +226,7 @@ void g(int x)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- if (1 == aorai_CurStates)
- if (x == 4) aorai_CurStates = S3;
+ if (1 == aorai_CurStates && x == 4) aorai_CurStates = S3;
return;
}
@@ -278,9 +272,7 @@ void g(int x)
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- if (1 == aorai_CurStates)
- if (res == 0)
- if (X == 5) aorai_CurStates = S2;
+ if (1 == aorai_CurStates && (res == 0 && X == 5)) aorai_CurStates = S2;
return;
}
@@ -351,14 +343,9 @@ int f(int x)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_real_main;
- if (0 == aorai_CurStates) {
- if (c != 0) aorai_CurStates = S1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (0 == aorai_CurStates)
- if (c == 0) aorai_CurStates = S2;
- }
+ if (0 == aorai_CurStates && c != 0) aorai_CurStates = S1;
+ else
+ if (0 == aorai_CurStates && c == 0) aorai_CurStates = S2;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 0b99905eb22..52323f131b7 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -132,21 +132,15 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- if (7 == aorai_CurStates) {
- if (x == 1) {
- aorai_CurStates = aorai_intermediate_state;
- aorai_x = x;
- }
- else goto _LAND;
- }
- else {
- _LAND: ;
- if (7 == aorai_CurStates)
- if (x == 3) {
- aorai_CurStates = aorai_intermediate_state_2;
- aorai_x_0 = x;
- }
+ 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;
+ }
return;
}
@@ -219,28 +213,13 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- if (4 == aorai_CurStates) {
- if (aorai_x_0 == 3) aorai_CurStates = OK; else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- if (1 == aorai_CurStates) {
- if (aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
- else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (4 == aorai_CurStates) {
- if (aorai_x_0 != 3) aorai_CurStates = aorai_reject;
- else goto _LAND;
- }
- else {
- _LAND: ;
- if (1 == aorai_CurStates)
- if (aorai_x != 1) aorai_CurStates = aorai_reject;
- }
- }
- }
+ 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;
return;
}
@@ -438,18 +417,13 @@ int f(int x)
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
- if (3 == aorai_CurStates) {
- if (aorai_y == 2) aorai_CurStates = OK; else goto _LAND;
- }
- else {
- _LAND: ;
+ if (3 == aorai_CurStates && aorai_y == 2) aorai_CurStates = OK;
+ else
if (0 == aorai_CurStates) aorai_CurStates = OK;
else
if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
else
- if (3 == aorai_CurStates)
- if (aorai_y != 2) aorai_CurStates = aorai_reject;
- }
+ if (3 == aorai_CurStates && aorai_y != 2) 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 ebd409ed392..ea603b7e865 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -315,14 +315,10 @@ 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)
- if (c <= 0) aorai_intermediate_state_0_tmp = 1;
- else aorai_intermediate_state_0_tmp = 0;
+ if (S0 == 1 && c <= 0) aorai_intermediate_state_0_tmp = 1;
else aorai_intermediate_state_0_tmp = 0;
bhv_aux = main_bhv_bhv(c);
- if (S0 == 1)
- if (bhv_aux) aorai_intermediate_state_tmp = 1;
- else aorai_intermediate_state_tmp = 0;
+ if (S0 == 1 && bhv_aux) aorai_intermediate_state_tmp = 1;
else aorai_intermediate_state_tmp = 0;
Sf_tmp = 0;
S0_tmp = 0;
@@ -410,25 +406,17 @@ 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_reject_tmp = 1;
- else
- if (aorai_intermediate_state_2 == 1) {
- if (res != 0) aorai_reject_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (aorai_reject == 1) aorai_reject_tmp = 1;
- else aorai_reject_tmp = 0;
- }
+ 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;
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) Sf_tmp = 1;
- else
- if (aorai_intermediate_state_2 == 1)
- if (res == 0) Sf_tmp = 1; else Sf_tmp = 0;
- else Sf_tmp = 0;
+ if (aorai_intermediate_state == 1 || aorai_intermediate_state_2 == 1 &&
+ res == 0) 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/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
index 8057befb9f5..ccc98a41d83 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -95,14 +95,10 @@ 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_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_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_counter = 1;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
@@ -543,9 +539,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) Sf_tmp = 1;
- else
- if (aorai_intermediate_state_0 == 1) Sf_tmp = 1; else Sf_tmp = 0;
+ if (aorai_intermediate_state == 1 || 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 b464e8baf7b..39843d1a28e 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -338,8 +338,7 @@ void g(void)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_h;
- if (4 == aorai_CurStates)
- if (aorai_x > 0) aorai_CurStates = f_0;
+ if (4 == aorai_CurStates && aorai_x > 0) aorai_CurStates = f_0;
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 fb6b465a225..1d964840b06 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -39,9 +39,7 @@ enum aorai_OpStatusList {
aorai_CurOperation = op_f;
S0_tmp = S0;
Sf_tmp = Sf;
- if (S0 == 1)
- if (x >= 4) Sf_tmp = 1; else Sf_tmp = 0;
- else Sf_tmp = 0;
+ if (S0 == 1 && x >= 4) 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/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
index 80809ada84f..8f230ecadb2 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -65,42 +65,13 @@ int x = 0;
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (last == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- 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 _LAND_1;
- }
- else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- 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 _LAND_2;
- }
- else {
- _LAND_2: ;
- if (last == 1)
- if (x == 4) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
- }
+ 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;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -157,42 +128,13 @@ int x = 0;
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (last == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- 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 _LAND_1;
- }
- else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- 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 _LAND_2;
- }
- else {
- _LAND_2: ;
- if (last == 1)
- if (x == 4) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
- }
+ 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;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -313,42 +255,13 @@ void f(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (last == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- 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 _LAND_1;
- }
- else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- 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 _LAND_2;
- }
- else {
- _LAND_2: ;
- if (last == 1)
- if (x == 4) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
- }
+ 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;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -405,42 +318,13 @@ void f(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (last == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- 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 _LAND_1;
- }
- else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- 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 _LAND_2;
- }
- else {
- _LAND_2: ;
- if (last == 1)
- if (x == 4) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
- }
+ 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;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -548,13 +432,9 @@ void g(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1)
- if (x == 3) step1_tmp = 1; else step1_tmp = 0;
- else step1_tmp = 0;
+ if (init == 1 && x == 3) step1_tmp = 1; else step1_tmp = 0;
last_tmp = 0;
- if (init == 1)
- if (x != 3) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
+ if (init == 1 && x != 3) init_tmp = 1; else init_tmp = 0;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -611,42 +491,13 @@ void g(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (last == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- 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 _LAND_1;
- }
- else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- 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 _LAND_2;
- }
- else {
- _LAND_2: ;
- if (last == 1)
- if (x == 4) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
- }
+ 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;
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 b8816b350cc..506dca121a3 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -278,16 +278,10 @@ 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_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 == 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_0 == 1) aorai_counter = 1;
if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_2_tmp = 0;
@@ -568,8 +562,7 @@ 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)
- if (1 <= aorai_counter) Sf_tmp = 1; else Sf_tmp = 0;
+ if (aorai_intermediate_state_2 == 1 && 1 <= aorai_counter) Sf_tmp = 1;
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 51f26c9c67f..91097fdf88b 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -95,14 +95,10 @@ 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_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_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_counter = 1;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
@@ -543,9 +539,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) Sf_tmp = 1;
- else
- if (aorai_intermediate_state_0 == 1) Sf_tmp = 1; else Sf_tmp = 0;
+ if (aorai_intermediate_state == 1 || 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/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index ee706aca96d..6ca094fa00c 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -204,8 +204,7 @@ void push(void)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_pop;
- if (3 == aorai_CurStates)
- if (aorai_n > 0) aorai_CurStates = emptying_stack;
+ if (3 == aorai_CurStates && aorai_n > 0) aorai_CurStates = emptying_stack;
return;
}
@@ -258,21 +257,15 @@ void push(void)
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_pop;
- if (2 == aorai_CurStates) {
- if (aorai_n == 1) {
- aorai_CurStates = empty_stack;
+ if (2 == aorai_CurStates && aorai_n == 1) {
+ aorai_CurStates = empty_stack;
+ aorai_n --;
+ }
+ else
+ if (2 == aorai_CurStates && aorai_n > 1) {
+ aorai_CurStates = filled_stack;
aorai_n --;
}
- else goto _LAND;
- }
- else {
- _LAND: ;
- if (2 == aorai_CurStates)
- if (aorai_n > 1) {
- aorai_CurStates = filled_stack;
- aorai_n --;
- }
- }
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 2f0841a2100..89553036d1a 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,9 +76,7 @@ int rr = 1;
SF_tmp = 0;
S4_tmp = 0;
S3_tmp = 0;
- if (S1 == 1)
- if (i >= 0) S2_tmp = 1; else S2_tmp = 0;
- else S2_tmp = 0;
+ if (S1 == 1 && i >= 0) S2_tmp = 1; else S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
@@ -293,9 +291,7 @@ void opa(int i, int j)
SF_tmp = SF;
mainst_tmp = mainst;
mainst_tmp = 0;
- if (S4 == 1)
- if (res > 0) SF_tmp = 1; else SF_tmp = 0;
- else SF_tmp = 0;
+ if (S4 == 1 && res > 0) SF_tmp = 1; 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 14191d7f00b..16997723976 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,9 +82,7 @@ int rr = 1;
S6_tmp = 0;
S5_tmp = 0;
S4_tmp = 0;
- if (S2 == 1)
- if (r >= 0) S3_tmp = 1; else S3_tmp = 0;
- else S3_tmp = 0;
+ if (S2 == 1 && r >= 0) S3_tmp = 1; else S3_tmp = 0;
S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
@@ -156,9 +154,7 @@ int rr = 1;
S7_tmp = 0;
S6_tmp = 0;
S5_tmp = 0;
- if (S3 == 1)
- if (res <= 5000) S4_tmp = 1; else S4_tmp = 0;
- else S4_tmp = 0;
+ if (S3 == 1 && res <= 5000) S4_tmp = 1; 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 862eecf00b3..6bd1a0b39b8 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
@@ -97,13 +97,9 @@ enum aorai_OpStatusList {
End_tmp = End;
Idle_tmp = Idle;
WillDoFoo_tmp = WillDoFoo;
- if (Idle == 1)
- if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
- else WillDoFoo_tmp = 0;
+ if (Idle == 1 && res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
Idle_tmp = 0;
- if (Idle == 1)
- if (res != -1) End_tmp = 1; else End_tmp = 0;
- else End_tmp = 0;
+ if (Idle == 1 && res != -1) End_tmp = 1; 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 d3c59bb4bef..43699ce9ec7 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -216,9 +216,7 @@ int decode_int(char *s)
S2_tmp = S2;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1) S2_tmp = 1;
- else
- if (S2 == 1) S2_tmp = 1; else S2_tmp = 0;
+ if (S1 == 1 || S2 == 1) S2_tmp = 1; else S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
@@ -264,12 +262,8 @@ int decode_int(char *s)
S2_tmp = S2;
main_0_tmp = main_0;
main_0_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;
+ if (S1 == 1 || S2 == 1) S2_tmp = 1; else S2_tmp = 0;
+ if (S1 == 1 || 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 6652049d8dd..cdfe4aba74b 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -100,25 +100,11 @@ enum aorai_OpStatusList {
End_tmp = End;
Idle_tmp = Idle;
WillDoFoo_tmp = WillDoFoo;
- if (Idle == 1) {
- if (res == -1) WillDoFoo_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (WillDoFoo == 1)
- if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
- else WillDoFoo_tmp = 0;
- }
+ if (Idle == 1 && res == -1 || WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1;
+ else WillDoFoo_tmp = 0;
Idle_tmp = 0;
- if (End == 1) {
- if (res != -1) End_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (Idle == 1)
- if (res != -1) End_tmp = 1; else End_tmp = 0;
- else End_tmp = 0;
- }
+ if (End == 1 && res != -1 || Idle == 1 && res != -1) End_tmp = 1;
+ 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 05996188970..bc9334eec11 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -123,24 +123,10 @@ enum aorai_OpStatusList {
Idle_tmp = Idle;
IgnoreFoo_tmp = IgnoreFoo;
WillDoFoo_tmp = WillDoFoo;
- if (Idle == 1) {
- if (res == -1) WillDoFoo_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- 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 _LAND_0;
- }
- else {
- _LAND_0: ;
- if (IgnoreFoo == 1)
- if (res != -1) IgnoreFoo_tmp = 1; else IgnoreFoo_tmp = 0;
- else IgnoreFoo_tmp = 0;
- }
+ 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;
Idle_tmp = 0;
End_tmp = 0;
End = End_tmp;
@@ -292,14 +278,11 @@ int isPresentRec(int *t, int i, int max, int val)
Idle_tmp = Idle;
IgnoreFoo_tmp = IgnoreFoo;
WillDoFoo_tmp = WillDoFoo;
- if (WillDoFoo == 1)
- if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
+ if (WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1;
else WillDoFoo_tmp = 0;
IgnoreFoo_tmp = 0;
Idle_tmp = 0;
- if (IgnoreFoo == 1)
- if (res != -1) End_tmp = 1; else End_tmp = 0;
- else End_tmp = 0;
+ if (IgnoreFoo == 1 && res != -1) End_tmp = 1; 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 0916e902014..0e102ceda96 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -47,9 +47,7 @@ int myAge = 0;
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1)
- if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
- else S1_tmp = 0;
+ if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
@@ -84,9 +82,7 @@ int myAge = 0;
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1)
- if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
- else S1_tmp = 0;
+ if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
@@ -138,9 +134,7 @@ void increment(void)
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (main_0 == 1)
- if (nobody.Age == 0) S1_tmp = 1; else S1_tmp = 0;
- else S1_tmp = 0;
+ if (main_0 == 1 && nobody.Age == 0) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
@@ -175,9 +169,7 @@ void increment(void)
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1)
- if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
- else S1_tmp = 0;
+ if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
--
GitLab