diff --git a/src/plugins/e-acsl/tests/gmp/arith.i b/src/plugins/e-acsl/tests/gmp/arith.i
index 9b63a0fabbe6f610f8ec9ccc9effdff631584998..eed3887af85ba1a70ad066546745204144166854 100644
--- a/src/plugins/e-acsl/tests/gmp/arith.i
+++ b/src/plugins/e-acsl/tests/gmp/arith.i
@@ -1,11 +1,11 @@
/* run.config
COMMENT: arithmetic operations
- COMMENT: add the last assertion when fixing BTS #751
*/
int main(void) {
int x = -3;
int y = 2;
+ long z = 2L;
/*@ assert -3 == x; */ ;
/*@ assert x == -3; */ ;
@@ -28,7 +28,10 @@ int main(void) {
/*@ assert (0 != 1) == !(0 != 0); */ ;
/*@ assert 0 == !1; */ ;
- /*@ assert 4 / y == 2; */ /* non trivial division */
+ /*@ assert 4 / y == 2; */ // non trivial division added when fixing bts #751
+
+ // example from the JFLA'15 paper (but for a 64-bit architecture)
+ /*@ assert 1 + ((z+1) / (y-123456789123456789)) == 1; */
return 0;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
index bfaa59f349b2066e58f0714bfeadc11977a7d5a4..0ce34f18808f718cce9efe9a0aca7c6b79ffba8a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
@@ -19,4 +19,7 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: preco
[value] using specification for function __gmpz_tdiv_q
[value] using specification for function __gmpz_get_ui
[value] using specification for function __gmpz_clear
+[value] using specification for function __gmpz_init_set_si
+[value] using specification for function __gmpz_add
+tests/gmp/arith.i:34:[kernel] warning: signed overflow. assert 1+__gen_e_acsl__7 ≤ 2147483647;
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
index bde116c459b83a684781b6cd37d0475722c2efbc..edfa526c381617674a5c0cb5f1cd8f657af28dc6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
@@ -4,8 +4,10 @@ int main(void)
int __retres;
int x;
int y;
+ long z;
x = -3;
y = 2;
+ z = 2L;
/*@ assert -3 ≡ x; */
__e_acsl_assert(-3 == x,(char *)"Assertion",(char *)"main",
(char *)"-3 == x",10);
@@ -86,6 +88,44 @@ int main(void)
(char *)"division_by_zero: y != 0",31);
__e_acsl_assert(4 / y == 2,(char *)"Assertion",(char *)"main",
(char *)"4/y == 2",31);
+ /*@ assert 1+(z+1)/(y-123456789123456789) ≡ 1; */
+ {
+ mpz_t __gen_e_acsl_z;
+ mpz_t __gen_e_acsl__4;
+ mpz_t __gen_e_acsl_add;
+ mpz_t __gen_e_acsl__5;
+ mpz_t __gen_e_acsl__6;
+ int __gen_e_acsl_div_guard_2;
+ mpz_t __gen_e_acsl_div_2;
+ unsigned long __gen_e_acsl__7;
+ __gmpz_init_set_si(__gen_e_acsl_z,z);
+ __gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)1);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_z),
+ (__mpz_struct const *)(__gen_e_acsl__4));
+ __gmpz_init_set_si(__gen_e_acsl__5,y - (long)123456789123456789);
+ __gmpz_init_set_ui(__gen_e_acsl__6,0UL);
+ __gen_e_acsl_div_guard_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__5),
+ (__mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init(__gen_e_acsl_div_2);
+ /*@ assert E_ACSL: y-123456789123456789 ≢ 0; */
+ __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),(char *)"Assertion",
+ (char *)"main",(char *)"y-123456789123456789 == 0",34);
+ __gmpz_tdiv_q(__gen_e_acsl_div_2,
+ (__mpz_struct const *)(__gen_e_acsl_add),
+ (__mpz_struct const *)(__gen_e_acsl__5));
+ __gen_e_acsl__7 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_div_2));
+ /*@ assert Value: signed_overflow: 1+__gen_e_acsl__7 ≤ 2147483647; */
+ __e_acsl_assert(1 + __gen_e_acsl__7 == 1,(char *)"Assertion",
+ (char *)"main",
+ (char *)"1+(z+1)/(y-123456789123456789) == 1",34);
+ __gmpz_clear(__gen_e_acsl_z);
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_div_2);
+ }
__retres = 0;
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
index 60b90d2514d45f4bbed7018912956381db818234..877cce249c7dbead6b917302bb4bb11b8b4003ff 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
@@ -4,8 +4,10 @@ int main(void)
int __retres;
int x;
int y;
+ long z;
x = -3;
y = 2;
+ z = 2L;
/*@ assert -3 ≡ x; */
{
mpz_t __gen_e_acsl_;
@@ -565,6 +567,57 @@ int main(void)
__gmpz_clear(__gen_e_acsl_div_3);
__gmpz_clear(__gen_e_acsl__56);
}
+ /*@ assert 1+(z+1)/(y-123456789123456789) ≡ 1; */
+ {
+ mpz_t __gen_e_acsl__57;
+ mpz_t __gen_e_acsl_z;
+ mpz_t __gen_e_acsl_add_5;
+ mpz_t __gen_e_acsl_y_3;
+ mpz_t __gen_e_acsl__58;
+ mpz_t __gen_e_acsl_sub_4;
+ mpz_t __gen_e_acsl__59;
+ int __gen_e_acsl_div_guard_4;
+ mpz_t __gen_e_acsl_div_4;
+ mpz_t __gen_e_acsl_add_6;
+ int __gen_e_acsl_eq_20;
+ __gmpz_init_set_ui(__gen_e_acsl__57,(unsigned long)1);
+ __gmpz_init_set_si(__gen_e_acsl_z,z);
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,(__mpz_struct const *)(__gen_e_acsl_z),
+ (__mpz_struct const *)(__gen_e_acsl__57));
+ __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
+ __gmpz_init_set_ui(__gen_e_acsl__58,123456789123456789);
+ __gmpz_init(__gen_e_acsl_sub_4);
+ __gmpz_sub(__gen_e_acsl_sub_4,(__mpz_struct const *)(__gen_e_acsl_y_3),
+ (__mpz_struct const *)(__gen_e_acsl__58));
+ __gmpz_init_set_ui(__gen_e_acsl__59,0UL);
+ __gen_e_acsl_div_guard_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_sub_4),
+ (__mpz_struct const *)(__gen_e_acsl__59));
+ __gmpz_init(__gen_e_acsl_div_4);
+ /*@ assert E_ACSL: y-123456789123456789 ≢ 0; */
+ __e_acsl_assert(! (__gen_e_acsl_div_guard_4 == 0),(char *)"Assertion",
+ (char *)"main",(char *)"y-123456789123456789 == 0",34);
+ __gmpz_tdiv_q(__gen_e_acsl_div_4,
+ (__mpz_struct const *)(__gen_e_acsl_add_5),
+ (__mpz_struct const *)(__gen_e_acsl_sub_4));
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,(__mpz_struct const *)(__gen_e_acsl__57),
+ (__mpz_struct const *)(__gen_e_acsl_div_4));
+ __gen_e_acsl_eq_20 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_add_6),
+ (__mpz_struct const *)(__gen_e_acsl__57));
+ __e_acsl_assert(__gen_e_acsl_eq_20 == 0,(char *)"Assertion",
+ (char *)"main",
+ (char *)"1+(z+1)/(y-123456789123456789) == 1",34);
+ __gmpz_clear(__gen_e_acsl__57);
+ __gmpz_clear(__gen_e_acsl_z);
+ __gmpz_clear(__gen_e_acsl_add_5);
+ __gmpz_clear(__gen_e_acsl_y_3);
+ __gmpz_clear(__gen_e_acsl__58);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl__59);
+ __gmpz_clear(__gen_e_acsl_div_4);
+ __gmpz_clear(__gen_e_acsl_add_6);
+ }
__retres = 0;
return __retres;
}