Merge branch 'bugfix/julien/unary_minus' into 'master'

Fix a pair of bugs in the type system

See merge request !105

src/plugins/e-acsl/doc/Changelog

@@ -15,6 +15,12 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2017/01/23] Fix bug #2252 about pointer arithmetic with
+	        negative offsets.
+-* E-ACSL       [2017/01/23] Fix bug with typing of unary and binary
+	        operations in a few cases: the generated code might have
+	        overflowed.
+
 #########################
 Plugin E-ACSL 0.8 Silicon
 #########################

src/plugins/e-acsl/tests/bts/bts2252.c

@@ -2,12 +2,24 @@
    COMMENT: bts #2252, failures due to typing of offsets
 */
 
-int *p;
-int main(void) {
-  int i = -1;
-  int t[10];
-  /*@ assert ! \valid_read(t+i); */
-  p = t;
-  /*@ assert ! \valid_read(p+i); */
-  return 0;
+#include <stdlib.h>
+
+int main() {
+  char* srcbuf = "Test Code";
+  int i, loc = 1;
+
+  char * destbuf = (char*)malloc(10*sizeof(char));
+  char ch = 'o';
+
+  if (destbuf != NULL) {
+    for (i = -1; i < 0; i++) {
+      /*@ assert ! \valid_read(srcbuf + i); */
+      if (srcbuf[i] == ch) { /* ERROR: Buffer Underrun */
+        loc = i;
+      }
+    }
+
+    strncpy (&destbuf[loc], &srcbuf[loc], 1);
+    free(destbuf);
+  }
 }

src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle

+tests/bts/bts2252.c:22:[kernel] warning: Calling undeclared function strncpy. Old style K&R code?
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/bts/bts2252.c:17:[value] warning: out of bounds read. assert \valid_read(srcbuf + i);

src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c

@@ -92,25 +92,25 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
                     (char *)"atp_NORMAL_computeAverageAccel",
                     (char *)"mem_access: \\valid_read((int *)*__gen_e_acsl_at_6)",
                     8);
-    __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_5)[1L]),
+    __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_5)[1]),
                                                     sizeof(int));
     __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
                     (char *)"atp_NORMAL_computeAverageAccel",
                     (char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_5)[1])",
                     8);
-    __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_4)[2L]),
+    __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_4)[2]),
                                                     sizeof(int));
     __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
                     (char *)"atp_NORMAL_computeAverageAccel",
                     (char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_4)[2])",
                     8);
-    __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_3)[3L]),
+    __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_3)[3]),
                                                     sizeof(int));
     __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
                     (char *)"atp_NORMAL_computeAverageAccel",
                     (char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_3)[3])",
                     8);
-    __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_2)[4L]),
+    __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_2)[4]),
                                                     sizeof(int));
     __e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",
                     (char *)"atp_NORMAL_computeAverageAccel",
@@ -121,7 +121,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
     __e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",
                     (char *)"atp_NORMAL_computeAverageAccel",
                     (char *)"mem_access: \\valid_read(__gen_e_acsl_at)",8);
-    __e_acsl_assert(*__gen_e_acsl_at == (int)((((((*__gen_e_acsl_at_2)[4L] + (*__gen_e_acsl_at_3)[3L]) + (*__gen_e_acsl_at_4)[2L]) + (*__gen_e_acsl_at_5)[1L]) + (*__gen_e_acsl_at_6)[0L]) / 5L),
+    __e_acsl_assert(*__gen_e_acsl_at == (int)((((((*__gen_e_acsl_at_2)[4] + (long)(*__gen_e_acsl_at_3)[3]) + (*__gen_e_acsl_at_4)[2]) + (*__gen_e_acsl_at_5)[1]) + (*__gen_e_acsl_at_6)[0]) / 5L),
                     (char *)"Postcondition",
                     (char *)"atp_NORMAL_computeAverageAccel",
                     (char *)"*\\old(AverageAccel) ==\n(((((*\\old(Accel))[4] + (*\\old(Accel))[3]) + (*\\old(Accel))[2]) +\n  (*\\old(Accel))[1])\n + (*\\old(Accel))[0])\n/ 5",

src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c

@@ -35,11 +35,11 @@ int main(int argc, char **argv)
     {
       int __gen_e_acsl_initialized;
       int __gen_e_acsl_and;
-      __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& _G[0L].str),
+      __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& _G[0].str),
                                                       sizeof(char *));
       if (__gen_e_acsl_initialized) {
         int __gen_e_acsl_valid_read;
-        __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_G[0L].str,
+        __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_G[0].str,
                                                       sizeof(char));
         __gen_e_acsl_and = __gen_e_acsl_valid_read;
       }

