Commit 37b1265b authored by Julien Signoles's avatar Julien Signoles Committed by Kostyantyn Vorobyov
Browse files

[typing] fix bug #2252 about pointer arithmetic with negative offsets

parent 03cd4cee
......@@ -15,6 +15,8 @@
# 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.
......
......@@ -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] + (long)(*__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",
......
......@@ -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;
}
......
......@@ -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",
......
......@@ -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)",
......
......@@ -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));
......
......@@ -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);
......
......@@ -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);
......
......@@ -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);
}
......
......@@ -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));
......
......@@ -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;
}
......@@ -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
......@@ -211,6 +208,18 @@ let coerce ~arith_operand ~ctx ~op ty =
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} *)
(******************************************************************************)
......@@ -432,10 +441,10 @@ let rec type_term ~force ?(arith_operand=false) ?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) ->
......@@ -485,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 =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment