Skip to content
Snippets Groups Projects
Commit aa1f4136 authored by Basile Desloges's avatar Basile Desloges Committed by Julien Signoles
Browse files

[eacsl:tests] Update tests with ranges

parent f88ddb49
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
+ 2
− 2
View file @ aa1f4136
...@@ -29,7 +29,7 @@ int main(void) ...@@ -29,7 +29,7 @@ int main(void)
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& p));
{ {
int __gen_e_acsl_valid; 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)); (void *)p,(void *)(& p));
__e_acsl_assert(! __gen_e_acsl_valid,"Assertion","main", __e_acsl_assert(! __gen_e_acsl_valid,"Assertion","main",
"!\\valid(p + (0 .. 9))","tests/bts/bts2406.c",10); "!\\valid(p + (0 .. 9))","tests/bts/bts2406.c",10);
...@@ -37,7 +37,7 @@ int main(void) ...@@ -37,7 +37,7 @@ int main(void)
/*@ assert ¬\valid(p + (0 .. 9)); */ ; /*@ assert ¬\valid(p + (0 .. 9)); */ ;
{ {
int __gen_e_acsl_valid_2; 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); (void *)(& t),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_2,"Assertion","main", __e_acsl_assert(__gen_e_acsl_valid_2,"Assertion","main",
"\\valid(&t[0 .. 9])","tests/bts/bts2406.c",11); "\\valid(&t[0 .. 9])","tests/bts/bts2406.c",11);
......
src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
+ 95
− 52
View file @ aa1f4136
...@@ -50,7 +50,7 @@ int main(void) ...@@ -50,7 +50,7 @@ int main(void)
{ {
int __gen_e_acsl_valid; int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)((char *)a + 4 * 0), __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", __e_acsl_assert(__gen_e_acsl_valid,"Assertion","main",
"\\valid(a + (0 .. 4))", "\\valid(a + (0 .. 4))",
"tests/memory/ranges_in_builtins.c",19); "tests/memory/ranges_in_builtins.c",19);
...@@ -60,17 +60,17 @@ int main(void) ...@@ -60,17 +60,17 @@ int main(void)
{ {
int __gen_e_acsl_valid_2; int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)a + 4 * 4), __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)); (void *)a,(void *)(& a));
__e_acsl_assert(__gen_e_acsl_valid_2,"Assertion","main", __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); "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; int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)((char *)a + 4 * 10), __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", __e_acsl_assert(! __gen_e_acsl_valid_3,"Assertion","main",
"!\\valid(a + (10 .. 11))", "!\\valid(a + (10 .. 11))",
"tests/memory/ranges_in_builtins.c",22); "tests/memory/ranges_in_builtins.c",22);
...@@ -84,26 +84,26 @@ int main(void) ...@@ -84,26 +84,26 @@ int main(void)
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)(b + 1 * 0),(size_t)10, __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(b + 1 * 0),(size_t)10,
(void *)b,(void *)(& b)); (void *)b,(void *)(& b));
__e_acsl_assert(__gen_e_acsl_valid_4,"Assertion","main", __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); "tests/memory/ranges_in_builtins.c",27);
} }
/*@ assert \valid(b + (0 .. 10)); */ ; /*@ assert \valid(b + (0 .. 9)); */ ;
{ {
int __gen_e_acsl_valid_5; 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)); (void *)b,(void *)(& b));
__e_acsl_assert(! __gen_e_acsl_valid_5,"Assertion","main", __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); "tests/memory/ranges_in_builtins.c",28);
} }
/*@ assert ¬\valid(b + (11 .. 15)); */ ; /*@ assert ¬\valid(b + (10 .. 15)); */ ;
long t[3] = {7l, 8l, 9l}; long t[3] = {7l, 8l, 9l};
__e_acsl_store_block((void *)(t),(size_t)24); __e_acsl_store_block((void *)(t),(size_t)24);
__e_acsl_full_init((void *)(& t)); __e_acsl_full_init((void *)(& t));
{ {
int __gen_e_acsl_valid_6; int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)((char *)(& t) + 8 * 0), __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", __e_acsl_assert(__gen_e_acsl_valid_6,"Assertion","main",
"\\valid(&t[0 .. 2])", "\\valid(&t[0 .. 2])",
"tests/memory/ranges_in_builtins.c",31); "tests/memory/ranges_in_builtins.c",31);
...@@ -112,7 +112,7 @@ int main(void) ...@@ -112,7 +112,7 @@ int main(void)
{ {
int __gen_e_acsl_valid_7; int __gen_e_acsl_valid_7;
__gen_e_acsl_valid_7 = __e_acsl_valid((void *)((char *)(& t) + 8 * 3), __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", __e_acsl_assert(! __gen_e_acsl_valid_7,"Assertion","main",
"!\\valid(&t[3 .. 5])", "!\\valid(&t[3 .. 5])",
"tests/memory/ranges_in_builtins.c",32); "tests/memory/ranges_in_builtins.c",32);
...@@ -127,7 +127,7 @@ int main(void) ...@@ -127,7 +127,7 @@ int main(void)
int __gen_e_acsl_initialized; int __gen_e_acsl_initialized;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)(& t2) + __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)(& t2) +
8 * 0), 8 * 0),
(size_t)8); (size_t)16);
__e_acsl_assert(__gen_e_acsl_initialized,"Assertion","main", __e_acsl_assert(__gen_e_acsl_initialized,"Assertion","main",
"\\initialized(&t2[0 .. 1])", "\\initialized(&t2[0 .. 1])",
"tests/memory/ranges_in_builtins.c",38); "tests/memory/ranges_in_builtins.c",38);
...@@ -137,7 +137,7 @@ int main(void) ...@@ -137,7 +137,7 @@ int main(void)
int __gen_e_acsl_initialized_2; int __gen_e_acsl_initialized_2;
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)((char *)(& t2) + __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)((char *)(& t2) +
8 * 2), 8 * 2),
(size_t)8); (size_t)16);
__e_acsl_assert(! __gen_e_acsl_initialized_2,"Assertion","main", __e_acsl_assert(! __gen_e_acsl_initialized_2,"Assertion","main",
"!\\initialized(&t2[2 .. 3])", "!\\initialized(&t2[2 .. 3])",
"tests/memory/ranges_in_builtins.c",39); "tests/memory/ranges_in_builtins.c",39);
...@@ -148,10 +148,10 @@ int main(void) ...@@ -148,10 +148,10 @@ int main(void)
__gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(b + 1 * 0), __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(b + 1 * 0),
(size_t)10); (size_t)10);
__e_acsl_assert(! __gen_e_acsl_initialized_3,"Assertion","main", __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); "tests/memory/ranges_in_builtins.c",41);
} }
/*@ assert ¬\initialized(b + (0 .. 10)); */ ; /*@ assert ¬\initialized(b + (0 .. 9)); */ ;
free((void *)b); free((void *)b);
int n = 2; int n = 2;
{ {
...@@ -198,7 +198,7 @@ int main(void) ...@@ -198,7 +198,7 @@ int main(void)
{ {
int __gen_e_acsl_valid_read; int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)(& t3[6][1][0]) + __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 *)(& t3[6][1][0]),
(void *)0); (void *)0);
__e_acsl_assert(! __gen_e_acsl_valid_read,"Assertion","main", __e_acsl_assert(! __gen_e_acsl_valid_read,"Assertion","main",
...@@ -243,15 +243,16 @@ int main(void) ...@@ -243,15 +243,16 @@ int main(void)
4 * 1), 4 * 1),
(size_t)4); (size_t)4);
__e_acsl_assert(__gen_e_acsl_initialized_5,"Assertion","main", __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); "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; int __gen_e_acsl_initialized_6;
/*@ assert Eva: initialization: \initialized(&s.b); */
__gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)((char *)s.b + __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)((char *)s.b +
4 * 0), 4 * 0),
(size_t)4); (size_t)8);
__e_acsl_assert(! __gen_e_acsl_initialized_6,"Assertion","main", __e_acsl_assert(! __gen_e_acsl_initialized_6,"Assertion","main",
"!\\initialized(s.b + (0 .. 1))", "!\\initialized(s.b + (0 .. 1))",
"tests/memory/ranges_in_builtins.c",54); "tests/memory/ranges_in_builtins.c",54);
...@@ -279,7 +280,7 @@ int main(void) ...@@ -279,7 +280,7 @@ int main(void)
"mem_access: \\valid_read(multi_dynamic + 4)", "mem_access: \\valid_read(multi_dynamic + 4)",
"tests/memory/ranges_in_builtins.c",63); "tests/memory/ranges_in_builtins.c",63);
__gen_e_acsl_valid_8 = __e_acsl_valid((void *)((char *)*(multi_dynamic + 4) + __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),
(void *)(multi_dynamic + 4)); (void *)(multi_dynamic + 4));
__e_acsl_assert(__gen_e_acsl_valid_8,"Assertion","main", __e_acsl_assert(__gen_e_acsl_valid_8,"Assertion","main",
...@@ -325,6 +326,7 @@ void __gen_e_acsl_g(long *ptr, size_t size) ...@@ -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__2;
__e_acsl_mpz_t __gen_e_acsl_sub; __e_acsl_mpz_t __gen_e_acsl_sub;
__e_acsl_mpz_t __gen_e_acsl_sub_2; __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; __e_acsl_mpz_t __gen_e_acsl_mul;
int __gen_e_acsl_le; int __gen_e_acsl_le;
int __gen_e_acsl_and; int __gen_e_acsl_and;
...@@ -343,10 +345,14 @@ void __gen_e_acsl_g(long *ptr, size_t size) ...@@ -343,10 +345,14 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_sub(__gen_e_acsl_sub_2, __gmpz_sub(__gen_e_acsl_sub_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sub), (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_)); (__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_init(__gen_e_acsl_mul);
__gmpz_mul(__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_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_), __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul)); (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
if (__gen_e_acsl_le <= 0) { if (__gen_e_acsl_le <= 0) {
...@@ -356,6 +362,7 @@ void __gen_e_acsl_g(long *ptr, size_t size) ...@@ -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_sub_3;
__e_acsl_mpz_t __gen_e_acsl__4; __e_acsl_mpz_t __gen_e_acsl__4;
__e_acsl_mpz_t __gen_e_acsl_sub_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_mul_2;
__e_acsl_mpz_t __gen_e_acsl__5; __e_acsl_mpz_t __gen_e_acsl__5;
int __gen_e_acsl_lt; int __gen_e_acsl_lt;
...@@ -371,10 +378,14 @@ void __gen_e_acsl_g(long *ptr, size_t size) ...@@ -371,10 +378,14 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__gmpz_sub(__gen_e_acsl_sub_4, __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_sub_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__4)); (__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_init(__gen_e_acsl_mul_2);
__gmpz_mul(__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_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); __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), __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)); (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
...@@ -385,6 +396,7 @@ void __gen_e_acsl_g(long *ptr, size_t size) ...@@ -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_sub_3);
__gmpz_clear(__gen_e_acsl__4); __gmpz_clear(__gen_e_acsl__4);
__gmpz_clear(__gen_e_acsl_sub_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_mul_2);
__gmpz_clear(__gen_e_acsl__5); __gmpz_clear(__gen_e_acsl__5);
} }
...@@ -405,6 +417,7 @@ void __gen_e_acsl_g(long *ptr, size_t size) ...@@ -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__2);
__gmpz_clear(__gen_e_acsl_sub); __gmpz_clear(__gen_e_acsl_sub);
__gmpz_clear(__gen_e_acsl_sub_2); __gmpz_clear(__gen_e_acsl_sub_2);
__gmpz_clear(__gen_e_acsl_add);
__gmpz_clear(__gen_e_acsl_mul); __gmpz_clear(__gen_e_acsl_mul);
} }
{ {
...@@ -434,8 +447,9 @@ void __gen_e_acsl_g(long *ptr, size_t size) ...@@ -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__6;
__e_acsl_mpz_t __gen_e_acsl_sizeof_3; __e_acsl_mpz_t __gen_e_acsl_sizeof_3;
__e_acsl_mpz_t __gen_e_acsl__7; __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_sub_5;
__e_acsl_mpz_t __gen_e_acsl_add_4;
__e_acsl_mpz_t __gen_e_acsl_mul_3; __e_acsl_mpz_t __gen_e_acsl_mul_3;
int __gen_e_acsl_le_2; int __gen_e_acsl_le_2;
int __gen_e_acsl_and_2; int __gen_e_acsl_and_2;
...@@ -444,53 +458,63 @@ void __gen_e_acsl_g(long *ptr, size_t size) ...@@ -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__6,0L);
__gmpz_init_set_si(__gen_e_acsl_sizeof_3,8L); __gmpz_init_set_si(__gen_e_acsl_sizeof_3,8L);
__gmpz_init_set_si(__gen_e_acsl__7,1L); __gmpz_init_set_si(__gen_e_acsl__7,1L);
__gmpz_init(__gen_e_acsl_add); __gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add, __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_at_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__7)); (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__gmpz_init(__gen_e_acsl_sub_5); __gmpz_init(__gen_e_acsl_sub_5);
__gmpz_sub(__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)); (__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_init(__gen_e_acsl_mul_3);
__gmpz_mul(__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_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), __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)); (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
if (__gen_e_acsl_le_2 <= 0) { if (__gen_e_acsl_le_2 <= 0) {
__e_acsl_mpz_t __gen_e_acsl_sizeof_4; __e_acsl_mpz_t __gen_e_acsl_sizeof_4;
__e_acsl_mpz_t __gen_e_acsl__8; __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__9;
__e_acsl_mpz_t __gen_e_acsl_sub_6; __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_mul_4;
__e_acsl_mpz_t __gen_e_acsl__10; __e_acsl_mpz_t __gen_e_acsl__10;
int __gen_e_acsl_lt_2; int __gen_e_acsl_lt_2;
__gmpz_init_set_si(__gen_e_acsl_sizeof_4,8L); __gmpz_init_set_si(__gen_e_acsl_sizeof_4,8L);
__gmpz_init_set_si(__gen_e_acsl__8,1L); __gmpz_init_set_si(__gen_e_acsl__8,1L);
__gmpz_init(__gen_e_acsl_add_2); __gmpz_init(__gen_e_acsl_add_5);
__gmpz_add(__gen_e_acsl_add_2, __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_at_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__8)); (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__gmpz_init_set_si(__gen_e_acsl__9,0L); __gmpz_init_set_si(__gen_e_acsl__9,0L);
__gmpz_init(__gen_e_acsl_sub_6); __gmpz_init(__gen_e_acsl_sub_6);
__gmpz_sub(__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)); (__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_init(__gen_e_acsl_mul_4);
__gmpz_mul(__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_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); __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), __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)); (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
__gen_e_acsl_and_2 = __gen_e_acsl_lt_2 < 0; __gen_e_acsl_and_2 = __gen_e_acsl_lt_2 < 0;
__gmpz_clear(__gen_e_acsl_sizeof_4); __gmpz_clear(__gen_e_acsl_sizeof_4);
__gmpz_clear(__gen_e_acsl__8); __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__9);
__gmpz_clear(__gen_e_acsl_sub_6); __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_mul_4);
__gmpz_clear(__gen_e_acsl__10); __gmpz_clear(__gen_e_acsl__10);
} }
...@@ -511,8 +535,9 @@ void __gen_e_acsl_g(long *ptr, size_t size) ...@@ -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__6);
__gmpz_clear(__gen_e_acsl_sizeof_3); __gmpz_clear(__gen_e_acsl_sizeof_3);
__gmpz_clear(__gen_e_acsl__7); __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_sub_5);
__gmpz_clear(__gen_e_acsl_add_4);
__gmpz_clear(__gen_e_acsl_mul_3); __gmpz_clear(__gen_e_acsl_mul_3);
__gmpz_clear(__gen_e_acsl_at_2); __gmpz_clear(__gen_e_acsl_at_2);
return; return;
...@@ -530,6 +555,8 @@ void __gen_e_acsl_f(char *s, long n) ...@@ -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_add;
__e_acsl_mpz_t __gen_e_acsl__3; __e_acsl_mpz_t __gen_e_acsl__3;
__e_acsl_mpz_t __gen_e_acsl_sub; __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; __e_acsl_mpz_t __gen_e_acsl_mul;
int __gen_e_acsl_le; int __gen_e_acsl_le;
int __gen_e_acsl_and; int __gen_e_acsl_and;
...@@ -549,50 +576,64 @@ void __gen_e_acsl_f(char *s, long n) ...@@ -549,50 +576,64 @@ void __gen_e_acsl_f(char *s, long n)
__gmpz_sub(__gen_e_acsl_sub, __gmpz_sub(__gen_e_acsl_sub,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add), (__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__3)); (__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_init(__gen_e_acsl_mul);
__gmpz_mul(__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_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_), __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul)); (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
if (__gen_e_acsl_le <= 0) { if (__gen_e_acsl_le <= 0) {
__e_acsl_mpz_t __gen_e_acsl_sizeof_2; __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_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__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_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_mul_2;
__e_acsl_mpz_t __gen_e_acsl__6; __e_acsl_mpz_t __gen_e_acsl__8;
int __gen_e_acsl_lt; int __gen_e_acsl_lt;
__gmpz_init_set_si(__gen_e_acsl_sizeof_2,1L); __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_n_2,n);
__gmpz_init_set_si(__gen_e_acsl__4,1000L); __gmpz_init_set_si(__gen_e_acsl__5,1000L);
__gmpz_init(__gen_e_acsl_add_2); __gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add_2, __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_n_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__4)); (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
__gmpz_init_set_si(__gen_e_acsl__5,3L); __gmpz_init_set_si(__gen_e_acsl__6,3L);
__gmpz_init(__gen_e_acsl_sub_2); __gmpz_init(__gen_e_acsl_sub_2);
__gmpz_sub(__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_add_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5)); (__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_init(__gen_e_acsl_mul_2);
__gmpz_mul(__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_sizeof_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2)); (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
__gmpz_init_set_ui(__gen_e_acsl__6,18446744073709551615UL); __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), __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; __gen_e_acsl_and = __gen_e_acsl_lt < 0;
__gmpz_clear(__gen_e_acsl_sizeof_2); __gmpz_clear(__gen_e_acsl_sizeof_2);
__gmpz_clear(__gen_e_acsl_n_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__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_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_mul_2);
__gmpz_clear(__gen_e_acsl__6); __gmpz_clear(__gen_e_acsl__8);
} }
else __gen_e_acsl_and = 0; else __gen_e_acsl_and = 0;
__e_acsl_assert(__gen_e_acsl_and,"RTE","f", __e_acsl_assert(__gen_e_acsl_and,"RTE","f",
...@@ -612,6 +653,8 @@ void __gen_e_acsl_f(char *s, long n) ...@@ -612,6 +653,8 @@ void __gen_e_acsl_f(char *s, long n)
__gmpz_clear(__gen_e_acsl_add); __gmpz_clear(__gen_e_acsl_add);
__gmpz_clear(__gen_e_acsl__3); __gmpz_clear(__gen_e_acsl__3);
__gmpz_clear(__gen_e_acsl_sub); __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); __gmpz_clear(__gen_e_acsl_mul);
} }
f(s,n); f(s,n);
......
src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle
+ 14
− 2
View file @ aa1f4136
...@@ -4,5 +4,17 @@ ...@@ -4,5 +4,17 @@
is not yet supported. is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/memory/ranges_in_builtins.c:21: Warning: [eva:alarm] tests/memory/ranges_in_builtins.c:7: Warning:
assertion got status invalid (stopping propagation). 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);
src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
+ 5
− 5
View file @ aa1f4136
...@@ -18,14 +18,14 @@ int main(void) { ...@@ -18,14 +18,14 @@ int main(void) {
a = malloc(10*sizeof(int)); a = malloc(10*sizeof(int));
/*@ assert \valid(a + (0 .. 4)); */ ; /*@ assert \valid(a + (0 .. 4)); */ ;
int j = 2; int j = 2;
/*@ assert \valid(a + (4 .. 8+j)); */ ; /*@ assert \valid(a + (4 .. 7+j)); */ ;
/*@ assert !\valid(a + (10 .. 11)); */ ; /*@ assert !\valid(a + (10 .. 11)); */ ;
free(a); free(a);
char *b; char *b;
b = malloc(10*sizeof(char)); b = malloc(10*sizeof(char));
/*@ assert \valid(b + (0 .. 10)); */ ; /*@ assert \valid(b + (0 .. 9)); */ ;
/*@ assert !\valid(b + (11 .. 15)); */ ; /*@ assert !\valid(b + (10 .. 15)); */ ;
long t[3] = {7l, 8l, 9l}; long t[3] = {7l, 8l, 9l};
/*@ assert \valid(&t[0..2]); */ ; /*@ assert \valid(&t[0..2]); */ ;
...@@ -38,7 +38,7 @@ int main(void) { ...@@ -38,7 +38,7 @@ int main(void) {
/*@ assert \initialized(&t2[0..1]); */ ; /*@ assert \initialized(&t2[0..1]); */ ;
/*@ assert !\initialized(&t2[2..3]); */ ; /*@ assert !\initialized(&t2[2..3]); */ ;
/*@ assert !\initialized(b + (0 .. 10));*/ /*@ assert !\initialized(b + (0 .. 9));*/
free(b); free(b);
int n = 2; int n = 2;
...@@ -50,7 +50,7 @@ int main(void) { ...@@ -50,7 +50,7 @@ int main(void) {
struct S s; struct S s;
s.a[0] = 7; s.a[1] = 8; 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)); */ ; /*@ assert !\initialized(s.b + (0..1)); */ ;
int **multi_dynamic; int **multi_dynamic;
......
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