src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c

 /* Generated by Frama-C */
-int *p;
+char *__gen_e_acsl_literal_string;
+/*@ assigns \result, *(x_0 + (0 ..)), *(x_1 + (0 ..));
+    assigns \result \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2;
+    assigns *(x_0 + (0 ..)) \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2;
+    assigns *(x_1 + (0 ..)) \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2;
+ */
+extern int ( /* missing proto */ strncpy)(char *x_0, char *x_1, int x_2);
+
 void __e_acsl_globals_init(void)
 {
-  __e_acsl_store_block((void *)(& p),8UL);
-  __e_acsl_full_init((void *)(& p));
+  __gen_e_acsl_literal_string = "Test Code";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+                       sizeof("Test Code"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+  __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
   return;
 }
 
 int main(void)
 {
   int __retres;
+  char *srcbuf;
   int i;
-  int t[10];
+  int loc;
+  char *destbuf;
+  char ch;
   __e_acsl_memory_init((int *)0,(char ***)0,8UL);
   __e_acsl_globals_init();
-  __e_acsl_store_block((void *)(t),40UL);
-  i = -1;
-  /*@ assert ¬\valid_read(&t[i]); */
-  {
-    {
-      int __gen_e_acsl_valid_read;
-      __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& t[i]),
-                                                    sizeof(int));
-      __e_acsl_assert(! __gen_e_acsl_valid_read,(char *)"Assertion",
-                      (char *)"main",(char *)"!\\valid_read(&t[i])",9);
-    }
-  }
-  p = t;
-  /*@ assert ¬\valid_read(p + i); */
-  {
-    {
-      int __gen_e_acsl_valid_read_2;
-      __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + i),
-                                                      sizeof(int));
-      __e_acsl_assert(! __gen_e_acsl_valid_read_2,(char *)"Assertion",
-                      (char *)"main",(char *)"!\\valid_read(p + i)",11);
+  __e_acsl_store_block((void *)(& srcbuf),8UL);
+  __e_acsl_full_init((void *)(& srcbuf));
+  srcbuf = (char *)__gen_e_acsl_literal_string;
+  loc = 1;
+  destbuf = (char *)malloc((unsigned long)10 * sizeof(char));
+  ch = (char)'o';
+  if (destbuf != (char *)0) {
+    i = -1;
+    while (i < 0) {
+      /*@ assert ¬\valid_read(srcbuf + i); */
+      {
+        {
+          int __gen_e_acsl_valid_read;
+          __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(srcbuf + i),
+                                                        sizeof(char));
+          __e_acsl_assert(! __gen_e_acsl_valid_read,(char *)"Assertion",
+                          (char *)"main",(char *)"!\\valid_read(srcbuf + i)",
+                          16);
+        }
+      }
+      /*@ assert Value: mem_access: \valid_read(srcbuf + i); */
+      if ((int)*(srcbuf + i) == (int)ch) loc = i;
+      i ++;
     }
+    strncpy(destbuf + loc,srcbuf + loc,1);
+    free((void *)destbuf);
   }
   __retres = 0;
-  __e_acsl_delete_block((void *)(& p));
-  __e_acsl_delete_block((void *)(t));
+  __e_acsl_delete_block((void *)(& srcbuf));
   __e_acsl_memory_clean();
   return __retres;
 }

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

@@ -33,5 +33,7 @@ int main(void) {
   // example from the JFLA'15 paper (but for a 64-bit architecture)
   /*@ assert 1 + ((z+1) / (y-123456789123456789)) == 1; */
 
+  /*@ assert 1 - x == -x + 1; */ // test GIT issue #37
+
   return 0;
 }

src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c

@@ -69,7 +69,7 @@ int main(void)
   __e_acsl_assert(3 % -2 == 1,(char *)"Assertion",(char *)"main",
                   (char *)"3 % -2 == 1",21);
   /*@ assert ((x * 2 + (3 + y)) - 4) + (x - y) ≡ -10; */
-  __e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - y) == -10,
+  __e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - (long)y) == -10,
                   (char *)"Assertion",(char *)"main",
                   (char *)"((x * 2 + (3 + y)) - 4) + (x - y) == -10",23);
   /*@ assert (0 ≡ 1) ≡ !(0 ≡ 0); */
