From 87564b2b91865eb5c7a1b2af3a62f5982cbb57fb Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 17 Jul 2020 10:43:06 +0200
Subject: [PATCH] [eacsl] Update tests
---
.../tests/arith/oracle_ci/gen_functions.c | 84 ++++++++---------
.../tests/gmp-only/oracle_ci/gen_functions.c | 92 +++++++++----------
2 files changed, 88 insertions(+), 88 deletions(-)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
index a1227023b92..812ba798a39 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
@@ -17,10 +17,10 @@ int __gen_e_acsl_p1(int x, int y);
*/
int __gen_e_acsl_p2(int x, int y);
-int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
-
int __gen_e_acsl_p2_5(int x, long y);
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
+
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
@@ -232,56 +232,18 @@ void __gen_e_acsl_k(int x)
return;
}
-int __gen_e_acsl_g(int x)
-{
- int __gen_e_acsl_g_hidden_2;
- __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
- return __gen_e_acsl_g_hidden_2;
-}
-
-mystruct __gen_e_acsl_t1(mystruct m)
-{
- return m;
-}
-
int __gen_e_acsl_p1(int x, int y)
{
int __retres = x + (long)y > 0L;
return __retres;
}
-long __gen_e_acsl_t2(mystruct m)
-{
- long __retres = m.k + (long)m.l;
- return __retres;
-}
-
int __gen_e_acsl_p2(int x, int y)
{
int __retres = x + (long)y > 0L;
return __retres;
}
-int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_gt;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(y));
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- int __retres = __gen_e_acsl_gt > 0;
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_add);
- __gmpz_clear(__gen_e_acsl__2);
- return __retres;
-}
-
int __gen_e_acsl_p2_5(int x, long y)
{
__e_acsl_mpz_t __gen_e_acsl_x_2;
@@ -306,9 +268,23 @@ int __gen_e_acsl_p2_5(int x, long y)
return __retres;
}
-int __gen_e_acsl_k_pred(int x)
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
{
- int __retres = x > 0;
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_gt;
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ int __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl__2);
return __retres;
}
@@ -363,6 +339,30 @@ int __gen_e_acsl_g_hidden(int x)
return x;
}
+int __gen_e_acsl_g(int x)
+{
+ int __gen_e_acsl_g_hidden_2;
+ __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
+ return __gen_e_acsl_g_hidden_2;
+}
+
+mystruct __gen_e_acsl_t1(mystruct m)
+{
+ return m;
+}
+
+long __gen_e_acsl_t2(mystruct m)
+{
+ long __retres = m.k + (long)m.l;
+ return __retres;
+}
+
+int __gen_e_acsl_k_pred(int x)
+{
+ int __retres = x > 0;
+ return __retres;
+}
+
double __gen_e_acsl_f2(double x)
{
__e_acsl_mpq_t __gen_e_acsl__8;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index 0050e6edc3b..471424de4c8 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
@@ -288,18 +288,6 @@ void __gen_e_acsl_k(int x)
return;
}
-int __gen_e_acsl_g(int x)
-{
- int __gen_e_acsl_g_hidden_2;
- __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
- return __gen_e_acsl_g_hidden_2;
-}
-
-mystruct __gen_e_acsl_t1(mystruct m)
-{
- return m;
-}
-
int __gen_e_acsl_p1(int x, int y)
{
__e_acsl_mpz_t __gen_e_acsl_x;
@@ -323,25 +311,6 @@ int __gen_e_acsl_p1(int x, int y)
return __retres;
}
-void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
-{
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl__11;
- __e_acsl_mpz_t __gen_e_acsl_add_7;
- __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
- __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
- __gmpz_init(__gen_e_acsl_add_7);
- __gmpz_add(__gen_e_acsl_add_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl__11);
- __gmpz_clear(__gen_e_acsl_add_7);
- return;
-}
-
int __gen_e_acsl_p2(int x, int y)
{
__e_acsl_mpz_t __gen_e_acsl_x_2;
@@ -387,21 +356,6 @@ int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
return __retres;
}
-int __gen_e_acsl_k_pred(int x)
-{
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_gt;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- int __retres = __gen_e_acsl_gt > 0;
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_);
- return __retres;
-}
-
void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
{
__e_acsl_mpz_t __gen_e_acsl_x_4;
@@ -466,6 +420,52 @@ int __gen_e_acsl_g_hidden(int x)
return x;
}
+int __gen_e_acsl_g(int x)
+{
+ int __gen_e_acsl_g_hidden_2;
+ __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
+ return __gen_e_acsl_g_hidden_2;
+}
+
+mystruct __gen_e_acsl_t1(mystruct m)
+{
+ return m;
+}
+
+void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
+{
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ __e_acsl_mpz_t __gen_e_acsl_add_7;
+ __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
+ __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
+ __gmpz_init(__gen_e_acsl_add_7);
+ __gmpz_add(__gen_e_acsl_add_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl_add_7);
+ return;
+}
+
+int __gen_e_acsl_k_pred(int x)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_gt;
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ int __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_);
+ return __retres;
+}
+
double __gen_e_acsl_f2(double x)
{
__e_acsl_mpq_t __gen_e_acsl__13;
--
GitLab