diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 8b4811dcab9a7ff97db822f5f320e5272f156ffc..846b909f021aef97bbcb0761d6dceeb906f77089 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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
#########################
diff --git a/src/plugins/e-acsl/tests/bts/bts2252.c b/src/plugins/e-acsl/tests/bts/bts2252.c
index 6b268ff1b972407ce4a818a1a12faf233318db7b..c52b56d04f0cd46500998328172f2f3c9d3c43a3 100644
--- a/src/plugins/e-acsl/tests/bts/bts2252.c
+++ b/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);
+ }
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..3e7b66c55fac4ab43c317b9b34c90f04a6ea19b8 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
@@ -1,4 +1,7 @@
+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);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index dc4cf863aa5d8da608a865a67699f723b633e52c..3b83bd403733f99d21d659c47f9f32ee69b61e5b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/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",
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
index 105c9ac89d9d0620495a481bd8670d59af91f5da..8d2fa61eada818904459b33f4e093b01fab2ab79 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index 3a492d48a045028e7511ffdd78c9d9cdf55e40d3..17547beac1f1023c14821f42b8154d44bae42d1c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -1,45 +1,61 @@
/* 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;
}
diff --git a/src/plugins/e-acsl/tests/gmp/arith.i b/src/plugins/e-acsl/tests/gmp/arith.i
index eed3887af85ba1a70ad066546745204144166854..df97877fb148968c52cd69013790c311dcf6160b 100644
--- a/src/plugins/e-acsl/tests/gmp/arith.i
+++ b/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;
}
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 56530af0d60dc28ef6da987a0b645806ae960094..c73057d06af41dc853049df7332779b0d64e0227 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
+++ b/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;
}
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 fc3b73b7c6fc4a1aa940119988e5f88abd312882..b092d8e8ad93c34d05743915c1c8681d875334af 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index 4a5071bb3d864f0ba84a6858981168053b4faeee..ff2254d54665a3f37e39f4cce403ebec896364fa 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/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; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
index 40eeac836a6012e0611a4264326e7991cc930bd7..df7cd29463475418f2c77d0c1bf1a76ed2b0cf9e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
+++ b/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",
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
index 9577c30f51b54431f7577f6869aa40bf18123be7..dd82340cf0c148636cdf682c433445d175e8ded9 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
+++ b/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)",
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
index 5987df01f5caed25468ee7cc3837ae8dbfd519ec..146ccb703bc938b54b4c9e88e97bce0fdd4f0184 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
+++ b/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));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
index 5cde7c00ea1752ff48fb5a6cab651253e8dbbeb3..a27a3104873ffe16294aee8f1e98b1190c03a967 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+++ b/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();
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
index a68bd6e361647a6d17233c8a362875d22c706c3e..b4827659ce9cd2b64ec24996531786fad3d0fcf3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
+++ b/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);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
index 166f4b74a497da04ce0bf138f5777b7ed3860772..3d22d25c102ef8f008bd7dd6c8fe37f4444a0eba 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+++ b/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);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
index 828b4fa4e4d404203735e21cf5a5307ecd5465a4..fd2d4ee168db229c2d590e37f7f0f8bb460bc51f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
+++ b/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);
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
index 9cd5dc9cb8a5d3b3fdae87cbbe6724ed6790a096..1147d35f960fa3d7d8f7c6a7d3397e7b5f6402f3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
+++ b/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));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
index 196e1a37605049d23495bcc07b7a8b45d30c3ae2..4b706094131500fea65fe8e1d68882cb5b16b853 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
+++ b/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",
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
index 79680b69a4a6b7788e6b44ce003cfe60c0b5bda6..820ed8e257187d129ec5adfb9d838270c0911b5c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
+++ b/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);
diff --git a/src/plugins/e-acsl/tests/runtime/ptr.i b/src/plugins/e-acsl/tests/runtime/ptr.i
index 36faea67dda9885871ce4e746a40ef4955be0112..d2821e3da57e4753b955e6e7bb7119ee0230a84d 100644
--- a/src/plugins/e-acsl/tests/runtime/ptr.i
+++ b/src/plugins/e-acsl/tests/runtime/ptr.i
@@ -23,6 +23,8 @@ int main(void) {
p = t+2;
t[2] = 5;
/*@ assert *p == 5; */
+ int k = -1;
+ /*@ assert *(p+k) == 3; */ // bts #2252
return 0;
}
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index f15a5d1612a49dc6b9e080bf877196f1aeb292cb..d2b5849b6adb83a30c986172b19d0afd412c8efc 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -46,9 +46,6 @@ let c_int = C_type IInt
let ikind ik = C_type ik
let other = Other
-(* the integer_ty corresponding to the largest possible offset. *)
-let offset_ty () = C_type Cil.theMachine.Cil.ptrdiffKind
-
include Datatype.Make
(struct
type t = integer_ty
@@ -197,16 +194,32 @@ let ty_of_interv ?ctx i =
(* compute a new {!computed_info} by coercing the given type [ty] to the given
context [ctx]. [op] is the type for the operator. *)
-let coerce ~ctx ~op ty =
+let coerce ~arith_operand ~ctx ~op ty =
if compare ty ctx = 1 then begin
(* type larger than the expected context,
so we must introduce an explicit cast *)
{ ty; op; cast = Some ctx }
end else
- (* only add an explicit cast if the context is [Gmp] and [ty] is not *)
- if ctx = Gmp && ty <> Gmp then { ty; op; cast = Some Gmp }
+ (* only add an explicit cast if the context is [Gmp] and [ty] is not;
+ or if the term corresponding to [ty] is an operand of an arithmetic
+ operation which must be explicitely coerced in order to force the
+ operation to be of the expected type. *)
+ if (ctx = Gmp && ty <> Gmp) || arith_operand
+ then { ty; op; cast = Some ctx }
else { ty; op; cast = None }
+(* the integer_ty corresponding to [t] whenever use as an offset.
+ In that case, it cannot be a GMP, so it must be coerced to an integral type
+ in that case *)
+let offset_ty t =
+ try
+ let i = Interval.infer t in
+ match ty_of_interv i with
+ | Gmp -> C_type ILongLong (* largest possible type *)
+ | ty -> ty
+ with Interval.Not_an_integer ->
+ Options.fatal "expected an integral type for %a" Printer.pp_term t
+
(******************************************************************************)
(** {2 Type system} *)
(******************************************************************************)
@@ -221,7 +234,7 @@ let mk_ctx ~force c =
(* type the term [t] in a context [ctx]. Take --e-acsl-gmp-only into account iff
not [force]. *)
-let rec type_term ~force ?ctx t =
+let rec type_term ~force ?(arith_operand=false) ?ctx t =
let ctx = Extlib.opt_map (mk_ctx ~force) ctx in
let dup ty = ty, ty in
let compute_ctx ?ctx i =
@@ -302,7 +315,7 @@ let rec type_term ~force ?ctx t =
with Interval.Not_an_integer ->
dup Other (* real *)
in
- ignore (type_term ~force:false ~ctx t');
+ ignore (type_term ~force ~arith_operand:true ~ctx t');
(match unop with
| LNot -> c_int, ctx_res (* converted into [t == 0] in case of GMP *)
| Neg | BNot -> dup ctx_res)
@@ -317,8 +330,18 @@ let rec type_term ~force ?ctx t =
with Interval.Not_an_integer ->
dup Other (* real *)
in
- ignore (type_term ~force ~ctx t1);
- ignore (type_term ~force ~ctx t2);
+ (* it is enough to explicitely coerce when required one operand to [ctx]
+ (through [arith_operand]) in order to force the type of the operation.
+ Heuristic: coerce the operand which is not a lval in order to lower
+ the number of explicit casts *)
+ let rec cast_first t1 t2 = match t1.term_node with
+ | TLval _ -> false
+ | TLogic_coerce(_, t) -> cast_first t t2
+ | _ -> true
+ in
+ let cast_first = cast_first t1 t2 in
+ ignore (type_term ~force ~arith_operand:cast_first ~ctx t1);
+ ignore (type_term ~force ~arith_operand:(not cast_first) ~ctx t2);
dup ctx_res
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
@@ -390,7 +413,7 @@ let rec type_term ~force ?ctx t =
dup ctx
| Tat (t, _)
- | TLogic_coerce (_, t) -> dup (type_term ~force ?ctx t).ty
+ | TLogic_coerce (_, t) -> dup (type_term ~force ~arith_operand ?ctx t).ty
| TCoerceE (t1, t2) ->
let ctx =
@@ -418,10 +441,10 @@ let rec type_term ~force ?ctx t =
dup Other
| TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
- (* it is a pointer, while [t2] is a size_t. But both [t1] and [t2] must
- be typed. *)
+ (* both [t1] and [t2] must be typed. *)
ignore (type_term ~force:false ~ctx:Other t1);
- ignore (type_term ~force:true ~ctx:(offset_ty ()) t2);
+ let ctx = offset_ty t2 in
+ ignore (type_term ~force:true ~ctx t2);
dup Other
| Tapp(li, _, args) ->
@@ -454,7 +477,7 @@ let rec type_term ~force ?ctx t =
let ty, op = infer t in
match ctx with
| None -> { ty; op; cast = None }
- | Some ctx -> coerce ~ctx ~op ty)
+ | Some ctx -> coerce ~arith_operand ~ctx ~op ty)
t
and type_term_lval (host, offset) =
@@ -471,8 +494,8 @@ and type_term_offset = function
| TField(_, toff)
| TModel(_, toff) -> type_term_offset toff
| TIndex(t, toff) ->
- (* [t] is an array index which must fit into offset_ty *)
- ignore (type_term ~force:true ~ctx:(offset_ty ()) t);
+ let ctx = offset_ty t in
+ ignore (type_term ~force:true ~ctx t);
type_term_offset toff
let rec type_predicate p =
@@ -574,7 +597,7 @@ let rec type_predicate p =
| Pfresh _ -> Error.not_yet "\\fresh"
| Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
in
- coerce ~ctx:c_int ~op c_int
+ coerce ~arith_operand:false ~ctx:c_int ~op c_int
let type_term ~force ?ctx t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."