[tests] add JFLA'15 example

src/plugins/e-acsl/tests/gmp/arith.i

 /* 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;
 }

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

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;
 }

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;
 }