@@ -140,6 +140,9 @@ int main(void)
       __gmpz_clear(__gen_e_acsl_div_2);
     }
   }
+  /*@ assert 1 - x ≡ -x + 1; */
+  __e_acsl_assert(1L - x == - ((long)x) + 1L,(char *)"Assertion",
+                  (char *)"main",(char *)"1 - x == -x + 1",36);
   __retres = 0;
   return __retres;
 }

src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c

@@ -688,6 +688,39 @@ int main(void)
       __gmpz_clear(__gen_e_acsl_add_6);
     }
   }
+  /*@ assert 1 - x ≡ -x + 1; */
+  {
+    {
+      __e_acsl_mpz_t __gen_e_acsl__60;
+      __e_acsl_mpz_t __gen_e_acsl_x_9;
+      __e_acsl_mpz_t __gen_e_acsl_sub_5;
+      __e_acsl_mpz_t __gen_e_acsl_neg_15;
+      __e_acsl_mpz_t __gen_e_acsl_add_7;
+      int __gen_e_acsl_eq_21;
+      __gmpz_init_set_si(__gen_e_acsl__60,1L);
+      __gmpz_init_set_si(__gen_e_acsl_x_9,(long)x);
+      __gmpz_init(__gen_e_acsl_sub_5);
+      __gmpz_sub(__gen_e_acsl_sub_5,
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__60),
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_9));
+      __gmpz_init(__gen_e_acsl_neg_15);
+      __gmpz_neg(__gen_e_acsl_neg_15,
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_9));
+      __gmpz_init(__gen_e_acsl_add_7);
+      __gmpz_add(__gen_e_acsl_add_7,
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_15),
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__60));
+      __gen_e_acsl_eq_21 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_5),
+                                      (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
+      __e_acsl_assert(__gen_e_acsl_eq_21 == 0,(char *)"Assertion",
+                      (char *)"main",(char *)"1 - x == -x + 1",36);
+      __gmpz_clear(__gen_e_acsl__60);
+      __gmpz_clear(__gen_e_acsl_x_9);
+      __gmpz_clear(__gen_e_acsl_sub_5);
+      __gmpz_clear(__gen_e_acsl_neg_15);
+      __gmpz_clear(__gen_e_acsl_add_7);
+    }
+  }
   __retres = 0;
   return __retres;
 }

src/plugins/e-acsl/tests/gmp/oracle/gen_at.c

@@ -113,7 +113,7 @@ int h(int x)
 
 int main(void)
 {
-  int __gen_e_acsl_at_3;
+  long __gen_e_acsl_at_3;
   long __gen_e_acsl_at_2;
   int __gen_e_acsl_at;
   int __retres;
@@ -125,7 +125,7 @@ int main(void)
   __e_acsl_full_init((void *)(& x));
   x = __gen_e_acsl_h(0);
   L:
-    __gen_e_acsl_at_3 = x;
+    __gen_e_acsl_at_3 = (long)x;
     __gen_e_acsl_at_2 = x + 1L;
     __gen_e_acsl_at = x;
     /*@ assert x ≡ 0; */

src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c

@@ -51,7 +51,7 @@ int main(void)
     {
       void *__gen_e_acsl_base_addr_3;
       void *__gen_e_acsl_base_addr_4;
-      __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[3L]));
+      __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[3]));
       __gen_e_acsl_base_addr_4 = __e_acsl_base_addr((void *)PA);
       __e_acsl_assert(__gen_e_acsl_base_addr_3 == __gen_e_acsl_base_addr_4,
                       (char *)"Assertion",(char *)"main",
@@ -76,8 +76,8 @@ int main(void)
     {
       void *__gen_e_acsl_base_addr_7;
       void *__gen_e_acsl_base_addr_8;
-      __gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + 2L));
-      __gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[3L]));
+      __gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + 2));
+      __gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[3]));
       __e_acsl_assert(__gen_e_acsl_base_addr_7 == __gen_e_acsl_base_addr_8,
                       (char *)"Assertion",(char *)"main",
                       (char *)"\\base_addr(PA + 2) == \\base_addr(&A[3])",17);
