diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
index 3dbfd57c93af5c2095db14eb114db36d0ea21f89..90b370c4f2cd506313c73d515bb600fe16deb609 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
@@ -29,7 +29,7 @@ int main(void)
__e_acsl_full_init((void *)(& p));
{
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)(p + 1 * 0),(size_t)9,
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(p + 1 * 0),(size_t)10,
(void *)p,(void *)(& p));
__e_acsl_assert(! __gen_e_acsl_valid,"Assertion","main",
"!\\valid(p + (0 .. 9))","tests/bts/bts2406.c",10);
@@ -37,7 +37,7 @@ int main(void)
/*@ assert ¬\valid(p + (0 .. 9)); */ ;
{
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& t + 1 * 0),(size_t)9,
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& t + 1 * 0),(size_t)10,
(void *)(& t),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_2,"Assertion","main",
"\\valid(&t[0 .. 9])","tests/bts/bts2406.c",11);
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
index 8e3439c83775f0bd853817078ee8f08865b6cf39..89bbf9a94b82384ac91ba5d41542435a548061a6 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
@@ -50,7 +50,7 @@ int main(void)
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)((char *)a + 4 * 0),
- (size_t)16,(void *)a,(void *)(& a));
+ (size_t)20,(void *)a,(void *)(& a));
__e_acsl_assert(__gen_e_acsl_valid,"Assertion","main",
"\\valid(a + (0 .. 4))",
"tests/memory/ranges_in_builtins.c",19);
@@ -60,17 +60,17 @@ int main(void)
{
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)a + 4 * 4),
- (size_t)(4L * ((8L + j) - 4L)),
+ (size_t)(4L * (((7L + j) - 4L) + 1L)),
(void *)a,(void *)(& a));
__e_acsl_assert(__gen_e_acsl_valid_2,"Assertion","main",
- "\\valid(a + (4 .. 8 + j))",
+ "\\valid(a + (4 .. 7 + j))",
"tests/memory/ranges_in_builtins.c",21);
}
- /*@ assert \valid(a + (4 .. 8 + j)); */ ;
+ /*@ assert \valid(a + (4 .. 7 + j)); */ ;
{
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)((char *)a + 4 * 10),
- (size_t)4,(void *)a,(void *)(& a));
+ (size_t)8,(void *)a,(void *)(& a));
__e_acsl_assert(! __gen_e_acsl_valid_3,"Assertion","main",
"!\\valid(a + (10 .. 11))",
"tests/memory/ranges_in_builtins.c",22);
@@ -84,26 +84,26 @@ int main(void)
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)(b + 1 * 0),(size_t)10,
(void *)b,(void *)(& b));
__e_acsl_assert(__gen_e_acsl_valid_4,"Assertion","main",
- "\\valid(b + (0 .. 10))",
+ "\\valid(b + (0 .. 9))",
"tests/memory/ranges_in_builtins.c",27);
}
- /*@ assert \valid(b + (0 .. 10)); */ ;
+ /*@ assert \valid(b + (0 .. 9)); */ ;
{
int __gen_e_acsl_valid_5;
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)(b + 1 * 11),(size_t)4,
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)(b + 1 * 10),(size_t)6,
(void *)b,(void *)(& b));
__e_acsl_assert(! __gen_e_acsl_valid_5,"Assertion","main",
- "!\\valid(b + (11 .. 15))",
+ "!\\valid(b + (10 .. 15))",
"tests/memory/ranges_in_builtins.c",28);
}
- /*@ assert ¬\valid(b + (11 .. 15)); */ ;
+ /*@ assert ¬\valid(b + (10 .. 15)); */ ;
long t[3] = {7l, 8l, 9l};
__e_acsl_store_block((void *)(t),(size_t)24);
__e_acsl_full_init((void *)(& t));
{
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)((char *)(& t) + 8 * 0),
- (size_t)16,(void *)(& t),(void *)0);
+ (size_t)24,(void *)(& t),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_6,"Assertion","main",
"\\valid(&t[0 .. 2])",
"tests/memory/ranges_in_builtins.c",31);
@@ -112,7 +112,7 @@ int main(void)
{
int __gen_e_acsl_valid_7;
__gen_e_acsl_valid_7 = __e_acsl_valid((void *)((char *)(& t) + 8 * 3),
- (size_t)16,(void *)(& t),(void *)0);
+ (size_t)24,(void *)(& t),(void *)0);
__e_acsl_assert(! __gen_e_acsl_valid_7,"Assertion","main",
"!\\valid(&t[3 .. 5])",
"tests/memory/ranges_in_builtins.c",32);
@@ -127,7 +127,7 @@ int main(void)
int __gen_e_acsl_initialized;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)(& t2) +
8 * 0),
- (size_t)8);
+ (size_t)16);
__e_acsl_assert(__gen_e_acsl_initialized,"Assertion","main",
"\\initialized(&t2[0 .. 1])",
"tests/memory/ranges_in_builtins.c",38);
@@ -137,7 +137,7 @@ int main(void)
int __gen_e_acsl_initialized_2;
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)((char *)(& t2) +
8 * 2),
- (size_t)8);
+ (size_t)16);
__e_acsl_assert(! __gen_e_acsl_initialized_2,"Assertion","main",
"!\\initialized(&t2[2 .. 3])",
"tests/memory/ranges_in_builtins.c",39);
@@ -148,10 +148,10 @@ int main(void)
__gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(b + 1 * 0),
(size_t)10);
__e_acsl_assert(! __gen_e_acsl_initialized_3,"Assertion","main",
- "!\\initialized(b + (0 .. 10))",
+ "!\\initialized(b + (0 .. 9))",
"tests/memory/ranges_in_builtins.c",41);
}
- /*@ assert ¬\initialized(b + (0 .. 10)); */ ;
+ /*@ assert ¬\initialized(b + (0 .. 9)); */ ;
free((void *)b);
int n = 2;
{
@@ -198,7 +198,7 @@ int main(void)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)(& t3[6][1][0]) +
- 4 * 2),(size_t)32,
+ 4 * 2),(size_t)36,
(void *)(& t3[6][1][0]),
(void *)0);
__e_acsl_assert(! __gen_e_acsl_valid_read,"Assertion","main",
@@ -243,15 +243,16 @@ int main(void)
4 * 1),
(size_t)4);
__e_acsl_assert(__gen_e_acsl_initialized_5,"Assertion","main",
- "\\initialized(&s.a[0] + (1 .. 2))",
+ "\\initialized(&s.a[0] + (1 .. 1))",
"tests/memory/ranges_in_builtins.c",53);
}
- /*@ assert \initialized(&s.a[0] + (1 .. 2)); */ ;
+ /*@ assert \initialized(&s.a[0] + (1 .. 1)); */ ;
{
int __gen_e_acsl_initialized_6;
+ /*@ assert Eva: initialization: \initialized(&s.b); */
__gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)((char *)s.b +
4 * 0),
- (size_t)4);
+ (size_t)8);
__e_acsl_assert(! __gen_e_acsl_initialized_6,"Assertion","main",
"!\\initialized(s.b + (0 .. 1))",
"tests/memory/ranges_in_builtins.c",54);
@@ -279,7 +280,7 @@ int main(void)
"mem_access: \\valid_read(multi_dynamic + 4)",
"tests/memory/ranges_in_builtins.c",63);
__gen_e_acsl_valid_8 = __e_acsl_valid((void *)((char *)*(multi_dynamic + 4) +
- 4 * 1),(size_t)24,
+ 4 * 1),(size_t)28,
(void *)*(multi_dynamic + 4),
(void *)(multi_dynamic + 4));
__e_acsl_assert(__gen_e_acsl_valid_8,"Assertion","main",
@@ -325,6 +326,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__e_acsl_mpz_t __gen_e_acsl__2;
__e_acsl_mpz_t __gen_e_acsl_sub;
__e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
__e_acsl_mpz_t __gen_e_acsl_mul;
int __gen_e_acsl_le;
int __gen_e_acsl_and;
@@ -343,10 +345,14 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_sub(__gen_e_acsl_sub_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
__gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
if (__gen_e_acsl_le <= 0) {
@@ -356,6 +362,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__e_acsl_mpz_t __gen_e_acsl_sub_3;
__e_acsl_mpz_t __gen_e_acsl__4;
__e_acsl_mpz_t __gen_e_acsl_sub_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
__e_acsl_mpz_t __gen_e_acsl_mul_2;
__e_acsl_mpz_t __gen_e_acsl__5;
int __gen_e_acsl_lt;
@@ -371,10 +378,14 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_sub(__gen_e_acsl_sub_4,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init(__gen_e_acsl_mul_2);
__gmpz_mul(__gen_e_acsl_mul_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
__gmpz_init_set_ui(__gen_e_acsl__5,18446744073709551615UL);
__gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
@@ -385,6 +396,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_clear(__gen_e_acsl_sub_3);
__gmpz_clear(__gen_e_acsl__4);
__gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl_add_2);
__gmpz_clear(__gen_e_acsl_mul_2);
__gmpz_clear(__gen_e_acsl__5);
}
@@ -405,6 +417,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_clear(__gen_e_acsl__2);
__gmpz_clear(__gen_e_acsl_sub);
__gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
__gmpz_clear(__gen_e_acsl_mul);
}
{
@@ -434,8 +447,9 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__e_acsl_mpz_t __gen_e_acsl__6;
__e_acsl_mpz_t __gen_e_acsl_sizeof_3;
__e_acsl_mpz_t __gen_e_acsl__7;
- __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
__e_acsl_mpz_t __gen_e_acsl_sub_5;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
__e_acsl_mpz_t __gen_e_acsl_mul_3;
int __gen_e_acsl_le_2;
int __gen_e_acsl_and_2;
@@ -444,53 +458,63 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_init_set_si(__gen_e_acsl__6,0L);
__gmpz_init_set_si(__gen_e_acsl_sizeof_3,8L);
__gmpz_init_set_si(__gen_e_acsl__7,1L);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__gmpz_init(__gen_e_acsl_sub_5);
__gmpz_sub(__gen_e_acsl_sub_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__gmpz_init(__gen_e_acsl_mul_3);
__gmpz_mul(__gen_e_acsl_mul_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_5));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
__gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__6),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
if (__gen_e_acsl_le_2 <= 0) {
__e_acsl_mpz_t __gen_e_acsl_sizeof_4;
__e_acsl_mpz_t __gen_e_acsl__8;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
__e_acsl_mpz_t __gen_e_acsl__9;
__e_acsl_mpz_t __gen_e_acsl_sub_6;
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
__e_acsl_mpz_t __gen_e_acsl_mul_4;
__e_acsl_mpz_t __gen_e_acsl__10;
int __gen_e_acsl_lt_2;
__gmpz_init_set_si(__gen_e_acsl_sizeof_4,8L);
__gmpz_init_set_si(__gen_e_acsl__8,1L);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__gmpz_init_set_si(__gen_e_acsl__9,0L);
__gmpz_init(__gen_e_acsl_sub_6);
__gmpz_sub(__gen_e_acsl_sub_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__gmpz_init(__gen_e_acsl_mul_4);
__gmpz_mul(__gen_e_acsl_mul_4,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_6));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
__gmpz_init_set_ui(__gen_e_acsl__10,18446744073709551615UL);
__gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_4),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
__gen_e_acsl_and_2 = __gen_e_acsl_lt_2 < 0;
__gmpz_clear(__gen_e_acsl_sizeof_4);
__gmpz_clear(__gen_e_acsl__8);
- __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl_add_5);
__gmpz_clear(__gen_e_acsl__9);
__gmpz_clear(__gen_e_acsl_sub_6);
+ __gmpz_clear(__gen_e_acsl_add_6);
__gmpz_clear(__gen_e_acsl_mul_4);
__gmpz_clear(__gen_e_acsl__10);
}
@@ -511,8 +535,9 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_clear(__gen_e_acsl__6);
__gmpz_clear(__gen_e_acsl_sizeof_3);
__gmpz_clear(__gen_e_acsl__7);
- __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_add_3);
__gmpz_clear(__gen_e_acsl_sub_5);
+ __gmpz_clear(__gen_e_acsl_add_4);
__gmpz_clear(__gen_e_acsl_mul_3);
__gmpz_clear(__gen_e_acsl_at_2);
return;
@@ -530,6 +555,8 @@ void __gen_e_acsl_f(char *s, long n)
__e_acsl_mpz_t __gen_e_acsl_add;
__e_acsl_mpz_t __gen_e_acsl__3;
__e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
__e_acsl_mpz_t __gen_e_acsl_mul;
int __gen_e_acsl_le;
int __gen_e_acsl_and;
@@ -549,50 +576,64 @@ void __gen_e_acsl_f(char *s, long n)
__gmpz_sub(__gen_e_acsl_sub,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_init_set_si(__gen_e_acsl__4,1L);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
__gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
if (__gen_e_acsl_le <= 0) {
__e_acsl_mpz_t __gen_e_acsl_sizeof_2;
__e_acsl_mpz_t __gen_e_acsl_n_2;
- __e_acsl_mpz_t __gen_e_acsl__4;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
__e_acsl_mpz_t __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl__6;
__e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
__e_acsl_mpz_t __gen_e_acsl_mul_2;
- __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl__8;
int __gen_e_acsl_lt;
__gmpz_init_set_si(__gen_e_acsl_sizeof_2,1L);
__gmpz_init_set_si(__gen_e_acsl_n_2,n);
- __gmpz_init_set_si(__gen_e_acsl__4,1000L);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
+ __gmpz_init_set_si(__gen_e_acsl__5,1000L);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __gmpz_init_set_si(__gen_e_acsl__5,3L);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gmpz_init_set_si(__gen_e_acsl__6,3L);
__gmpz_init(__gen_e_acsl_sub_2);
__gmpz_sub(__gen_e_acsl_sub_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init_set_si(__gen_e_acsl__7,1L);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__gmpz_init(__gen_e_acsl_mul_2);
__gmpz_mul(__gen_e_acsl_mul_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2));
- __gmpz_init_set_ui(__gen_e_acsl__6,18446744073709551615UL);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_init_set_ui(__gen_e_acsl__8,18446744073709551615UL);
__gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__gen_e_acsl_and = __gen_e_acsl_lt < 0;
__gmpz_clear(__gen_e_acsl_sizeof_2);
__gmpz_clear(__gen_e_acsl_n_2);
- __gmpz_clear(__gen_e_acsl__4);
- __gmpz_clear(__gen_e_acsl_add_2);
__gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl__6);
__gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl_add_4);
__gmpz_clear(__gen_e_acsl_mul_2);
- __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl__8);
}
else __gen_e_acsl_and = 0;
__e_acsl_assert(__gen_e_acsl_and,"RTE","f",
@@ -612,6 +653,8 @@ void __gen_e_acsl_f(char *s, long n)
__gmpz_clear(__gen_e_acsl_add);
__gmpz_clear(__gen_e_acsl__3);
__gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_add_2);
__gmpz_clear(__gen_e_acsl_mul);
}
f(s,n);
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle
index a6b067c83c9b1f9067ea56155bc55976e2060ea8..74e130d7182ee876c8f3b1bc3fb688967cb221a4 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle
@@ -4,5 +4,17 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/ranges_in_builtins.c:21: Warning:
- assertion got status invalid (stopping propagation).
+[eva:alarm] tests/memory/ranges_in_builtins.c:7: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/ranges_in_builtins.c:8: Warning:
+ function __gmpz_init_set: precondition ¬\initialized(z) got status unknown.
+[eva:alarm] tests/memory/ranges_in_builtins.c:8: Warning:
+ function __gmpz_init_set: precondition ¬\initialized(z) got status unknown.
+[eva:alarm] tests/memory/ranges_in_builtins.c:8: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/ranges_in_builtins.c:8: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/ranges_in_builtins.c:49: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/ranges_in_builtins.c:54: Warning:
+ accessing uninitialized left-value. assert \initialized(&s.b);
diff --git a/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
index 208afd355b95ebac47ccc3979e1238c582be9682..4cb9d45b44a903599da58cbd1453c3d143c6446c 100644
--- a/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
@@ -18,14 +18,14 @@ int main(void) {
a = malloc(10*sizeof(int));
/*@ assert \valid(a + (0 .. 4)); */ ;
int j = 2;
- /*@ assert \valid(a + (4 .. 8+j)); */ ;
+ /*@ assert \valid(a + (4 .. 7+j)); */ ;
/*@ assert !\valid(a + (10 .. 11)); */ ;
free(a);
char *b;
b = malloc(10*sizeof(char));
- /*@ assert \valid(b + (0 .. 10)); */ ;
- /*@ assert !\valid(b + (11 .. 15)); */ ;
+ /*@ assert \valid(b + (0 .. 9)); */ ;
+ /*@ assert !\valid(b + (10 .. 15)); */ ;
long t[3] = {7l, 8l, 9l};
/*@ assert \valid(&t[0..2]); */ ;
@@ -38,7 +38,7 @@ int main(void) {
/*@ assert \initialized(&t2[0..1]); */ ;
/*@ assert !\initialized(&t2[2..3]); */ ;
- /*@ assert !\initialized(b + (0 .. 10));*/
+ /*@ assert !\initialized(b + (0 .. 9));*/
free(b);
int n = 2;
@@ -50,7 +50,7 @@ int main(void) {
struct S s;
s.a[0] = 7; s.a[1] = 8;
- /*@ assert \initialized(&s.a[0] + (1..2)); */ ;
+ /*@ assert \initialized(&s.a[0] + (1..1)); */ ;
/*@ assert !\initialized(s.b + (0..1)); */ ;
int **multi_dynamic;