Commit 3f9b8dd3 authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'bugfix/basile/eacsl-fix-range-translation' into 'master'

[eacsl:codegen] Fix translation of ranges

See merge request frama-c/frama-c!2750
parents 4788bc52 9af1aab7
......@@ -25,6 +25,7 @@
Plugin E-ACSL <next-release>
############################
-* E-ACSL [2020-07-10] Fix translation of trange (incorrect length).
-* E-ACSL [2020-07-09] Decrease the number of allocated blocks when one
block is freed.
- E-ACSL [2020-06-19] Add support of bitwise operators for C integers.
......
......@@ -204,13 +204,17 @@ let call_memory_block ~loc kf name ctx env ptr r p =
we need to clone them in order to force retyping *)
let s = { s with term_node = s.term_node } in
let n1 = { n1 with term_node = n1.term_node } in
Logic_const.term
~loc
(TBinOp(
Mult,
s,
Logic_const.term ~loc (TBinOp(MinusA, n2, n1)) Linteger))
Linteger
(* The range are inclusives, so the total number of elements is
[n2 - n1 + 1] *)
let count = Logic_const.term
~loc
(TBinOp (
PlusA,
Logic_const.term ~loc (TBinOp (MinusA, n2, n1)) Linteger,
Logic_const.tinteger ~loc 1))
Linteger
in
Logic_const.term ~loc (TBinOp (Mult, s, count)) Linteger
in
Typing.type_term ~use_gmp_opt:false size_term;
let size, env = match Typing.get_number_ty size_term with
......
......@@ -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);
......
......@@ -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);
......
......@@ -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);
......@@ -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;
......
Supports Markdown
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