@@ -110,7 +110,7 @@ int main(void)
     {
       void *__gen_e_acsl_base_addr_11;
       void *__gen_e_acsl_base_addr_12;
-      __gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[3L]));
+      __gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[3]));
       __gen_e_acsl_base_addr_12 = __e_acsl_base_addr((void *)pa);
       __e_acsl_assert(__gen_e_acsl_base_addr_11 == __gen_e_acsl_base_addr_12,
                       (char *)"Assertion",(char *)"main",
@@ -136,7 +136,7 @@ int main(void)
     {
       void *__gen_e_acsl_base_addr_15;
       void *__gen_e_acsl_base_addr_16;
-      __gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + 2L));
+      __gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + 2));
       __gen_e_acsl_base_addr_16 = __e_acsl_base_addr((void *)(a));
       __e_acsl_assert(__gen_e_acsl_base_addr_15 == __gen_e_acsl_base_addr_16,
                       (char *)"Assertion",(char *)"main",
@@ -165,7 +165,7 @@ int main(void)
     {
       void *__gen_e_acsl_base_addr_19;
       void *__gen_e_acsl_base_addr_20;
-      __gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + 2L));
+      __gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + 2));
       __gen_e_acsl_base_addr_20 = __e_acsl_base_addr((void *)(& l));
       __e_acsl_assert(__gen_e_acsl_base_addr_19 == __gen_e_acsl_base_addr_20,
                       (char *)"Assertion",(char *)"main",
@@ -223,8 +223,8 @@ int main(void)
     {
       void *__gen_e_acsl_base_addr_27;
       void *__gen_e_acsl_base_addr_28;
-      __gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + 1L));
-      __gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + 5L));
+      __gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + 1));
+      __gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + 5));
       __e_acsl_assert(__gen_e_acsl_base_addr_27 == __gen_e_acsl_base_addr_28,
                       (char *)"Assertion",(char *)"main",
                       (char *)"\\base_addr(p + 1) == \\base_addr(pd + 5)",45);
