From 4cd013c9ab68b448bf0a5aa051b1ad93d6eee686 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 15 Jun 2020 17:41:31 +0200
Subject: [PATCH] [eacsl] Update tests
---
src/plugins/e-acsl/tests/gmp-only/arith.i | 3 ++
.../tests/gmp-only/oracle_ci/arith.res.oracle | 2 +
.../tests/gmp-only/oracle_ci/gen_arith.c | 46 +++++++++++++++++++
3 files changed, 51 insertions(+)
diff --git a/src/plugins/e-acsl/tests/gmp-only/arith.i b/src/plugins/e-acsl/tests/gmp-only/arith.i
index df97877fb14..c8ebfe29294 100644
--- a/src/plugins/e-acsl/tests/gmp-only/arith.i
+++ b/src/plugins/e-acsl/tests/gmp-only/arith.i
@@ -35,5 +35,8 @@ int main(void) {
/*@ assert 1 - x == -x + 1; */ // test GIT issue #37
+ short a = 1, b = 1;
+ //@ assert a+b > 2. - 1.; // gitlab eacsl issue #120
+
return 0;
}
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
index 58ff928b06a..dcdfce7343e 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
@@ -42,3 +42,5 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp-only/arith.i:36: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:39: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
index dc901aa064e..9899c99482f 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
@@ -677,6 +677,52 @@ int main(void)
__gmpz_clear(__gen_e_acsl_add_7);
}
/*@ assert 1 - x ≡ -x + 1; */ ;
+ short a = (short)1;
+ short b = (short)1;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_a;
+ __e_acsl_mpz_t __gen_e_acsl_b;
+ __e_acsl_mpq_t __gen_e_acsl__61;
+ __e_acsl_mpq_t __gen_e_acsl__62;
+ __e_acsl_mpq_t __gen_e_acsl_add_8;
+ __e_acsl_mpq_t __gen_e_acsl__63;
+ __e_acsl_mpq_t __gen_e_acsl__64;
+ __e_acsl_mpq_t __gen_e_acsl_sub_6;
+ int __gen_e_acsl_gt_2;
+ __gmpz_init_set_si(__gen_e_acsl_a,(long)a);
+ __gmpz_init_set_si(__gen_e_acsl_b,(long)b);
+ __gmpq_init(__gen_e_acsl__61);
+ __gmpq_set_z(__gen_e_acsl__61,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_a));
+ __gmpq_init(__gen_e_acsl__62);
+ __gmpq_set_z(__gen_e_acsl__62,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_b));
+ __gmpq_init(__gen_e_acsl_add_8);
+ __gmpq_add(__gen_e_acsl_add_8,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__61),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__62));
+ __gmpq_init(__gen_e_acsl__63);
+ __gmpq_set_d(__gen_e_acsl__63,2.);
+ __gmpq_init(__gen_e_acsl__64);
+ __gmpq_set_d(__gen_e_acsl__64,1.);
+ __gmpq_init(__gen_e_acsl_sub_6);
+ __gmpq_sub(__gen_e_acsl_sub_6,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__63),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__64));
+ __gen_e_acsl_gt_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_8),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_sub_6));
+ __e_acsl_assert(__gen_e_acsl_gt_2 > 0,"Assertion","main",
+ "a + b > 2. - 1.","tests/gmp-only/arith.i",39);
+ __gmpz_clear(__gen_e_acsl_a);
+ __gmpz_clear(__gen_e_acsl_b);
+ __gmpq_clear(__gen_e_acsl__61);
+ __gmpq_clear(__gen_e_acsl__62);
+ __gmpq_clear(__gen_e_acsl_add_8);
+ __gmpq_clear(__gen_e_acsl__63);
+ __gmpq_clear(__gen_e_acsl__64);
+ __gmpq_clear(__gen_e_acsl_sub_6);
+ }
+ /*@ assert a + b > 2. - 1.; */ ;
__retres = 0;
return __retres;
}
--
GitLab