diff --git a/src/plugins/e-acsl/tests/gmp-only/arith.i b/src/plugins/e-acsl/tests/gmp-only/arith.i index df97877fb148968c52cd69013790c311dcf6160b..c8ebfe292942522f999afb4a47965af629f183cb 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 58ff928b06ae06fc7cc29f0189bd96640c51f53b..dcdfce7343e960ffd5c60c241410b9144066c9e3 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 dc901aa064e92b92e00e8c4b63a5fb05f813fca9..9899c99482fd3a9ee9baba785b2fe903ce547253 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; }