@@ -235,8 +235,8 @@ int main(void)
     {
       void *__gen_e_acsl_base_addr_29;
       void *__gen_e_acsl_base_addr_30;
-      __gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + 11L));
-      __gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + 1L));
+      __gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + 11));
+      __gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + 1));
       __e_acsl_assert(__gen_e_acsl_base_addr_29 == __gen_e_acsl_base_addr_30,
                       (char *)"Assertion",(char *)"main",
                       (char *)"\\base_addr(p + 11) == \\base_addr(pd + 1)",
@@ -250,7 +250,7 @@ int main(void)
     {
       void *__gen_e_acsl_base_addr_31;
       void *__gen_e_acsl_base_addr_32;
-      __gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + 5L));
+      __gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + 5));
       __gen_e_acsl_base_addr_32 = __e_acsl_base_addr((void *)pd);
       __e_acsl_assert(__gen_e_acsl_base_addr_31 == __gen_e_acsl_base_addr_32,
                       (char *)"Assertion",(char *)"main",
@@ -262,7 +262,7 @@ int main(void)
     {
       void *__gen_e_acsl_base_addr_33;
       void *__gen_e_acsl_base_addr_34;
-      __gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - 5L));
+      __gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - 5));
       __gen_e_acsl_base_addr_34 = __e_acsl_base_addr((void *)pd);
       __e_acsl_assert(__gen_e_acsl_base_addr_33 == __gen_e_acsl_base_addr_34,
                       (char *)"Assertion",(char *)"main",

src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c

@@ -71,7 +71,7 @@ int main(void)
   {
     {
       unsigned long __gen_e_acsl_block_length_4;
-      __gen_e_acsl_block_length_4 = __e_acsl_block_length((void *)(& A[3L]));
+      __gen_e_acsl_block_length_4 = __e_acsl_block_length((void *)(& A[3]));
       __e_acsl_assert(__gen_e_acsl_block_length_4 == 16,(char *)"Assertion",
                       (char *)"main",
                       (char *)"\\block_length(&A[3]) == sizeof(A)",21);
@@ -93,8 +93,8 @@ int main(void)
     {
       unsigned long __gen_e_acsl_block_length_6;
       unsigned long __gen_e_acsl_block_length_7;
-      __gen_e_acsl_block_length_6 = __e_acsl_block_length((void *)(PA + 1L));
-      __gen_e_acsl_block_length_7 = __e_acsl_block_length((void *)(& A[1L]));
+      __gen_e_acsl_block_length_6 = __e_acsl_block_length((void *)(PA + 1));
+      __gen_e_acsl_block_length_7 = __e_acsl_block_length((void *)(& A[1]));
       __e_acsl_assert(__gen_e_acsl_block_length_6 == __gen_e_acsl_block_length_7,
                       (char *)"Assertion",(char *)"main",
                       (char *)"\\block_length(PA + 1) == \\block_length(&A[1])",
@@ -125,7 +125,7 @@ int main(void)
   {
     {
       unsigned long __gen_e_acsl_block_length_9;
-      __gen_e_acsl_block_length_9 = __e_acsl_block_length((void *)(& a[3L]));
+      __gen_e_acsl_block_length_9 = __e_acsl_block_length((void *)(& a[3]));
       __e_acsl_assert(__gen_e_acsl_block_length_9 == 16,(char *)"Assertion",
                       (char *)"main",
                       (char *)"\\block_length(&a[3]) == sizeof(a)",30);
@@ -148,8 +148,8 @@ int main(void)
     {
       unsigned long __gen_e_acsl_block_length_11;
       unsigned long __gen_e_acsl_block_length_12;
-      __gen_e_acsl_block_length_11 = __e_acsl_block_length((void *)(pa + 1L));
-      __gen_e_acsl_block_length_12 = __e_acsl_block_length((void *)(& a[1L]));
+      __gen_e_acsl_block_length_11 = __e_acsl_block_length((void *)(pa + 1));
+      __gen_e_acsl_block_length_12 = __e_acsl_block_length((void *)(& a[1]));
       __e_acsl_assert(__gen_e_acsl_block_length_11 == __gen_e_acsl_block_length_12,
                       (char *)"Assertion",(char *)"main",
                       (char *)"\\block_length(pa + 1) == \\block_length(&a[1])",
@@ -184,7 +184,7 @@ int main(void)
   {
     {
       unsigned long __gen_e_acsl_block_length_15;
-      __gen_e_acsl_block_length_15 = __e_acsl_block_length((void *)(pl + 7L));
+      __gen_e_acsl_block_length_15 = __e_acsl_block_length((void *)(pl + 7));
       __e_acsl_assert(__gen_e_acsl_block_length_15 == 8,(char *)"Assertion",
                       (char *)"main",
                       (char *)"\\block_length(pl + 7) == sizeof(long)",41);
@@ -235,7 +235,7 @@ int main(void)
   {
     {
       unsigned long __gen_e_acsl_block_length_21;
-      __gen_e_acsl_block_length_21 = __e_acsl_block_length((void *)(p + 11L));
+      __gen_e_acsl_block_length_21 = __e_acsl_block_length((void *)(p + 11));
       __e_acsl_assert(__gen_e_acsl_block_length_21 == size,
                       (char *)"Assertion",(char *)"main",
                       (char *)"\\block_length(p + 11) == size",51);
@@ -248,8 +248,8 @@ int main(void)
     {
       unsigned long __gen_e_acsl_block_length_22;
       unsigned long __gen_e_acsl_block_length_23;
-      __gen_e_acsl_block_length_22 = __e_acsl_block_length((void *)(p + 5L));
-      __gen_e_acsl_block_length_23 = __e_acsl_block_length((void *)(p - 5L));
+      __gen_e_acsl_block_length_22 = __e_acsl_block_length((void *)(p + 5));
+      __gen_e_acsl_block_length_23 = __e_acsl_block_length((void *)(p - 5));
       __e_acsl_assert(__gen_e_acsl_block_length_22 == __gen_e_acsl_block_length_23,
                       (char *)"Assertion",(char *)"main",
                       (char *)"\\block_length(p + 5) == \\block_length(p - 5)",

src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c

@@ -81,7 +81,7 @@ int main(int argc, char **argv)
                                                       sizeof(char *));
       if (__gen_e_acsl_initialized) {
         int __gen_e_acsl_valid_read;
-        __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_A[0L],
+        __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_A[0],
                                                       sizeof(char));
         __gen_e_acsl_and = __gen_e_acsl_valid_read;
       }
@@ -95,11 +95,11 @@ int main(int argc, char **argv)
     {
       int __gen_e_acsl_initialized_2;
       int __gen_e_acsl_and_2;
-      __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& _A[1L]),
+      __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& _A[1]),
                                                         sizeof(char *));
       if (__gen_e_acsl_initialized_2) {
         int __gen_e_acsl_valid_read_2;
-        __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)_A[1L],
+        __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)_A[1],
                                                         sizeof(char));
         __gen_e_acsl_and_2 = __gen_e_acsl_valid_read_2;
       }
@@ -168,7 +168,7 @@ int main(int argc, char **argv)
     }
   }
   /*@ assert _G[0].num ≡ 99; */
-  __e_acsl_assert(_G[0L].num == 99,(char *)"Assertion",(char *)"main",
+  __e_acsl_assert(_G[0].num == 99,(char *)"Assertion",(char *)"main",
                   (char *)"_G[0].num == 99",43);
   __retres = 0;
   __e_acsl_delete_block((void *)(_G));

src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c

@@ -233,11 +233,11 @@ void __gen_e_acsl_n(void)
  */
 void __gen_e_acsl_m(void)
 {
-  int __gen_e_acsl_at_4;
+  long __gen_e_acsl_at_4;
   int __gen_e_acsl_at_3;
   int __gen_e_acsl_at_2;
   int __gen_e_acsl_at;
-  __gen_e_acsl_at_4 = X;
+  __gen_e_acsl_at_4 = (long)X;
   {
     int __gen_e_acsl_and_2;
     if (X == 5) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0;
@@ -312,7 +312,7 @@ void __gen_e_acsl_k(void)
                     (char *)"k",(char *)"X == 3 && Y == 2 ==> X == 3",42);
     if (X == 3) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0;
     if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
-    else __gen_e_acsl_implies_3 = X + Y == 5L;
+    else __gen_e_acsl_implies_3 = X + (long)Y == 5L;
     __e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
                     (char *)"k",(char *)"X == 3 && Y == 2 ==> X + Y == 5",43);
     k();

src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c

@@ -170,7 +170,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_initialized_12;
-      __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& d[1L]),
+      __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& d[1]),
                                                          sizeof(long));
       __e_acsl_assert(! __gen_e_acsl_initialized_12,(char *)"Assertion",
                       (char *)"main",(char *)"!\\initialized(&d[1])",44);
@@ -200,7 +200,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_initialized_15;
-      __gen_e_acsl_initialized_15 = __e_acsl_initialized((void *)(r + 1L),
+      __gen_e_acsl_initialized_15 = __e_acsl_initialized((void *)(r + 1),
                                                          sizeof(long));
       __e_acsl_assert(! __gen_e_acsl_initialized_15,(char *)"Assertion",
                       (char *)"main",(char *)"!\\initialized(r + 1)",47);
@@ -222,7 +222,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_initialized_17;
-      __gen_e_acsl_initialized_17 = __e_acsl_initialized((void *)(& d[1L]),
+      __gen_e_acsl_initialized_17 = __e_acsl_initialized((void *)(& d[1]),
                                                          sizeof(long));
       __e_acsl_assert(! __gen_e_acsl_initialized_17,(char *)"Assertion",
                       (char *)"main",(char *)"!\\initialized(&d[1])",51);
@@ -252,7 +252,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_initialized_20;
-      __gen_e_acsl_initialized_20 = __e_acsl_initialized((void *)(r + 1L),
+      __gen_e_acsl_initialized_20 = __e_acsl_initialized((void *)(r + 1),
                                                          sizeof(long));
       __e_acsl_assert(! __gen_e_acsl_initialized_20,(char *)"Assertion",
                       (char *)"main",(char *)"!\\initialized(r + 1)",54);
@@ -274,7 +274,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_initialized_22;
-      __gen_e_acsl_initialized_22 = __e_acsl_initialized((void *)(& d[1L]),
+      __gen_e_acsl_initialized_22 = __e_acsl_initialized((void *)(& d[1]),
                                                          sizeof(long));
       __e_acsl_assert(__gen_e_acsl_initialized_22,(char *)"Assertion",
                       (char *)"main",(char *)"\\initialized(&d[1])",58);
@@ -304,7 +304,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_initialized_25;
-      __gen_e_acsl_initialized_25 = __e_acsl_initialized((void *)(r + 1L),
+      __gen_e_acsl_initialized_25 = __e_acsl_initialized((void *)(r + 1),
                                                          sizeof(long));
       __e_acsl_assert(__gen_e_acsl_initialized_25,(char *)"Assertion",
                       (char *)"main",(char *)"\\initialized(r + 1)",61);

src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c

@@ -153,13 +153,13 @@ int __gen_e_acsl_search(int elt)
     __gen_e_acsl_i = 0;
     while (1) {
       if (__gen_e_acsl_i < 9) ; else break;
-      __e_acsl_assert(__gen_e_acsl_i + 1L < 10L,(char *)"RTE",
+      __e_acsl_assert((int)(__gen_e_acsl_i + 1L) < 10,(char *)"RTE",
                       (char *)"search",
-                      (char *)"index_bound: (long)(__gen_e_acsl_i + 1) < 10",
+                      (char *)"index_bound: (int)(__gen_e_acsl_i + 1) < 10",
                       7);
-      __e_acsl_assert(0L <= __gen_e_acsl_i + 1L,(char *)"RTE",
+      __e_acsl_assert(0 <= (int)(__gen_e_acsl_i + 1L),(char *)"RTE",
                       (char *)"search",
-                      (char *)"index_bound: 0 <= (long)(__gen_e_acsl_i + 1)",
+                      (char *)"index_bound: 0 <= (int)(__gen_e_acsl_i + 1)",
                       7);
       __e_acsl_assert(__gen_e_acsl_i < 10,(char *)"RTE",(char *)"search",
                       (char *)"index_bound: __gen_e_acsl_i < 10",7);

src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c

@@ -41,7 +41,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_offset_2;
-      __gen_e_acsl_offset_2 = __e_acsl_offset((void *)(& A[3L]));
+      __gen_e_acsl_offset_2 = __e_acsl_offset((void *)(& A[3]));
       __e_acsl_assert(__gen_e_acsl_offset_2 == 12UL,(char *)"Assertion",
                       (char *)"main",(char *)"\\offset(&A[3]) == 12",14);
     }
@@ -60,7 +60,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_offset_4;
-      __gen_e_acsl_offset_4 = __e_acsl_offset((void *)(PA + 1L));
+      __gen_e_acsl_offset_4 = __e_acsl_offset((void *)(PA + 1));
       __e_acsl_assert(__gen_e_acsl_offset_4 == 8UL,(char *)"Assertion",
                       (char *)"main",(char *)"\\offset(PA + 1) == 8",17);
     }
@@ -86,7 +86,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_offset_6;
-      __gen_e_acsl_offset_6 = __e_acsl_offset((void *)(& a[1L]));
+      __gen_e_acsl_offset_6 = __e_acsl_offset((void *)(& a[1]));
       __e_acsl_assert(__gen_e_acsl_offset_6 == 4UL,(char *)"Assertion",
                       (char *)"main",(char *)"\\offset(&a[1]) == 4",22);
     }
@@ -95,7 +95,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_offset_7;
-      __gen_e_acsl_offset_7 = __e_acsl_offset((void *)(& a[3L]));
+      __gen_e_acsl_offset_7 = __e_acsl_offset((void *)(& a[3]));
       __e_acsl_assert(__gen_e_acsl_offset_7 == 12UL,(char *)"Assertion",
                       (char *)"main",(char *)"\\offset(&a[3]) == 12",23);
     }
@@ -126,7 +126,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_offset_10;
-      __gen_e_acsl_offset_10 = __e_acsl_offset((void *)(pl + 1L));
+      __gen_e_acsl_offset_10 = __e_acsl_offset((void *)(pl + 1));
       __e_acsl_assert(__gen_e_acsl_offset_10 == 1UL,(char *)"Assertion",
                       (char *)"main",(char *)"\\offset(pl + 1) == 1",30);
     }
@@ -135,7 +135,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_offset_11;
-      __gen_e_acsl_offset_11 = __e_acsl_offset((void *)(pl + 7L));
+      __gen_e_acsl_offset_11 = __e_acsl_offset((void *)(pl + 7));
       __e_acsl_assert(__gen_e_acsl_offset_11 == 7UL,(char *)"Assertion",
                       (char *)"main",(char *)"\\offset(pl + 7) == 7",31);
     }
@@ -177,7 +177,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_offset_15;
-      __gen_e_acsl_offset_15 = __e_acsl_offset((void *)(p + 1L));
+      __gen_e_acsl_offset_15 = __e_acsl_offset((void *)(p + 1));
       __e_acsl_assert(__gen_e_acsl_offset_15 == 1UL,(char *)"Assertion",
                       (char *)"main",(char *)"\\offset(p + 1) == 1",40);
     }
@@ -186,7 +186,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_offset_16;
-      __gen_e_acsl_offset_16 = __e_acsl_offset((void *)(p + 11L));
+      __gen_e_acsl_offset_16 = __e_acsl_offset((void *)(p + 11));
       __e_acsl_assert(__gen_e_acsl_offset_16 == 11UL,(char *)"Assertion",
                       (char *)"main",(char *)"\\offset(p + 11) == 11",41);
     }
@@ -197,7 +197,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_offset_17;
-      __gen_e_acsl_offset_17 = __e_acsl_offset((void *)(p + 5L));
+      __gen_e_acsl_offset_17 = __e_acsl_offset((void *)(p + 5));
       __e_acsl_assert(__gen_e_acsl_offset_17 == 10UL,(char *)"Assertion",
                       (char *)"main",(char *)"\\offset(p + 5) == 10",43);
     }
@@ -206,7 +206,7 @@ int main(void)
   {
     {
       int __gen_e_acsl_offset_18;
-      __gen_e_acsl_offset_18 = __e_acsl_offset((void *)(p - 5L));
+      __gen_e_acsl_offset_18 = __e_acsl_offset((void *)(p - 5));
       __e_acsl_assert(__gen_e_acsl_offset_18 == 0UL,(char *)"Assertion",
                       (char *)"main",(char *)"\\offset(p - 5) == 0",44);
     }

src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c

@@ -5,6 +5,7 @@ int main(void)
   int x;
   int t[3];
   int *p;
+  int k;
   __e_acsl_memory_init((int *)0,(char ***)0,8UL);
   __e_acsl_store_block((void *)(& p),8UL);
   __e_acsl_store_block((void *)(t),12UL);
@@ -39,10 +40,10 @@ int main(void)
     }
   }
   /*@ assert t[0] ≡ 2; */
-  __e_acsl_assert(t[0L] == 2,(char *)"Assertion",(char *)"main",
+  __e_acsl_assert(t[0] == 2,(char *)"Assertion",(char *)"main",
                   (char *)"t[0] == 2",12);
   /*@ assert t[2] ≡ 4; */
-  __e_acsl_assert(t[2L] == 4,(char *)"Assertion",(char *)"main",
+  __e_acsl_assert(t[2] == 4,(char *)"Assertion",(char *)"main",
                   (char *)"t[2] == 4",13);
   /*@ assert t[(2 * sizeof(int)) / sizeof((int)0x0)] ≡ 4; */
   __e_acsl_assert(t[(2 * 4) / 4] == 4,(char *)"Assertion",(char *)"main",
@@ -73,12 +74,12 @@ int main(void)
       {
         {
           int __gen_e_acsl_valid_read_2;
-          __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t[2L] - i),
+          __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t[2] - i),
                                                           sizeof(int));
           __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
                           (char *)"main",
                           (char *)"mem_access: \\valid_read(&t[2] - i)",19);
-          __e_acsl_assert(*(& t[2L] - i) == 4L - i,(char *)"Assertion",
+          __e_acsl_assert(*(& t[2] - i) == 4L - i,(char *)"Assertion",
                           (char *)"main",(char *)"*(&t[2] - i) == 4 - i",19);
         }
       }
@@ -109,6 +110,19 @@ int main(void)
                       (char *)"*p == 5",25);
     }
   }
+  k = -1;
+  /*@ assert *(p + k) ≡ 3; */
+  {
+    {
+      int __gen_e_acsl_valid_read_4;
+      __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + k),
+                                                      sizeof(int));
+      __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
+                      (char *)"mem_access: \\valid_read(p + k)",27);
+      __e_acsl_assert(*(p + k) == 3,(char *)"Assertion",(char *)"main",
+                      (char *)"*(p + k) == 3",27);
+    }
+  }
   __retres = 0;
   __e_acsl_delete_block((void *)(& p));
   __e_acsl_delete_block((void *)(t));

src/plugins/e-acsl/tests/runtime/oracle/gen_result.c

@@ -64,10 +64,10 @@ int __gen_e_acsl_g(int x)
 int __gen_e_acsl_f(int x)
 {
   int __gen_e_acsl_at_2;
-  int __gen_e_acsl_at;
+  long __gen_e_acsl_at;
   int __retres;
   __gen_e_acsl_at_2 = x;
-  __gen_e_acsl_at = x;
+  __gen_e_acsl_at = (long)x;
   __retres = f(x);
   __e_acsl_assert(__retres == (int)(__gen_e_acsl_at - __gen_e_acsl_at_2),
                   (char *)"Postcondition",(char *)"f",

src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c

@@ -87,7 +87,7 @@ int main(void)
                       37);
       if (x == 3) __gen_e_acsl_and_2 = y == 2; else __gen_e_acsl_and_2 = 0;
       if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
-      else __gen_e_acsl_implies_3 = x + y == 5L;
+      else __gen_e_acsl_implies_3 = x + (long)y == 5L;
       __e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
                       (char *)"main",
                       (char *)"x == 3 && y == 2 ==> x + y == 5",38);