diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
index 994e5e176d8b6f2c1d0a276505cc9b85773538e7..9fa7a4c3837305fe11f1259849cd635115a40859 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
@@ -2,8 +2,6 @@
[e-acsl] Warning: annotating undefined function `strncpy':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:362: Warning:
- E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:372: Warning:
E-ACSL construct `logic functions performing read accesses'
is not yet supported.
@@ -15,8 +13,6 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:363: Warning:
E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:366: Warning:
- E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:362: Warning:
Some assumes clauses couldn't be translated.
Ignoring complete and disjoint behaviors annotations.
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
index 58c0df1de84e4233601befe38ea728af74dfe708..23e58720f83757fa2167d59192c14bfd47dfec50 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
@@ -56,6 +56,7 @@ char *__gen_e_acsl_strncpy(char * __restrict dest,
__e_acsl_contract_t *__gen_e_acsl_contract;
char *__retres;
{
+ unsigned long __gen_e_acsl_size;
__e_acsl_mpz_t __gen_e_acsl_n;
__e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_sub;
@@ -63,7 +64,24 @@ char *__gen_e_acsl_strncpy(char * __restrict dest,
__e_acsl_mpz_t __gen_e_acsl_sub_2;
__e_acsl_mpz_t __gen_e_acsl_add;
unsigned long __gen_e_acsl__3;
+ unsigned long __gen_e_acsl_if;
int __gen_e_acsl_valid;
+ unsigned long __gen_e_acsl_size_2;
+ unsigned long __gen_e_acsl__4;
+ unsigned long __gen_e_acsl_if_2;
+ int __gen_e_acsl_valid_read;
+ unsigned long __gen_e_acsl_size_3;
+ unsigned long __gen_e_acsl__5;
+ unsigned long __gen_e_acsl_if_3;
+ int __gen_e_acsl_valid_read_2;
+ unsigned long __gen_e_acsl_size_4;
+ unsigned long __gen_e_acsl__6;
+ unsigned long __gen_e_acsl_if_4;
+ unsigned long __gen_e_acsl_size_5;
+ unsigned long __gen_e_acsl__7;
+ unsigned long __gen_e_acsl_if_5;
+ int __gen_e_acsl_separated;
+ __e_acsl_store_block((void *)(& src),(size_t)8);
__e_acsl_store_block((void *)(& dest),(size_t)8);
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__gmpz_init_set_ui(__gen_e_acsl_n,n);
@@ -82,12 +100,54 @@ char *__gen_e_acsl_strncpy(char * __restrict dest,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
__gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size = 1UL * __gen_e_acsl__3;
+ if (__gen_e_acsl_size <= 0UL) __gen_e_acsl_if = 0UL;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
__gen_e_acsl_valid = __e_acsl_valid((void *)(dest + 1 * 0),
- __gen_e_acsl__3,(void *)dest,
+ __gen_e_acsl_if,(void *)dest,
(void *)(& dest));
__e_acsl_assert(__gen_e_acsl_valid,"Precondition","strncpy",
"\\valid(dest + (0 .. n - 1))",
"FRAMAC_SHARE/libc/string.h",364);
+ __gen_e_acsl__4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_2 = 1UL * __gen_e_acsl__4;
+ if (__gen_e_acsl_size_2 <= 0UL) __gen_e_acsl_if_2 = 0UL;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(dest + 1 * 0),
+ __gen_e_acsl_if_2,
+ (void *)dest,
+ (void *)(& dest));
+ /*@ assert E_ACSL: separated_guard: \valid_read(dest + (0 .. n - 1)); */
+ __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","strncpy",
+ "separated_guard: \\valid_read(dest + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",366);
+ __gen_e_acsl__5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__5;
+ if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_3 = 0UL;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(src + 1 * 0),
+ __gen_e_acsl_if_3,
+ (void *)src,
+ (void *)(& src));
+ /*@ assert E_ACSL: separated_guard: \valid_read(src + (0 .. n - 1)); */
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","strncpy",
+ "separated_guard: \\valid_read(src + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",366);
+ __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_4 = 1UL * __gen_e_acsl__6;
+ if (__gen_e_acsl_size_4 <= 0UL) __gen_e_acsl_if_4 = 0UL;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl__7 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_5 = 1UL * __gen_e_acsl__7;
+ if (__gen_e_acsl_size_5 <= 0UL) __gen_e_acsl_if_5 = 0UL;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_separated = __e_acsl_separated((size_t)2,dest + 1 * 0,
+ __gen_e_acsl_if_4,
+ src + 1 * 0,
+ __gen_e_acsl_if_5);
+ __e_acsl_assert(__gen_e_acsl_separated,"Precondition","strncpy",
+ "\\separated(dest + (0 .. n - 1), src + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",366);
__gmpz_clear(__gen_e_acsl_n);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_sub);
@@ -106,42 +166,48 @@ char *__gen_e_acsl_strncpy(char * __restrict dest,
__gen_e_acsl_at = dest;
__retres = strncpy(dest,src,n);
{
- __e_acsl_mpz_t __gen_e_acsl__4;
+ unsigned long __gen_e_acsl_size_6;
+ __e_acsl_mpz_t __gen_e_acsl__8;
__e_acsl_mpz_t __gen_e_acsl_sub_3;
- __e_acsl_mpz_t __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl__9;
__e_acsl_mpz_t __gen_e_acsl_sub_4;
__e_acsl_mpz_t __gen_e_acsl_add_2;
- unsigned long __gen_e_acsl__6;
+ unsigned long __gen_e_acsl__10;
+ unsigned long __gen_e_acsl_if_6;
int __gen_e_acsl_initialized;
__e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","strncpy",
"\\result == \\old(dest)","FRAMAC_SHARE/libc/string.h",
369);
- __gmpz_init_set_si(__gen_e_acsl__4,1L);
+ __gmpz_init_set_si(__gen_e_acsl__8,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __gmpz_init_set_si(__gen_e_acsl__5,0L);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_init_set_si(__gen_e_acsl__9,0L);
__gmpz_init(__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__5));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
__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__4));
- __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gen_e_acsl__10 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gen_e_acsl_size_6 = 1UL * __gen_e_acsl__10;
+ if (__gen_e_acsl_size_6 <= 0UL) __gen_e_acsl_if_6 = 0UL;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
1 * 0),
- __gen_e_acsl__6);
+ __gen_e_acsl_if_6);
__e_acsl_assert(__gen_e_acsl_initialized,"Postcondition","strncpy",
"\\initialized(\\old(dest) + (0 .. \\old(n) - 1))",
"FRAMAC_SHARE/libc/string.h",370);
__e_acsl_contract_clean(__gen_e_acsl_contract);
+ __e_acsl_delete_block((void *)(& src));
__e_acsl_delete_block((void *)(& dest));
- __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl__8);
__gmpz_clear(__gen_e_acsl_sub_3);
- __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl__9);
__gmpz_clear(__gen_e_acsl_sub_4);
__gmpz_clear(__gen_e_acsl_add_2);
__gmpz_clear(__gen_e_acsl_at_3);
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 3c48bb9e56162ba5522dfccc4ab3b1564e640cad..08f3b321a24ee68353bd2d629d1f6859c1458c26 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
@@ -28,16 +28,28 @@ int main(void)
__e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
{
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)(p + 1 * 0),(size_t)10,
- (void *)p,(void *)(& p));
+ __gen_e_acsl_size = 1 * ((9 - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(p + 1 * 0),
+ (size_t)__gen_e_acsl_if,(void *)p,
+ (void *)(& p));
__e_acsl_assert(! __gen_e_acsl_valid,"Assertion","main",
"!\\valid(p + (0 .. 9))","tests/bts/bts2406.c",10);
}
/*@ assert ¬\valid(p + (0 .. 9)); */ ;
{
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& t + 1 * 0),(size_t)10,
+ __gen_e_acsl_size_2 = 1 * ((9 - 0) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& t + 1 * 0),
+ (size_t)__gen_e_acsl_if_2,
(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/format/oracle_ci/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
index 86a8665ee99080f618094bcf2f7a7024b80ca31f..09554f35c6239bf11140f87b8473afb363a08eaf 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
@@ -171,6 +171,7 @@ char *__gen_e_acsl_literal_string_12;
char *__gen_e_acsl_literal_string_35;
char *__gen_e_acsl_literal_string_9;
char *__gen_e_acsl_literal_string_6;
+char *__gen_e_acsl_literal_string_338;
char *__gen_e_acsl_literal_string_70;
char *__gen_e_acsl_literal_string_47;
char *__gen_e_acsl_literal_string_32;
@@ -491,6 +492,7 @@ void test_specifier_application(char const *allowed, char const *fmt,
size_t tmp;
unsigned long __lengthof_format;
int i;
+ __e_acsl_store_block((void *)(& fmt),(size_t)8);
__e_acsl_store_block((void *)(& allowed),(size_t)8);
tmp = __gen_e_acsl_strlen(fmt);
int len = (int)tmp;
@@ -581,6 +583,7 @@ void test_specifier_application(char const *allowed, char const *fmt,
}
__e_acsl_delete_block((void *)format);
/* __fc_vla_free((void *)format); */
+ __e_acsl_delete_block((void *)(& fmt));
__e_acsl_delete_block((void *)(& allowed));
__e_acsl_delete_block((void *)(& format));
return;
@@ -700,11 +703,13 @@ char *__gen_e_acsl_strcpy(char * __restrict dest, char const * __restrict src)
{
char *__gen_e_acsl_at;
char *__retres;
+ __e_acsl_store_block((void *)(& src),(size_t)8);
__e_acsl_store_block((void *)(& dest),(size_t)8);
__gen_e_acsl_at = dest;
__retres = strcpy(dest,src);
__e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","strcpy",
"\\result == \\old(dest)","FRAMAC_SHARE/libc/string.h",358);
+ __e_acsl_delete_block((void *)(& src));
__e_acsl_delete_block((void *)(& dest));
return __retres;
}
@@ -821,7 +826,9 @@ char *__gen_e_acsl_strchr(char const *s, int c)
size_t __gen_e_acsl_strlen(char const *s)
{
size_t __retres;
+ __e_acsl_store_block((void *)(& s),(size_t)8);
__retres = strlen(s);
+ __e_acsl_delete_block((void *)(& s));
return __retres;
}
@@ -1655,6 +1662,11 @@ void __e_acsl_globals_init(void)
sizeof("fFeEgGaA"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
+ __gen_e_acsl_literal_string_338 = "diouxfFeEgGaAcspn";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_338,
+ sizeof("diouxfFeEgGaAcspn"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_338);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_338);
__gen_e_acsl_literal_string_70 = "diouxXncsaAeEfFgG";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_70,
sizeof("diouxXncsaAeEfFgG"));
@@ -2531,6 +2543,8 @@ void __e_acsl_globals_init(void)
sizeof("% n"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_323);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_323);
+ __e_acsl_store_block((void *)(& valid_specifiers),(size_t)8);
+ __e_acsl_full_init((void *)(& valid_specifiers));
__e_acsl_store_block((void *)(& __fc_p_time_tm),(size_t)8);
__e_acsl_full_init((void *)(& __fc_p_time_tm));
__e_acsl_store_block((void *)(& __fc_time_tm),(size_t)36);
@@ -2541,6 +2555,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
+ __e_acsl_delete_block((void *)(& valid_specifiers));
__e_acsl_delete_block((void *)(& __fc_p_time_tm));
__e_acsl_delete_block((void *)(& __fc_time_tm));
}
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
index 7e9dbd5e9e4cc0ccf159e9c4c9bdbb7ba25a2110..c34d2188fe098363b7362b92d86f6bfa743eb423 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
@@ -23,8 +23,6 @@
[e-acsl] Warning: annotating undefined function `waitpid':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:351: Warning:
- E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
@@ -42,7 +40,9 @@
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:354: Warning:
- E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:351: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
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 d34788a14e92d66e46d0a3a1a20c57184474b438..9e15dfb8febf6839dcddb1f65f9d0a7d19c24353 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
@@ -36,12 +36,14 @@ int main(void)
char *b;
double t2[4];
float t3[7][2][4];
+ int t4[10][10][10];
struct S s;
int **multi_dynamic;
int i;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_store_block((void *)(& multi_dynamic),(size_t)8);
__e_acsl_store_block((void *)(& s),(size_t)24);
+ __e_acsl_store_block((void *)(t4),(size_t)4000);
__e_acsl_store_block((void *)(t3),(size_t)224);
__e_acsl_store_block((void *)(t2),(size_t)32);
__e_acsl_store_block((void *)(& b),(size_t)8);
@@ -49,9 +51,15 @@ int main(void)
__e_acsl_full_init((void *)(& a));
a = (int *)malloc((unsigned long)10 * sizeof(int));
{
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
int __gen_e_acsl_valid;
+ __gen_e_acsl_size = 4 * ((4 - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
__gen_e_acsl_valid = __e_acsl_valid((void *)((char *)a + 4 * 0),
- (size_t)20,(void *)a,(void *)(& a));
+ (size_t)__gen_e_acsl_if,(void *)a,
+ (void *)(& a));
__e_acsl_assert(__gen_e_acsl_valid,"Assertion","main",
"\\valid(a + (0 .. 4))",
"tests/memory/ranges_in_builtins.c",19);
@@ -59,9 +67,14 @@ int main(void)
/*@ assert \valid(a + (0 .. 4)); */ ;
int j = 2;
{
+ long __gen_e_acsl_size_2;
+ long __gen_e_acsl_if_2;
int __gen_e_acsl_valid_2;
+ __gen_e_acsl_size_2 = 4L * (((7L + j) - 4L) + 1L);
+ if (__gen_e_acsl_size_2 <= 0L) __gen_e_acsl_if_2 = 0L;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)a + 4 * 4),
- (size_t)(4L * (((7L + j) - 4L) + 1L)),
+ (size_t)__gen_e_acsl_if_2,
(void *)a,(void *)(& a));
__e_acsl_assert(__gen_e_acsl_valid_2,"Assertion","main",
"\\valid(a + (4 .. 7 + j))",
@@ -69,9 +82,15 @@ int main(void)
}
/*@ assert \valid(a + (4 .. 7 + j)); */ ;
{
+ int __gen_e_acsl_size_3;
+ int __gen_e_acsl_if_3;
int __gen_e_acsl_valid_3;
+ __gen_e_acsl_size_3 = 4 * ((11 - 10) + 1);
+ if (__gen_e_acsl_size_3 <= 0) __gen_e_acsl_if_3 = 0;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)((char *)a + 4 * 10),
- (size_t)8,(void *)a,(void *)(& a));
+ (size_t)__gen_e_acsl_if_3,
+ (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);
@@ -81,8 +100,14 @@ int main(void)
__e_acsl_full_init((void *)(& b));
b = (char *)malloc((unsigned long)10 * sizeof(char));
{
+ int __gen_e_acsl_size_4;
+ int __gen_e_acsl_if_4;
int __gen_e_acsl_valid_4;
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(b + 1 * 0),(size_t)10,
+ __gen_e_acsl_size_4 = 1 * ((9 - 0) + 1);
+ if (__gen_e_acsl_size_4 <= 0) __gen_e_acsl_if_4 = 0;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(b + 1 * 0),
+ (size_t)__gen_e_acsl_if_4,
(void *)b,(void *)(& b));
__e_acsl_assert(__gen_e_acsl_valid_4,"Assertion","main",
"\\valid(b + (0 .. 9))",
@@ -90,8 +115,14 @@ int main(void)
}
/*@ assert \valid(b + (0 .. 9)); */ ;
{
+ int __gen_e_acsl_size_5;
+ int __gen_e_acsl_if_5;
int __gen_e_acsl_valid_5;
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)(b + 1 * 10),(size_t)6,
+ __gen_e_acsl_size_5 = 1 * ((15 - 10) + 1);
+ if (__gen_e_acsl_size_5 <= 0) __gen_e_acsl_if_5 = 0;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)(b + 1 * 10),
+ (size_t)__gen_e_acsl_if_5,
(void *)b,(void *)(& b));
__e_acsl_assert(! __gen_e_acsl_valid_5,"Assertion","main",
"!\\valid(b + (10 .. 15))",
@@ -102,18 +133,30 @@ int main(void)
__e_acsl_store_block((void *)(t),(size_t)24);
__e_acsl_full_init((void *)(& t));
{
+ int __gen_e_acsl_size_6;
+ int __gen_e_acsl_if_6;
int __gen_e_acsl_valid_6;
+ __gen_e_acsl_size_6 = 8 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)((char *)(& t) + 8 * 0),
- (size_t)24,(void *)(& t),(void *)0);
+ (size_t)__gen_e_acsl_if_6,
+ (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);
}
/*@ assert \valid(&t[0 .. 2]); */ ;
{
+ int __gen_e_acsl_size_7;
+ int __gen_e_acsl_if_7;
int __gen_e_acsl_valid_7;
+ __gen_e_acsl_size_7 = 8 * ((5 - 3) + 1);
+ if (__gen_e_acsl_size_7 <= 0) __gen_e_acsl_if_7 = 0;
+ else __gen_e_acsl_if_7 = __gen_e_acsl_size_7;
__gen_e_acsl_valid_7 = __e_acsl_valid((void *)((char *)(& t) + 8 * 3),
- (size_t)24,(void *)(& t),(void *)0);
+ (size_t)__gen_e_acsl_if_7,
+ (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);
@@ -125,29 +168,44 @@ int main(void)
__e_acsl_initialize((void *)(& t2[1]),sizeof(double));
t2[1] = 1.5;
{
+ int __gen_e_acsl_size_8;
+ int __gen_e_acsl_if_8;
int __gen_e_acsl_initialized;
+ __gen_e_acsl_size_8 = 8 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_8 <= 0) __gen_e_acsl_if_8 = 0;
+ else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)(& t2) +
8 * 0),
- (size_t)16);
+ (size_t)__gen_e_acsl_if_8);
__e_acsl_assert(__gen_e_acsl_initialized,"Assertion","main",
"\\initialized(&t2[0 .. 1])",
"tests/memory/ranges_in_builtins.c",38);
}
/*@ assert \initialized(&t2[0 .. 1]); */ ;
{
+ int __gen_e_acsl_size_9;
+ int __gen_e_acsl_if_9;
int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_size_9 = 8 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_9 <= 0) __gen_e_acsl_if_9 = 0;
+ else __gen_e_acsl_if_9 = __gen_e_acsl_size_9;
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)((char *)(& t2) +
8 * 2),
- (size_t)16);
+ (size_t)__gen_e_acsl_if_9);
__e_acsl_assert(! __gen_e_acsl_initialized_2,"Assertion","main",
"!\\initialized(&t2[2 .. 3])",
"tests/memory/ranges_in_builtins.c",39);
}
/*@ assert ¬\initialized(&t2[2 .. 3]); */ ;
{
+ int __gen_e_acsl_size_10;
+ int __gen_e_acsl_if_10;
int __gen_e_acsl_initialized_3;
+ __gen_e_acsl_size_10 = 1 * ((9 - 0) + 1);
+ if (__gen_e_acsl_size_10 <= 0) __gen_e_acsl_if_10 = 0;
+ else __gen_e_acsl_if_10 = __gen_e_acsl_size_10;
__gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(b + 1 * 0),
- (size_t)10);
+ (size_t)__gen_e_acsl_if_10);
__e_acsl_assert(! __gen_e_acsl_initialized_3,"Assertion","main",
"!\\initialized(b + (0 .. 9))",
"tests/memory/ranges_in_builtins.c",41);
@@ -197,9 +255,15 @@ int main(void)
}
/*@ assert ¬\initialized(&t3[n - 1 .. n + 2][1][0 .. 1]); */ ;
{
+ int __gen_e_acsl_size_11;
+ int __gen_e_acsl_if_11;
int __gen_e_acsl_valid_read;
+ __gen_e_acsl_size_11 = 4 * ((10 - 2) + 1);
+ if (__gen_e_acsl_size_11 <= 0) __gen_e_acsl_if_11 = 0;
+ else __gen_e_acsl_if_11 = __gen_e_acsl_size_11;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)(& t3[6][1][0]) +
- 4 * 2),(size_t)36,
+ 4 * 2),
+ (size_t)__gen_e_acsl_if_11,
(void *)(& t3[6][1][0]),
(void *)0);
__e_acsl_assert(! __gen_e_acsl_valid_read,"Assertion","main",
@@ -234,29 +298,68 @@ int main(void)
"tests/memory/ranges_in_builtins.c",49);
}
/*@ assert \valid_read(&t3[n - 1 .. n + 2][1]); */ ;
+ {
+ int __gen_e_acsl_x;
+ int __gen_e_acsl_forall_4;
+ int __gen_e_acsl_range_4;
+ __gen_e_acsl_x = 5;
+ __gen_e_acsl_forall_4 = 1;
+ __gen_e_acsl_range_4 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_4 <= __gen_e_acsl_x) ; else break;
+ {
+ int __gen_e_acsl_valid_8;
+ __gen_e_acsl_valid_8 = __e_acsl_valid((void *)(& t4[4][__gen_e_acsl_range_4][2]),
+ sizeof(int),
+ (void *)(& t4[4][__gen_e_acsl_range_4][2]),
+ (void *)0);
+ if (__gen_e_acsl_valid_8) ;
+ else {
+ __gen_e_acsl_forall_4 = 0;
+ goto e_acsl_end_loop4;
+ }
+ }
+ __gen_e_acsl_range_4 ++;
+ }
+ e_acsl_end_loop4: ;
+ __e_acsl_assert(__gen_e_acsl_forall_4,"Assertion","main",
+ "\\let x = 5; \\valid(&t4[4][0 .. x][2])",
+ "tests/memory/ranges_in_builtins.c",52);
+ }
+ /*@ assert \let x = 5; \valid(&t4[4][0 .. x][2]); */ ;
__e_acsl_initialize((void *)(& s.a[0]),sizeof(int));
s.a[0] = 7;
__e_acsl_initialize((void *)(& s.a[1]),sizeof(int));
s.a[1] = 8;
{
+ int __gen_e_acsl_size_12;
+ int __gen_e_acsl_if_12;
int __gen_e_acsl_initialized_5;
+ __gen_e_acsl_size_12 = 4 * ((1 - 1) + 1);
+ if (__gen_e_acsl_size_12 <= 0) __gen_e_acsl_if_12 = 0;
+ else __gen_e_acsl_if_12 = __gen_e_acsl_size_12;
__gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)((char *)(& s.a[0]) +
4 * 1),
- (size_t)4);
+ (size_t)__gen_e_acsl_if_12);
__e_acsl_assert(__gen_e_acsl_initialized_5,"Assertion","main",
"\\initialized(&s.a[0] + (1 .. 1))",
- "tests/memory/ranges_in_builtins.c",53);
+ "tests/memory/ranges_in_builtins.c",56);
}
/*@ assert \initialized(&s.a[0] + (1 .. 1)); */ ;
{
+ int __gen_e_acsl_size_13;
+ int __gen_e_acsl_if_13;
int __gen_e_acsl_initialized_6;
+ __gen_e_acsl_size_13 = 4 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_13 <= 0) __gen_e_acsl_if_13 = 0;
+ else __gen_e_acsl_if_13 = __gen_e_acsl_size_13;
/*@ assert Eva: initialization: \initialized(&s.b); */
__gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)((char *)s.b +
4 * 0),
- (size_t)8);
+ (size_t)__gen_e_acsl_if_13);
__e_acsl_assert(! __gen_e_acsl_initialized_6,"Assertion","main",
"!\\initialized(s.b + (0 .. 1))",
- "tests/memory/ranges_in_builtins.c",54);
+ "tests/memory/ranges_in_builtins.c",57);
}
/*@ assert ¬\initialized(s.b + (0 .. 1)); */ ;
int size1 = 5;
@@ -272,21 +375,27 @@ int main(void)
}
{
int __gen_e_acsl_valid_read_3;
- int __gen_e_acsl_valid_8;
+ int __gen_e_acsl_size_14;
+ int __gen_e_acsl_if_14;
+ int __gen_e_acsl_valid_9;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(multi_dynamic + 4),
sizeof(int *),
(void *)multi_dynamic,
(void *)(& multi_dynamic));
__e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","main",
"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)28,
+ "tests/memory/ranges_in_builtins.c",66);
+ __gen_e_acsl_size_14 = 4 * ((7 - 1) + 1);
+ if (__gen_e_acsl_size_14 <= 0) __gen_e_acsl_if_14 = 0;
+ else __gen_e_acsl_if_14 = __gen_e_acsl_size_14;
+ __gen_e_acsl_valid_9 = __e_acsl_valid((void *)((char *)*(multi_dynamic + 4) +
+ 4 * 1),
+ (size_t)__gen_e_acsl_if_14,
(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_9,"Assertion","main",
"\\valid(*(multi_dynamic + 4) + (1 .. 7))",
- "tests/memory/ranges_in_builtins.c",63);
+ "tests/memory/ranges_in_builtins.c",66);
}
/*@ assert \valid(*(multi_dynamic + 4) + (1 .. 7)); */ ;
/*@ assert \valid(*(multi_dynamic + (2 .. 4)) + (1 .. 7)); */ ;
@@ -304,6 +413,7 @@ int main(void)
__e_acsl_delete_block((void *)(& c));
__e_acsl_delete_block((void *)(& multi_dynamic));
__e_acsl_delete_block((void *)(& s));
+ __e_acsl_delete_block((void *)(t4));
__e_acsl_delete_block((void *)(t3));
__e_acsl_delete_block((void *)(t2));
__e_acsl_delete_block((void *)(t));
@@ -321,105 +431,93 @@ void __gen_e_acsl_g(long *ptr, size_t size)
__e_acsl_mpz_t __gen_e_acsl_at_2;
long *__gen_e_acsl_at;
{
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl_sizeof;
__e_acsl_mpz_t __gen_e_acsl_size;
- __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof;
+ __e_acsl_mpz_t __gen_e_acsl_size_2;
+ __e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__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;
int __gen_e_acsl_le;
- int __gen_e_acsl_and;
- unsigned long __gen_e_acsl_size_3;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_le_2;
+ __e_acsl_mpz_t __gen_e_acsl_size_3;
+ int __gen_e_acsl_le_3;
+ unsigned long __gen_e_acsl_size_4;
int __gen_e_acsl_valid;
__e_acsl_store_block((void *)(& ptr),(size_t)8);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
__gmpz_init_set_si(__gen_e_acsl_sizeof,8L);
- __gmpz_init_set_ui(__gen_e_acsl_size,size);
- __gmpz_init_set_si(__gen_e_acsl__2,1L);
+ __gmpz_init_set_ui(__gen_e_acsl_size_2,size);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
__gmpz_init(__gen_e_acsl_sub);
__gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
__gmpz_init(__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_));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__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));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
__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_add));
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gmpz_init_set(__gen_e_acsl_size,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
if (__gen_e_acsl_le <= 0) {
- __e_acsl_mpz_t __gen_e_acsl_sizeof_2;
- __e_acsl_mpz_t __gen_e_acsl_size_2;
__e_acsl_mpz_t __gen_e_acsl__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_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;
- __gmpz_init_set_si(__gen_e_acsl_sizeof_2,8L);
- __gmpz_init_set_ui(__gen_e_acsl_size_2,size);
- __gmpz_init_set_si(__gen_e_acsl__3,1L);
- __gmpz_init(__gen_e_acsl_sub_3);
- __gmpz_sub(__gen_e_acsl_sub_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __gmpz_init_set_si(__gen_e_acsl__4,0L);
- __gmpz_init(__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__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_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));
- __gen_e_acsl_and = __gen_e_acsl_lt < 0;
- __gmpz_clear(__gen_e_acsl_sizeof_2);
- __gmpz_clear(__gen_e_acsl_size_2);
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__gmpz_clear(__gen_e_acsl__3);
- __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);
}
- else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,"RTE","g",
+ else __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gmpz_init_set_ui(__gen_e_acsl__4,18446744073709551615UL);
+ __gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __gmpz_init_set(__gen_e_acsl_size_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __e_acsl_assert(__gen_e_acsl_le_2 <= 0,"RTE","g",
"\\valid(ptr + (0 .. size - 1))",
"tests/memory/ranges_in_builtins.c",7);
- __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gen_e_acsl_size_4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
__gen_e_acsl_valid = __e_acsl_valid((void *)((char *)ptr + 8 * 0),
- __gen_e_acsl_size_3,(void *)ptr,
+ __gen_e_acsl_size_4,(void *)ptr,
(void *)(& ptr));
__e_acsl_assert(__gen_e_acsl_valid,"Precondition","g",
"\\valid(ptr + (0 .. size - 1))",
"tests/memory/ranges_in_builtins.c",7);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_sizeof);
__gmpz_clear(__gen_e_acsl_size);
- __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sizeof);
+ __gmpz_clear(__gen_e_acsl_size_2);
+ __gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__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_if);
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_size_3);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_size_8;
+ __gmpz_init_set_ui(__gen_e_acsl_size_8,size);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_8));
+ __gmpz_clear(__gen_e_acsl_size_8);
}
{
__e_acsl_mpz_t __gen_e_acsl_size_6;
@@ -428,118 +526,88 @@ void __gen_e_acsl_g(long *ptr, size_t size)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
__gmpz_clear(__gen_e_acsl_size_6);
}
- {
- __e_acsl_mpz_t __gen_e_acsl_size_5;
- __gmpz_init_set_ui(__gen_e_acsl_size_5,size);
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
- __gmpz_clear(__gen_e_acsl_size_5);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_size_4;
- __gmpz_init_set_ui(__gen_e_acsl_size_4,size);
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4));
- __gmpz_clear(__gen_e_acsl_size_4);
- }
__gen_e_acsl_at = ptr;
g(ptr,size);
{
+ __e_acsl_mpz_t __gen_e_acsl_size_5;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof_2;
__e_acsl_mpz_t __gen_e_acsl__6;
- __e_acsl_mpz_t __gen_e_acsl_sizeof_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
__e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
__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;
- unsigned long __gen_e_acsl_size_7;
+ __e_acsl_mpz_t __gen_e_acsl_mul_2;
+ int __gen_e_acsl_le_4;
+ __e_acsl_mpz_t __gen_e_acsl_if_2;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_le_5;
+ __e_acsl_mpz_t __gen_e_acsl_size_7;
+ int __gen_e_acsl_le_6;
+ unsigned long __gen_e_acsl_size_9;
int __gen_e_acsl_valid_2;
- __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_3);
- __gmpz_add(__gen_e_acsl_add_3,
+ __gmpz_init_set_si(__gen_e_acsl_sizeof_2,8L);
+ __gmpz_init_set_si(__gen_e_acsl__6,1L);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
(__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_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),
+ __gmpz_init_set_si(__gen_e_acsl__7,0L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
(__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_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;
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __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_add_3));
+ __gmpz_init_set(__gen_e_acsl_size_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2));
+ __gen_e_acsl_le_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ if (__gen_e_acsl_le_4 <= 0) {
__e_acsl_mpz_t __gen_e_acsl__8;
- __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_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_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_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_init_set_si(__gen_e_acsl__8,0L);
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__gmpz_clear(__gen_e_acsl__8);
- __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);
}
- else __gen_e_acsl_and_2 = 0;
- __e_acsl_assert(__gen_e_acsl_and_2,"RTE","g",
+ else __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_5));
+ __gmpz_init_set_ui(__gen_e_acsl__9,18446744073709551615UL);
+ __gen_e_acsl_le_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __gmpz_init_set(__gen_e_acsl_size_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2));
+ __gen_e_acsl_le_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __e_acsl_assert(__gen_e_acsl_le_5 <= 0,"RTE","g",
"\\valid(\\old(ptr) + (0 .. \\old(size) + 1))",
"tests/memory/ranges_in_builtins.c",8);
- __gen_e_acsl_size_7 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
+ __gen_e_acsl_size_9 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)__gen_e_acsl_at +
8 * 0),
- __gen_e_acsl_size_7,
+ __gen_e_acsl_size_9,
(void *)__gen_e_acsl_at,
(void *)(& __gen_e_acsl_at));
__e_acsl_assert(! __gen_e_acsl_valid_2,"Postcondition","g",
"!\\valid(\\old(ptr) + (0 .. \\old(size) + 1))",
"tests/memory/ranges_in_builtins.c",8);
__e_acsl_delete_block((void *)(& ptr));
+ __gmpz_clear(__gen_e_acsl_size_5);
+ __gmpz_clear(__gen_e_acsl_sizeof_2);
__gmpz_clear(__gen_e_acsl__6);
- __gmpz_clear(__gen_e_acsl_sizeof_3);
+ __gmpz_clear(__gen_e_acsl_add_2);
__gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl_sub_3);
__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_mul_2);
+ __gmpz_clear(__gen_e_acsl_if_2);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_size_7);
__gmpz_clear(__gen_e_acsl_at_2);
return;
}
@@ -549,114 +617,92 @@ void __gen_e_acsl_g(long *ptr, size_t size)
void __gen_e_acsl_f(char *s, long n)
{
{
- __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_size;
__e_acsl_mpz_t __gen_e_acsl_sizeof;
__e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_add;
- __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl__2;
__e_acsl_mpz_t __gen_e_acsl_sub;
- __e_acsl_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl__3;
__e_acsl_mpz_t __gen_e_acsl_add_2;
__e_acsl_mpz_t __gen_e_acsl_mul;
+ __e_acsl_mpz_t __gen_e_acsl__4;
int __gen_e_acsl_le;
- int __gen_e_acsl_and;
- unsigned long __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ int __gen_e_acsl_le_2;
+ __e_acsl_mpz_t __gen_e_acsl_size_2;
+ int __gen_e_acsl_le_3;
+ unsigned long __gen_e_acsl_size_3;
int __gen_e_acsl_valid;
__e_acsl_store_block((void *)(& s),(size_t)8);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
__gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
__gmpz_init_set_si(__gen_e_acsl_n,n);
- __gmpz_init_set_si(__gen_e_acsl__2,1000L);
+ __gmpz_init_set_si(__gen_e_acsl_,1000L);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_init_set_si(__gen_e_acsl__3,3L);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_si(__gen_e_acsl__2,3L);
__gmpz_init(__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__3));
- __gmpz_init_set_si(__gen_e_acsl__4,1L);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init_set_si(__gen_e_acsl__3,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));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__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_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));
+ __gmpz_init_set(__gen_e_acsl_size,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
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__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__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__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__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_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_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__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_init_set_si(__gen_e_acsl__5,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__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__7);
- __gmpz_clear(__gen_e_acsl_add_4);
- __gmpz_clear(__gen_e_acsl_mul_2);
- __gmpz_clear(__gen_e_acsl__8);
}
- else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,"RTE","f",
+ else __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gmpz_init_set_ui(__gen_e_acsl__6,18446744073709551615UL);
+ __gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init_set(__gen_e_acsl_size_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert(__gen_e_acsl_le_2 <= 0,"RTE","f",
"\\valid(s + (3 .. n + 1000))",
"tests/memory/ranges_in_builtins.c",5);
- __gen_e_acsl_size = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
__gen_e_acsl_valid = __e_acsl_valid((void *)(s + 1 * 3),
- __gen_e_acsl_size,(void *)s,
+ __gen_e_acsl_size_3,(void *)s,
(void *)(& s));
__e_acsl_assert(! __gen_e_acsl_valid,"Precondition","f",
"!\\valid(s + (3 .. n + 1000))",
"tests/memory/ranges_in_builtins.c",5);
- __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_size);
__gmpz_clear(__gen_e_acsl_sizeof);
__gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_add);
- __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl__2);
__gmpz_clear(__gen_e_acsl_sub);
- __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl__3);
__gmpz_clear(__gen_e_acsl_add_2);
__gmpz_clear(__gen_e_acsl_mul);
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_if);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_size_2);
}
f(s,n);
__e_acsl_delete_block((void *)(& s));
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c
index 6a5a747d509ac2596667b6f684ccf9e640a62b0f..10644067af706030bda70f5b9223838e183558e8 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
@@ -49,9 +50,8 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","main",
"separated_guard: \\valid_read(&c)",
"tests/memory/separated.c",14);
- __gen_e_acsl_separated = __e_acsl_separated((size_t)3,(void *)(& c),
- sizeof(int),(void *)(& b),
- sizeof(int),(void *)(& a),
+ __gen_e_acsl_separated = __e_acsl_separated((size_t)3,& a,sizeof(int),
+ & b,sizeof(int),& c,
sizeof(int));
__e_acsl_assert(__gen_e_acsl_separated,"Assertion","main",
"\\separated(&a, &b, &c)","tests/memory/separated.c",
@@ -104,13 +104,10 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_and,"RTE","main",
"separated_guard: \\valid_read(d)",
"tests/memory/separated.c",15);
- __gen_e_acsl_separated_2 = __e_acsl_separated((size_t)4,(void *)d,
- sizeof(int),
- (void *)(& c),
- sizeof(int),
- (void *)(& b),
- sizeof(int),
- (void *)(& a),
+ __gen_e_acsl_separated_2 = __e_acsl_separated((size_t)4,& a,
+ sizeof(int),& b,
+ sizeof(int),& c,
+ sizeof(int),d,
sizeof(int));
__e_acsl_assert(! __gen_e_acsl_separated_2,"Assertion","main",
"!\\separated(&a, &b, &c, d)",
@@ -127,96 +124,156 @@ int main(void)
__e_acsl_store_block((void *)(array),(size_t)160);
__e_acsl_full_init((void *)(& array));
{
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
int __gen_e_acsl_valid_read_8;
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
int __gen_e_acsl_valid_read_9;
+ int __gen_e_acsl_size_3;
+ int __gen_e_acsl_if_3;
+ int __gen_e_acsl_size_4;
+ int __gen_e_acsl_if_4;
int __gen_e_acsl_separated_3;
+ __gen_e_acsl_size = 8 * ((9 - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
__gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 0),
- (size_t)80,
+ (size_t)__gen_e_acsl_if,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 9]); */
__e_acsl_assert(__gen_e_acsl_valid_read_8,"RTE","main",
"separated_guard: \\valid_read(&array[0 .. 9])",
"tests/memory/separated.c",21);
+ __gen_e_acsl_size_2 = 8 * ((19 - 10) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
__gen_e_acsl_valid_read_9 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 10),
- (size_t)80,
+ (size_t)__gen_e_acsl_if_2,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[10 .. 19]); */
__e_acsl_assert(__gen_e_acsl_valid_read_9,"RTE","main",
"separated_guard: \\valid_read(&array[10 .. 19])",
"tests/memory/separated.c",21);
+ __gen_e_acsl_size_3 = 8 * ((9 - 0) + 1);
+ if (__gen_e_acsl_size_3 <= 0) __gen_e_acsl_if_3 = 0;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_size_4 = 8 * ((19 - 10) + 1);
+ if (__gen_e_acsl_size_4 <= 0) __gen_e_acsl_if_4 = 0;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
__gen_e_acsl_separated_3 = __e_acsl_separated((size_t)2,
- (void *)((char *)(& array) +
- 8 * 10),80,
- (void *)((char *)(& array) +
- 8 * 0),80);
+ (char *)(& array) + 8 * 0,
+ __gen_e_acsl_if_3,
+ (char *)(& array) +
+ 8 * 10,__gen_e_acsl_if_4);
__e_acsl_assert(__gen_e_acsl_separated_3,"Assertion","main",
"\\separated(&array[0 .. 9], &array[10 .. 19])",
"tests/memory/separated.c",21);
}
/*@ assert \separated(&array[0 .. 9], &array[10 .. 19]); */ ;
{
+ int __gen_e_acsl_size_5;
+ int __gen_e_acsl_if_5;
int __gen_e_acsl_valid_read_10;
+ int __gen_e_acsl_size_6;
+ int __gen_e_acsl_if_6;
int __gen_e_acsl_valid_read_11;
+ int __gen_e_acsl_size_7;
+ int __gen_e_acsl_if_7;
+ int __gen_e_acsl_size_8;
+ int __gen_e_acsl_if_8;
int __gen_e_acsl_separated_4;
+ __gen_e_acsl_size_5 = 8 * ((10 - 0) + 1);
+ if (__gen_e_acsl_size_5 <= 0) __gen_e_acsl_if_5 = 0;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
__gen_e_acsl_valid_read_10 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 0),
- (size_t)88,
+ (size_t)__gen_e_acsl_if_5,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 10]); */
__e_acsl_assert(__gen_e_acsl_valid_read_10,"RTE","main",
"separated_guard: \\valid_read(&array[0 .. 10])",
"tests/memory/separated.c",22);
+ __gen_e_acsl_size_6 = 8 * ((15 - 5) + 1);
+ if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
__gen_e_acsl_valid_read_11 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 5),
- (size_t)88,
+ (size_t)__gen_e_acsl_if_6,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[5 .. 15]); */
__e_acsl_assert(__gen_e_acsl_valid_read_11,"RTE","main",
"separated_guard: \\valid_read(&array[5 .. 15])",
"tests/memory/separated.c",22);
+ __gen_e_acsl_size_7 = 8 * ((10 - 0) + 1);
+ if (__gen_e_acsl_size_7 <= 0) __gen_e_acsl_if_7 = 0;
+ else __gen_e_acsl_if_7 = __gen_e_acsl_size_7;
+ __gen_e_acsl_size_8 = 8 * ((15 - 5) + 1);
+ if (__gen_e_acsl_size_8 <= 0) __gen_e_acsl_if_8 = 0;
+ else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
__gen_e_acsl_separated_4 = __e_acsl_separated((size_t)2,
- (void *)((char *)(& array) +
- 8 * 5),88,
- (void *)((char *)(& array) +
- 8 * 0),88);
+ (char *)(& array) + 8 * 0,
+ __gen_e_acsl_if_7,
+ (char *)(& array) + 8 * 5,
+ __gen_e_acsl_if_8);
__e_acsl_assert(! __gen_e_acsl_separated_4,"Assertion","main",
"!\\separated(&array[0 .. 10], &array[5 .. 15])",
"tests/memory/separated.c",22);
}
/*@ assert ¬\separated(&array[0 .. 10], &array[5 .. 15]); */ ;
{
+ int __gen_e_acsl_size_9;
+ int __gen_e_acsl_if_9;
int __gen_e_acsl_valid_read_12;
+ int __gen_e_acsl_size_10;
+ int __gen_e_acsl_if_10;
int __gen_e_acsl_valid_read_13;
+ int __gen_e_acsl_size_11;
+ int __gen_e_acsl_if_11;
+ int __gen_e_acsl_size_12;
+ int __gen_e_acsl_if_12;
int __gen_e_acsl_separated_5;
+ __gen_e_acsl_size_9 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_9 <= 0) __gen_e_acsl_if_9 = 0;
+ else __gen_e_acsl_if_9 = __gen_e_acsl_size_9;
__gen_e_acsl_valid_read_12 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 0),
- (size_t)160,
+ (size_t)__gen_e_acsl_if_9,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 19]); */
__e_acsl_assert(__gen_e_acsl_valid_read_12,"RTE","main",
"separated_guard: \\valid_read(&array[0 .. 19])",
"tests/memory/separated.c",23);
+ __gen_e_acsl_size_10 = 8 * ((15 - 5) + 1);
+ if (__gen_e_acsl_size_10 <= 0) __gen_e_acsl_if_10 = 0;
+ else __gen_e_acsl_if_10 = __gen_e_acsl_size_10;
__gen_e_acsl_valid_read_13 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 5),
- (size_t)88,
+ (size_t)__gen_e_acsl_if_10,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[5 .. 15]); */
__e_acsl_assert(__gen_e_acsl_valid_read_13,"RTE","main",
"separated_guard: \\valid_read(&array[5 .. 15])",
"tests/memory/separated.c",23);
+ __gen_e_acsl_size_11 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_11 <= 0) __gen_e_acsl_if_11 = 0;
+ else __gen_e_acsl_if_11 = __gen_e_acsl_size_11;
+ __gen_e_acsl_size_12 = 8 * ((15 - 5) + 1);
+ if (__gen_e_acsl_size_12 <= 0) __gen_e_acsl_if_12 = 0;
+ else __gen_e_acsl_if_12 = __gen_e_acsl_size_12;
__gen_e_acsl_separated_5 = __e_acsl_separated((size_t)2,
- (void *)((char *)(& array) +
- 8 * 5),88,
- (void *)((char *)(& array) +
- 8 * 0),160);
+ (char *)(& array) + 8 * 0,
+ __gen_e_acsl_if_11,
+ (char *)(& array) + 8 * 5,
+ __gen_e_acsl_if_12);
__e_acsl_assert(! __gen_e_acsl_separated_5,"Assertion","main",
"!\\separated(&array[0 .. 19], &array[5 .. 15])",
"tests/memory/separated.c",23);
@@ -242,10 +299,9 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_valid_read_15,"RTE","main",
"separated_guard: \\valid_read(&array[1])",
"tests/memory/separated.c",24);
- __gen_e_acsl_separated_6 = __e_acsl_separated((size_t)2,
- (void *)(& array[1]),
+ __gen_e_acsl_separated_6 = __e_acsl_separated((size_t)2,array,
sizeof(double),
- (void *)(array),
+ & array[1],
sizeof(double));
__e_acsl_assert(__gen_e_acsl_separated_6,"Assertion","main",
"\\separated((double *)array, &array[1])",
@@ -253,37 +309,162 @@ int main(void)
}
/*@ assert \separated((double *)array, &array[1]); */ ;
{
+ int __gen_e_acsl_size_13;
+ int __gen_e_acsl_if_13;
int __gen_e_acsl_valid_read_16;
+ int __gen_e_acsl_size_14;
+ int __gen_e_acsl_if_14;
int __gen_e_acsl_valid_read_17;
+ int __gen_e_acsl_size_15;
+ int __gen_e_acsl_if_15;
+ int __gen_e_acsl_size_16;
+ int __gen_e_acsl_if_16;
int __gen_e_acsl_separated_7;
+ __gen_e_acsl_size_13 = 8 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_13 <= 0) __gen_e_acsl_if_13 = 0;
+ else __gen_e_acsl_if_13 = __gen_e_acsl_size_13;
__gen_e_acsl_valid_read_16 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 0),
- (size_t)16,
+ (size_t)__gen_e_acsl_if_13,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 1]); */
__e_acsl_assert(__gen_e_acsl_valid_read_16,"RTE","main",
"separated_guard: \\valid_read(&array[0 .. 1])",
"tests/memory/separated.c",25);
+ __gen_e_acsl_size_14 = 8 * ((2 - 1) + 1);
+ if (__gen_e_acsl_size_14 <= 0) __gen_e_acsl_if_14 = 0;
+ else __gen_e_acsl_if_14 = __gen_e_acsl_size_14;
__gen_e_acsl_valid_read_17 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 1),
- (size_t)16,
+ (size_t)__gen_e_acsl_if_14,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[1 .. 2]); */
__e_acsl_assert(__gen_e_acsl_valid_read_17,"RTE","main",
"separated_guard: \\valid_read(&array[1 .. 2])",
"tests/memory/separated.c",25);
+ __gen_e_acsl_size_15 = 8 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_15 <= 0) __gen_e_acsl_if_15 = 0;
+ else __gen_e_acsl_if_15 = __gen_e_acsl_size_15;
+ __gen_e_acsl_size_16 = 8 * ((2 - 1) + 1);
+ if (__gen_e_acsl_size_16 <= 0) __gen_e_acsl_if_16 = 0;
+ else __gen_e_acsl_if_16 = __gen_e_acsl_size_16;
__gen_e_acsl_separated_7 = __e_acsl_separated((size_t)2,
- (void *)((char *)(& array) +
- 8 * 1),16,
- (void *)((char *)(& array) +
- 8 * 0),16);
+ (char *)(& array) + 8 * 0,
+ __gen_e_acsl_if_15,
+ (char *)(& array) + 8 * 1,
+ __gen_e_acsl_if_16);
__e_acsl_assert(! __gen_e_acsl_separated_7,"Assertion","main",
"!\\separated(&array[0 .. 1], &array[1 .. 2])",
"tests/memory/separated.c",25);
}
/*@ assert ¬\separated(&array[0 .. 1], &array[1 .. 2]); */ ;
+ {
+ int __gen_e_acsl_size_17;
+ int __gen_e_acsl_if_17;
+ int __gen_e_acsl_valid_read_18;
+ int __gen_e_acsl_size_18;
+ int __gen_e_acsl_if_18;
+ int __gen_e_acsl_valid_read_19;
+ int __gen_e_acsl_size_19;
+ int __gen_e_acsl_if_19;
+ int __gen_e_acsl_size_20;
+ int __gen_e_acsl_if_20;
+ int __gen_e_acsl_separated_8;
+ __gen_e_acsl_size_17 = 8 * ((5 - 15) + 1);
+ if (__gen_e_acsl_size_17 <= 0) __gen_e_acsl_if_17 = 0;
+ else __gen_e_acsl_if_17 = __gen_e_acsl_size_17;
+ __gen_e_acsl_valid_read_18 = __e_acsl_valid_read((void *)((char *)(& array) +
+ 8 * 15),
+ (size_t)__gen_e_acsl_if_17,
+ (void *)(& array),
+ (void *)0);
+ /*@ assert E_ACSL: separated_guard: \valid_read(&array[15 .. 5]); */
+ __e_acsl_assert(__gen_e_acsl_valid_read_18,"RTE","main",
+ "separated_guard: \\valid_read(&array[15 .. 5])",
+ "tests/memory/separated.c",26);
+ __gen_e_acsl_size_18 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_18 <= 0) __gen_e_acsl_if_18 = 0;
+ else __gen_e_acsl_if_18 = __gen_e_acsl_size_18;
+ __gen_e_acsl_valid_read_19 = __e_acsl_valid_read((void *)((char *)(& array) +
+ 8 * 0),
+ (size_t)__gen_e_acsl_if_18,
+ (void *)(& array),
+ (void *)0);
+ /*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 19]); */
+ __e_acsl_assert(__gen_e_acsl_valid_read_19,"RTE","main",
+ "separated_guard: \\valid_read(&array[0 .. 19])",
+ "tests/memory/separated.c",26);
+ __gen_e_acsl_size_19 = 8 * ((5 - 15) + 1);
+ if (__gen_e_acsl_size_19 <= 0) __gen_e_acsl_if_19 = 0;
+ else __gen_e_acsl_if_19 = __gen_e_acsl_size_19;
+ __gen_e_acsl_size_20 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_20 <= 0) __gen_e_acsl_if_20 = 0;
+ else __gen_e_acsl_if_20 = __gen_e_acsl_size_20;
+ __gen_e_acsl_separated_8 = __e_acsl_separated((size_t)2,
+ (char *)(& array) +
+ 8 * 15,
+ __gen_e_acsl_if_19,
+ (char *)(& array) + 8 * 0,
+ __gen_e_acsl_if_20);
+ __e_acsl_assert(__gen_e_acsl_separated_8,"Assertion","main",
+ "\\separated(&array[15 .. 5], &array[0 .. 19])",
+ "tests/memory/separated.c",26);
+ }
+ /*@ assert \separated(&array[15 .. 5], &array[0 .. 19]); */ ;
+ {
+ int __gen_e_acsl_size_21;
+ int __gen_e_acsl_if_21;
+ int __gen_e_acsl_valid_read_20;
+ int __gen_e_acsl_size_22;
+ int __gen_e_acsl_if_22;
+ int __gen_e_acsl_valid_read_21;
+ int __gen_e_acsl_size_23;
+ int __gen_e_acsl_if_23;
+ int __gen_e_acsl_size_24;
+ int __gen_e_acsl_if_24;
+ int __gen_e_acsl_separated_9;
+ __gen_e_acsl_size_21 = 8 * ((-3 - 0) + 1);
+ if (__gen_e_acsl_size_21 <= 0) __gen_e_acsl_if_21 = 0;
+ else __gen_e_acsl_if_21 = __gen_e_acsl_size_21;
+ __gen_e_acsl_valid_read_20 = __e_acsl_valid_read((void *)((char *)(& array) +
+ 8 * 0),
+ (size_t)__gen_e_acsl_if_21,
+ (void *)(& array),
+ (void *)0);
+ /*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. -3]); */
+ __e_acsl_assert(__gen_e_acsl_valid_read_20,"RTE","main",
+ "separated_guard: \\valid_read(&array[0 .. -3])",
+ "tests/memory/separated.c",27);
+ __gen_e_acsl_size_22 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_22 <= 0) __gen_e_acsl_if_22 = 0;
+ else __gen_e_acsl_if_22 = __gen_e_acsl_size_22;
+ __gen_e_acsl_valid_read_21 = __e_acsl_valid_read((void *)((char *)(& array) +
+ 8 * 0),
+ (size_t)__gen_e_acsl_if_22,
+ (void *)(& array),
+ (void *)0);
+ /*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 19]); */
+ __e_acsl_assert(__gen_e_acsl_valid_read_21,"RTE","main",
+ "separated_guard: \\valid_read(&array[0 .. 19])",
+ "tests/memory/separated.c",27);
+ __gen_e_acsl_size_23 = 8 * ((-3 - 0) + 1);
+ if (__gen_e_acsl_size_23 <= 0) __gen_e_acsl_if_23 = 0;
+ else __gen_e_acsl_if_23 = __gen_e_acsl_size_23;
+ __gen_e_acsl_size_24 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_24 <= 0) __gen_e_acsl_if_24 = 0;
+ else __gen_e_acsl_if_24 = __gen_e_acsl_size_24;
+ __gen_e_acsl_separated_9 = __e_acsl_separated((size_t)2,
+ (char *)(& array) + 8 * 0,
+ __gen_e_acsl_if_23,
+ (char *)(& array) + 8 * 0,
+ __gen_e_acsl_if_24);
+ __e_acsl_assert(__gen_e_acsl_separated_9,"Assertion","main",
+ "\\separated(&array[0 .. -3], &array[0 .. 19])",
+ "tests/memory/separated.c",27);
+ }
+ /*@ assert \separated(&array[0 .. -3], &array[0 .. 19]); */ ;
__e_acsl_delete_block((void *)(array));
}
{
@@ -301,42 +482,42 @@ int main(void)
int __gen_e_acsl_and_2;
int __gen_e_acsl_initialized_3;
int __gen_e_acsl_and_3;
- int __gen_e_acsl_separated_8;
+ int __gen_e_acsl_separated_10;
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& a_0),
sizeof(int *));
if (__gen_e_acsl_initialized_2) {
- int __gen_e_acsl_valid_read_18;
- __gen_e_acsl_valid_read_18 = __e_acsl_valid_read((void *)a_0,
+ int __gen_e_acsl_valid_read_22;
+ __gen_e_acsl_valid_read_22 = __e_acsl_valid_read((void *)a_0,
sizeof(int),
(void *)a_0,
(void *)(& a_0));
- __gen_e_acsl_and_2 = __gen_e_acsl_valid_read_18;
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_read_22;
}
else __gen_e_acsl_and_2 = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(a_0); */
__e_acsl_assert(__gen_e_acsl_and_2,"RTE","main",
"separated_guard: \\valid_read(a_0)",
- "tests/memory/separated.c",34);
+ "tests/memory/separated.c",36);
__gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& b_0),
sizeof(int *));
if (__gen_e_acsl_initialized_3) {
- int __gen_e_acsl_valid_read_19;
- __gen_e_acsl_valid_read_19 = __e_acsl_valid_read((void *)b_0,
+ int __gen_e_acsl_valid_read_23;
+ __gen_e_acsl_valid_read_23 = __e_acsl_valid_read((void *)b_0,
sizeof(int),
(void *)b_0,
(void *)(& b_0));
- __gen_e_acsl_and_3 = __gen_e_acsl_valid_read_19;
+ __gen_e_acsl_and_3 = __gen_e_acsl_valid_read_23;
}
else __gen_e_acsl_and_3 = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(b_0); */
__e_acsl_assert(__gen_e_acsl_and_3,"RTE","main",
"separated_guard: \\valid_read(b_0)",
- "tests/memory/separated.c",34);
- __gen_e_acsl_separated_8 = __e_acsl_separated((size_t)2,(void *)b_0,
- sizeof(int),(void *)a_0,
- sizeof(int));
- __e_acsl_assert(__gen_e_acsl_separated_8,"Assertion","main",
- "\\separated(a_0, b_0)","tests/memory/separated.c",34);
+ "tests/memory/separated.c",36);
+ __gen_e_acsl_separated_10 = __e_acsl_separated((size_t)2,a_0,
+ sizeof(int),b_0,
+ sizeof(int));
+ __e_acsl_assert(__gen_e_acsl_separated_10,"Assertion","main",
+ "\\separated(a_0, b_0)","tests/memory/separated.c",36);
}
/*@ assert \separated(a_0, b_0); */ ;
{
@@ -346,59 +527,59 @@ int main(void)
int __gen_e_acsl_and_5;
int __gen_e_acsl_initialized_6;
int __gen_e_acsl_and_6;
- int __gen_e_acsl_separated_9;
+ int __gen_e_acsl_separated_11;
__gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& a_0),
sizeof(int *));
if (__gen_e_acsl_initialized_4) {
- int __gen_e_acsl_valid_read_20;
- __gen_e_acsl_valid_read_20 = __e_acsl_valid_read((void *)a_0,
+ int __gen_e_acsl_valid_read_24;
+ __gen_e_acsl_valid_read_24 = __e_acsl_valid_read((void *)a_0,
sizeof(int),
(void *)a_0,
(void *)(& a_0));
- __gen_e_acsl_and_4 = __gen_e_acsl_valid_read_20;
+ __gen_e_acsl_and_4 = __gen_e_acsl_valid_read_24;
}
else __gen_e_acsl_and_4 = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(a_0); */
__e_acsl_assert(__gen_e_acsl_and_4,"RTE","main",
"separated_guard: \\valid_read(a_0)",
- "tests/memory/separated.c",35);
+ "tests/memory/separated.c",37);
__gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& b_0),
sizeof(int *));
if (__gen_e_acsl_initialized_5) {
- int __gen_e_acsl_valid_read_21;
- __gen_e_acsl_valid_read_21 = __e_acsl_valid_read((void *)b_0,
+ int __gen_e_acsl_valid_read_25;
+ __gen_e_acsl_valid_read_25 = __e_acsl_valid_read((void *)b_0,
sizeof(int),
(void *)b_0,
(void *)(& b_0));
- __gen_e_acsl_and_5 = __gen_e_acsl_valid_read_21;
+ __gen_e_acsl_and_5 = __gen_e_acsl_valid_read_25;
}
else __gen_e_acsl_and_5 = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(b_0); */
__e_acsl_assert(__gen_e_acsl_and_5,"RTE","main",
"separated_guard: \\valid_read(b_0)",
- "tests/memory/separated.c",35);
+ "tests/memory/separated.c",37);
__gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& c_0),
sizeof(int *));
if (__gen_e_acsl_initialized_6) {
- int __gen_e_acsl_valid_read_22;
- __gen_e_acsl_valid_read_22 = __e_acsl_valid_read((void *)c_0,
+ int __gen_e_acsl_valid_read_26;
+ __gen_e_acsl_valid_read_26 = __e_acsl_valid_read((void *)c_0,
sizeof(int),
(void *)c_0,
(void *)(& c_0));
- __gen_e_acsl_and_6 = __gen_e_acsl_valid_read_22;
+ __gen_e_acsl_and_6 = __gen_e_acsl_valid_read_26;
}
else __gen_e_acsl_and_6 = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(c_0); */
__e_acsl_assert(__gen_e_acsl_and_6,"RTE","main",
"separated_guard: \\valid_read(c_0)",
- "tests/memory/separated.c",35);
- __gen_e_acsl_separated_9 = __e_acsl_separated((size_t)3,(void *)c_0,
- sizeof(int),(void *)b_0,
- sizeof(int),(void *)a_0,
- sizeof(int));
- __e_acsl_assert(! __gen_e_acsl_separated_9,"Assertion","main",
+ "tests/memory/separated.c",37);
+ __gen_e_acsl_separated_11 = __e_acsl_separated((size_t)3,a_0,
+ sizeof(int),b_0,
+ sizeof(int),c_0,
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_separated_11,"Assertion","main",
"!\\separated(a_0, b_0, c_0)",
- "tests/memory/separated.c",35);
+ "tests/memory/separated.c",37);
}
/*@ assert ¬\separated(a_0, b_0, c_0); */ ;
free((void *)a_0);
@@ -412,171 +593,1209 @@ int main(void)
__e_acsl_store_block((void *)(& array_0),(size_t)8);
__e_acsl_full_init((void *)(& array_0));
{
- int __gen_e_acsl_valid_read_23;
- int __gen_e_acsl_valid_read_24;
- int __gen_e_acsl_separated_10;
- __gen_e_acsl_valid_read_23 = __e_acsl_valid_read((void *)((char *)array_0 +
+ int __gen_e_acsl_size_25;
+ int __gen_e_acsl_if_25;
+ int __gen_e_acsl_valid_read_27;
+ int __gen_e_acsl_size_26;
+ int __gen_e_acsl_if_26;
+ int __gen_e_acsl_valid_read_28;
+ int __gen_e_acsl_size_27;
+ int __gen_e_acsl_if_27;
+ int __gen_e_acsl_size_28;
+ int __gen_e_acsl_if_28;
+ int __gen_e_acsl_separated_12;
+ __gen_e_acsl_size_25 = 8 * ((9 - 0) + 1);
+ if (__gen_e_acsl_size_25 <= 0) __gen_e_acsl_if_25 = 0;
+ else __gen_e_acsl_if_25 = __gen_e_acsl_size_25;
+ __gen_e_acsl_valid_read_27 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 0),
- (size_t)80,
+ (size_t)__gen_e_acsl_if_25,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. 9)); */
- __e_acsl_assert(__gen_e_acsl_valid_read_23,"RTE","main",
+ __e_acsl_assert(__gen_e_acsl_valid_read_27,"RTE","main",
"separated_guard: \\valid_read(array_0 + (0 .. 9))",
- "tests/memory/separated.c",44);
- __gen_e_acsl_valid_read_24 = __e_acsl_valid_read((void *)((char *)array_0 +
+ "tests/memory/separated.c",46);
+ __gen_e_acsl_size_26 = 8 * ((19 - 10) + 1);
+ if (__gen_e_acsl_size_26 <= 0) __gen_e_acsl_if_26 = 0;
+ else __gen_e_acsl_if_26 = __gen_e_acsl_size_26;
+ __gen_e_acsl_valid_read_28 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 10),
- (size_t)80,
+ (size_t)__gen_e_acsl_if_26,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (10 .. 19));
*/
- __e_acsl_assert(__gen_e_acsl_valid_read_24,"RTE","main",
+ __e_acsl_assert(__gen_e_acsl_valid_read_28,"RTE","main",
"separated_guard: \\valid_read(array_0 + (10 .. 19))",
- "tests/memory/separated.c",44);
- __gen_e_acsl_separated_10 = __e_acsl_separated((size_t)2,
- (void *)((char *)array_0 +
- 8 * 10),80,
- (void *)((char *)array_0 +
- 8 * 0),80);
- __e_acsl_assert(__gen_e_acsl_separated_10,"Assertion","main",
+ "tests/memory/separated.c",46);
+ __gen_e_acsl_size_27 = 8 * ((9 - 0) + 1);
+ if (__gen_e_acsl_size_27 <= 0) __gen_e_acsl_if_27 = 0;
+ else __gen_e_acsl_if_27 = __gen_e_acsl_size_27;
+ __gen_e_acsl_size_28 = 8 * ((19 - 10) + 1);
+ if (__gen_e_acsl_size_28 <= 0) __gen_e_acsl_if_28 = 0;
+ else __gen_e_acsl_if_28 = __gen_e_acsl_size_28;
+ __gen_e_acsl_separated_12 = __e_acsl_separated((size_t)2,
+ (char *)array_0 + 8 * 0,
+ __gen_e_acsl_if_27,
+ (char *)array_0 + 8 * 10,
+ __gen_e_acsl_if_28);
+ __e_acsl_assert(__gen_e_acsl_separated_12,"Assertion","main",
"\\separated(array_0 + (0 .. 9), array_0 + (10 .. 19))",
- "tests/memory/separated.c",44);
+ "tests/memory/separated.c",46);
}
/*@ assert \separated(array_0 + (0 .. 9), array_0 + (10 .. 19)); */ ;
{
- int __gen_e_acsl_valid_read_25;
- int __gen_e_acsl_valid_read_26;
- int __gen_e_acsl_separated_11;
- __gen_e_acsl_valid_read_25 = __e_acsl_valid_read((void *)((char *)array_0 +
+ int __gen_e_acsl_size_29;
+ int __gen_e_acsl_if_29;
+ int __gen_e_acsl_valid_read_29;
+ int __gen_e_acsl_size_30;
+ int __gen_e_acsl_if_30;
+ int __gen_e_acsl_valid_read_30;
+ int __gen_e_acsl_size_31;
+ int __gen_e_acsl_if_31;
+ int __gen_e_acsl_size_32;
+ int __gen_e_acsl_if_32;
+ int __gen_e_acsl_separated_13;
+ __gen_e_acsl_size_29 = 8 * ((10 - 0) + 1);
+ if (__gen_e_acsl_size_29 <= 0) __gen_e_acsl_if_29 = 0;
+ else __gen_e_acsl_if_29 = __gen_e_acsl_size_29;
+ __gen_e_acsl_valid_read_29 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 0),
- (size_t)88,
+ (size_t)__gen_e_acsl_if_29,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. 10));
*/
- __e_acsl_assert(__gen_e_acsl_valid_read_25,"RTE","main",
+ __e_acsl_assert(__gen_e_acsl_valid_read_29,"RTE","main",
"separated_guard: \\valid_read(array_0 + (0 .. 10))",
- "tests/memory/separated.c",45);
- __gen_e_acsl_valid_read_26 = __e_acsl_valid_read((void *)((char *)array_0 +
+ "tests/memory/separated.c",47);
+ __gen_e_acsl_size_30 = 8 * ((15 - 5) + 1);
+ if (__gen_e_acsl_size_30 <= 0) __gen_e_acsl_if_30 = 0;
+ else __gen_e_acsl_if_30 = __gen_e_acsl_size_30;
+ __gen_e_acsl_valid_read_30 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 5),
- (size_t)88,
+ (size_t)__gen_e_acsl_if_30,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (5 .. 15));
*/
- __e_acsl_assert(__gen_e_acsl_valid_read_26,"RTE","main",
+ __e_acsl_assert(__gen_e_acsl_valid_read_30,"RTE","main",
"separated_guard: \\valid_read(array_0 + (5 .. 15))",
- "tests/memory/separated.c",45);
- __gen_e_acsl_separated_11 = __e_acsl_separated((size_t)2,
- (void *)((char *)array_0 +
- 8 * 5),88,
- (void *)((char *)array_0 +
- 8 * 0),88);
- __e_acsl_assert(! __gen_e_acsl_separated_11,"Assertion","main",
+ "tests/memory/separated.c",47);
+ __gen_e_acsl_size_31 = 8 * ((10 - 0) + 1);
+ if (__gen_e_acsl_size_31 <= 0) __gen_e_acsl_if_31 = 0;
+ else __gen_e_acsl_if_31 = __gen_e_acsl_size_31;
+ __gen_e_acsl_size_32 = 8 * ((15 - 5) + 1);
+ if (__gen_e_acsl_size_32 <= 0) __gen_e_acsl_if_32 = 0;
+ else __gen_e_acsl_if_32 = __gen_e_acsl_size_32;
+ __gen_e_acsl_separated_13 = __e_acsl_separated((size_t)2,
+ (char *)array_0 + 8 * 0,
+ __gen_e_acsl_if_31,
+ (char *)array_0 + 8 * 5,
+ __gen_e_acsl_if_32);
+ __e_acsl_assert(! __gen_e_acsl_separated_13,"Assertion","main",
"!\\separated(array_0 + (0 .. 10), array_0 + (5 .. 15))",
- "tests/memory/separated.c",45);
+ "tests/memory/separated.c",47);
}
/*@ assert ¬\separated(array_0 + (0 .. 10), array_0 + (5 .. 15)); */ ;
{
- int __gen_e_acsl_valid_read_27;
- int __gen_e_acsl_valid_read_28;
- int __gen_e_acsl_separated_12;
- __gen_e_acsl_valid_read_27 = __e_acsl_valid_read((void *)((char *)array_0 +
+ int __gen_e_acsl_size_33;
+ int __gen_e_acsl_if_33;
+ int __gen_e_acsl_valid_read_31;
+ int __gen_e_acsl_size_34;
+ int __gen_e_acsl_if_34;
+ int __gen_e_acsl_valid_read_32;
+ int __gen_e_acsl_size_35;
+ int __gen_e_acsl_if_35;
+ int __gen_e_acsl_size_36;
+ int __gen_e_acsl_if_36;
+ int __gen_e_acsl_separated_14;
+ __gen_e_acsl_size_33 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_33 <= 0) __gen_e_acsl_if_33 = 0;
+ else __gen_e_acsl_if_33 = __gen_e_acsl_size_33;
+ __gen_e_acsl_valid_read_31 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 0),
- (size_t)160,
+ (size_t)__gen_e_acsl_if_33,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. 19));
*/
- __e_acsl_assert(__gen_e_acsl_valid_read_27,"RTE","main",
+ __e_acsl_assert(__gen_e_acsl_valid_read_31,"RTE","main",
"separated_guard: \\valid_read(array_0 + (0 .. 19))",
- "tests/memory/separated.c",46);
- __gen_e_acsl_valid_read_28 = __e_acsl_valid_read((void *)((char *)array_0 +
+ "tests/memory/separated.c",48);
+ __gen_e_acsl_size_34 = 8 * ((15 - 5) + 1);
+ if (__gen_e_acsl_size_34 <= 0) __gen_e_acsl_if_34 = 0;
+ else __gen_e_acsl_if_34 = __gen_e_acsl_size_34;
+ __gen_e_acsl_valid_read_32 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 5),
- (size_t)88,
+ (size_t)__gen_e_acsl_if_34,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (5 .. 15));
*/
- __e_acsl_assert(__gen_e_acsl_valid_read_28,"RTE","main",
+ __e_acsl_assert(__gen_e_acsl_valid_read_32,"RTE","main",
"separated_guard: \\valid_read(array_0 + (5 .. 15))",
- "tests/memory/separated.c",46);
- __gen_e_acsl_separated_12 = __e_acsl_separated((size_t)2,
- (void *)((char *)array_0 +
- 8 * 5),88,
- (void *)((char *)array_0 +
- 8 * 0),160);
- __e_acsl_assert(! __gen_e_acsl_separated_12,"Assertion","main",
+ "tests/memory/separated.c",48);
+ __gen_e_acsl_size_35 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_35 <= 0) __gen_e_acsl_if_35 = 0;
+ else __gen_e_acsl_if_35 = __gen_e_acsl_size_35;
+ __gen_e_acsl_size_36 = 8 * ((15 - 5) + 1);
+ if (__gen_e_acsl_size_36 <= 0) __gen_e_acsl_if_36 = 0;
+ else __gen_e_acsl_if_36 = __gen_e_acsl_size_36;
+ __gen_e_acsl_separated_14 = __e_acsl_separated((size_t)2,
+ (char *)array_0 + 8 * 0,
+ __gen_e_acsl_if_35,
+ (char *)array_0 + 8 * 5,
+ __gen_e_acsl_if_36);
+ __e_acsl_assert(! __gen_e_acsl_separated_14,"Assertion","main",
"!\\separated(array_0 + (0 .. 19), array_0 + (5 .. 15))",
- "tests/memory/separated.c",46);
+ "tests/memory/separated.c",48);
}
/*@ assert ¬\separated(array_0 + (0 .. 19), array_0 + (5 .. 15)); */ ;
{
- int __gen_e_acsl_valid_read_29;
- int __gen_e_acsl_valid_read_30;
- int __gen_e_acsl_separated_13;
- __gen_e_acsl_valid_read_29 = __e_acsl_valid_read((void *)(array_0 + 0),
+ int __gen_e_acsl_valid_read_33;
+ int __gen_e_acsl_valid_read_34;
+ int __gen_e_acsl_separated_15;
+ __gen_e_acsl_valid_read_33 = __e_acsl_valid_read((void *)(array_0 + 0),
sizeof(double),
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + 0); */
- __e_acsl_assert(__gen_e_acsl_valid_read_29,"RTE","main",
+ __e_acsl_assert(__gen_e_acsl_valid_read_33,"RTE","main",
"separated_guard: \\valid_read(array_0 + 0)",
- "tests/memory/separated.c",47);
- __gen_e_acsl_valid_read_30 = __e_acsl_valid_read((void *)(array_0 + 1),
+ "tests/memory/separated.c",49);
+ __gen_e_acsl_valid_read_34 = __e_acsl_valid_read((void *)(array_0 + 1),
sizeof(double),
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + 1); */
- __e_acsl_assert(__gen_e_acsl_valid_read_30,"RTE","main",
+ __e_acsl_assert(__gen_e_acsl_valid_read_34,"RTE","main",
"separated_guard: \\valid_read(array_0 + 1)",
- "tests/memory/separated.c",47);
- __gen_e_acsl_separated_13 = __e_acsl_separated((size_t)2,
- (void *)(array_0 + 1),
+ "tests/memory/separated.c",49);
+ __gen_e_acsl_separated_15 = __e_acsl_separated((size_t)2,array_0 + 0,
sizeof(double),
- (void *)(array_0 + 0),
+ array_0 + 1,
sizeof(double));
- __e_acsl_assert(__gen_e_acsl_separated_13,"Assertion","main",
+ __e_acsl_assert(__gen_e_acsl_separated_15,"Assertion","main",
"\\separated(array_0 + 0, array_0 + 1)",
- "tests/memory/separated.c",47);
+ "tests/memory/separated.c",49);
}
/*@ assert \separated(array_0 + 0, array_0 + 1); */ ;
{
- int __gen_e_acsl_valid_read_31;
- int __gen_e_acsl_valid_read_32;
- int __gen_e_acsl_separated_14;
- __gen_e_acsl_valid_read_31 = __e_acsl_valid_read((void *)((char *)array_0 +
+ int __gen_e_acsl_size_37;
+ int __gen_e_acsl_if_37;
+ int __gen_e_acsl_valid_read_35;
+ int __gen_e_acsl_size_38;
+ int __gen_e_acsl_if_38;
+ int __gen_e_acsl_valid_read_36;
+ int __gen_e_acsl_size_39;
+ int __gen_e_acsl_if_39;
+ int __gen_e_acsl_size_40;
+ int __gen_e_acsl_if_40;
+ int __gen_e_acsl_separated_16;
+ __gen_e_acsl_size_37 = 8 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_37 <= 0) __gen_e_acsl_if_37 = 0;
+ else __gen_e_acsl_if_37 = __gen_e_acsl_size_37;
+ __gen_e_acsl_valid_read_35 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 0),
- (size_t)16,
+ (size_t)__gen_e_acsl_if_37,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. 1)); */
- __e_acsl_assert(__gen_e_acsl_valid_read_31,"RTE","main",
+ __e_acsl_assert(__gen_e_acsl_valid_read_35,"RTE","main",
"separated_guard: \\valid_read(array_0 + (0 .. 1))",
- "tests/memory/separated.c",48);
- __gen_e_acsl_valid_read_32 = __e_acsl_valid_read((void *)((char *)array_0 +
+ "tests/memory/separated.c",50);
+ __gen_e_acsl_size_38 = 8 * ((2 - 1) + 1);
+ if (__gen_e_acsl_size_38 <= 0) __gen_e_acsl_if_38 = 0;
+ else __gen_e_acsl_if_38 = __gen_e_acsl_size_38;
+ __gen_e_acsl_valid_read_36 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 1),
- (size_t)16,
+ (size_t)__gen_e_acsl_if_38,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (1 .. 2)); */
- __e_acsl_assert(__gen_e_acsl_valid_read_32,"RTE","main",
+ __e_acsl_assert(__gen_e_acsl_valid_read_36,"RTE","main",
"separated_guard: \\valid_read(array_0 + (1 .. 2))",
- "tests/memory/separated.c",48);
- __gen_e_acsl_separated_14 = __e_acsl_separated((size_t)2,
- (void *)((char *)array_0 +
- 8 * 1),16,
- (void *)((char *)array_0 +
- 8 * 0),16);
- __e_acsl_assert(! __gen_e_acsl_separated_14,"Assertion","main",
+ "tests/memory/separated.c",50);
+ __gen_e_acsl_size_39 = 8 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_39 <= 0) __gen_e_acsl_if_39 = 0;
+ else __gen_e_acsl_if_39 = __gen_e_acsl_size_39;
+ __gen_e_acsl_size_40 = 8 * ((2 - 1) + 1);
+ if (__gen_e_acsl_size_40 <= 0) __gen_e_acsl_if_40 = 0;
+ else __gen_e_acsl_if_40 = __gen_e_acsl_size_40;
+ __gen_e_acsl_separated_16 = __e_acsl_separated((size_t)2,
+ (char *)array_0 + 8 * 0,
+ __gen_e_acsl_if_39,
+ (char *)array_0 + 8 * 1,
+ __gen_e_acsl_if_40);
+ __e_acsl_assert(! __gen_e_acsl_separated_16,"Assertion","main",
"!\\separated(array_0 + (0 .. 1), array_0 + (1 .. 2))",
- "tests/memory/separated.c",48);
+ "tests/memory/separated.c",50);
}
/*@ assert ¬\separated(array_0 + (0 .. 1), array_0 + (1 .. 2)); */ ;
+ {
+ int __gen_e_acsl_size_41;
+ int __gen_e_acsl_if_41;
+ int __gen_e_acsl_valid_read_37;
+ int __gen_e_acsl_size_42;
+ int __gen_e_acsl_if_42;
+ int __gen_e_acsl_valid_read_38;
+ int __gen_e_acsl_size_43;
+ int __gen_e_acsl_if_43;
+ int __gen_e_acsl_size_44;
+ int __gen_e_acsl_if_44;
+ int __gen_e_acsl_separated_17;
+ __gen_e_acsl_size_41 = 8 * ((5 - 15) + 1);
+ if (__gen_e_acsl_size_41 <= 0) __gen_e_acsl_if_41 = 0;
+ else __gen_e_acsl_if_41 = __gen_e_acsl_size_41;
+ __gen_e_acsl_valid_read_37 = __e_acsl_valid_read((void *)((char *)array_0 +
+ 8 * 15),
+ (size_t)__gen_e_acsl_if_41,
+ (void *)array_0,
+ (void *)(& array_0));
+ /*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (15 .. 5));
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_37,"RTE","main",
+ "separated_guard: \\valid_read(array_0 + (15 .. 5))",
+ "tests/memory/separated.c",51);
+ __gen_e_acsl_size_42 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_42 <= 0) __gen_e_acsl_if_42 = 0;
+ else __gen_e_acsl_if_42 = __gen_e_acsl_size_42;
+ __gen_e_acsl_valid_read_38 = __e_acsl_valid_read((void *)((char *)array_0 +
+ 8 * 0),
+ (size_t)__gen_e_acsl_if_42,
+ (void *)array_0,
+ (void *)(& array_0));
+ /*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. 19));
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_38,"RTE","main",
+ "separated_guard: \\valid_read(array_0 + (0 .. 19))",
+ "tests/memory/separated.c",51);
+ __gen_e_acsl_size_43 = 8 * ((5 - 15) + 1);
+ if (__gen_e_acsl_size_43 <= 0) __gen_e_acsl_if_43 = 0;
+ else __gen_e_acsl_if_43 = __gen_e_acsl_size_43;
+ __gen_e_acsl_size_44 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_44 <= 0) __gen_e_acsl_if_44 = 0;
+ else __gen_e_acsl_if_44 = __gen_e_acsl_size_44;
+ __gen_e_acsl_separated_17 = __e_acsl_separated((size_t)2,
+ (char *)array_0 + 8 * 15,
+ __gen_e_acsl_if_43,
+ (char *)array_0 + 8 * 0,
+ __gen_e_acsl_if_44);
+ __e_acsl_assert(__gen_e_acsl_separated_17,"Assertion","main",
+ "\\separated(array_0 + (15 .. 5), array_0 + (0 .. 19))",
+ "tests/memory/separated.c",51);
+ }
+ /*@ assert \separated(array_0 + (15 .. 5), array_0 + (0 .. 19)); */ ;
+ {
+ int __gen_e_acsl_size_45;
+ int __gen_e_acsl_if_45;
+ int __gen_e_acsl_valid_read_39;
+ int __gen_e_acsl_size_46;
+ int __gen_e_acsl_if_46;
+ int __gen_e_acsl_valid_read_40;
+ int __gen_e_acsl_size_47;
+ int __gen_e_acsl_if_47;
+ int __gen_e_acsl_size_48;
+ int __gen_e_acsl_if_48;
+ int __gen_e_acsl_separated_18;
+ __gen_e_acsl_size_45 = 8 * ((-3 - 0) + 1);
+ if (__gen_e_acsl_size_45 <= 0) __gen_e_acsl_if_45 = 0;
+ else __gen_e_acsl_if_45 = __gen_e_acsl_size_45;
+ __gen_e_acsl_valid_read_39 = __e_acsl_valid_read((void *)((char *)array_0 +
+ 8 * 0),
+ (size_t)__gen_e_acsl_if_45,
+ (void *)array_0,
+ (void *)(& array_0));
+ /*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. -3));
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_39,"RTE","main",
+ "separated_guard: \\valid_read(array_0 + (0 .. -3))",
+ "tests/memory/separated.c",52);
+ __gen_e_acsl_size_46 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_46 <= 0) __gen_e_acsl_if_46 = 0;
+ else __gen_e_acsl_if_46 = __gen_e_acsl_size_46;
+ __gen_e_acsl_valid_read_40 = __e_acsl_valid_read((void *)((char *)array_0 +
+ 8 * 0),
+ (size_t)__gen_e_acsl_if_46,
+ (void *)array_0,
+ (void *)(& array_0));
+ /*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. 19));
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_40,"RTE","main",
+ "separated_guard: \\valid_read(array_0 + (0 .. 19))",
+ "tests/memory/separated.c",52);
+ __gen_e_acsl_size_47 = 8 * ((-3 - 0) + 1);
+ if (__gen_e_acsl_size_47 <= 0) __gen_e_acsl_if_47 = 0;
+ else __gen_e_acsl_if_47 = __gen_e_acsl_size_47;
+ __gen_e_acsl_size_48 = 8 * ((19 - 0) + 1);
+ if (__gen_e_acsl_size_48 <= 0) __gen_e_acsl_if_48 = 0;
+ else __gen_e_acsl_if_48 = __gen_e_acsl_size_48;
+ __gen_e_acsl_separated_18 = __e_acsl_separated((size_t)2,
+ (char *)array_0 + 8 * 0,
+ __gen_e_acsl_if_47,
+ (char *)array_0 + 8 * 0,
+ __gen_e_acsl_if_48);
+ __e_acsl_assert(__gen_e_acsl_separated_18,"Assertion","main",
+ "\\separated(array_0 + (0 .. -3), array_0 + (0 .. 19))",
+ "tests/memory/separated.c",52);
+ }
+ /*@ assert \separated(array_0 + (0 .. -3), array_0 + (0 .. 19)); */ ;
free((void *)array_0);
__e_acsl_delete_block((void *)(& array_0));
}
+ {
+ double array_1[10][10][10] = {{{(double)0}}};
+ __e_acsl_store_block((void *)(array_1),(size_t)8000);
+ __e_acsl_full_init((void *)(& array_1));
+ {
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_range;
+ int __gen_e_acsl_forall_2;
+ int __gen_e_acsl_range_2;
+ int __gen_e_acsl_forall_3;
+ int __gen_e_acsl_range_3;
+ int __gen_e_acsl_forall_4;
+ int __gen_e_acsl_range_4;
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_range = 0;
+ while (1) {
+ if (__gen_e_acsl_range <= 2) ; else break;
+ {
+ int __gen_e_acsl_valid_read_41;
+ __gen_e_acsl_valid_read_41 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range][0]),
+ sizeof(double),
+ (void *)(& array_1[0][__gen_e_acsl_range][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_41) ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop1;
+ }
+ }
+ __gen_e_acsl_range ++;
+ }
+ e_acsl_end_loop1: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[0][0 .. 2][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0][0 .. 2][0])",
+ "tests/memory/separated.c",60);
+ __gen_e_acsl_forall_2 = 1;
+ __gen_e_acsl_range_2 = 3;
+ while (1) {
+ if (__gen_e_acsl_range_2 <= 5) ; else break;
+ {
+ int __gen_e_acsl_valid_read_42;
+ __gen_e_acsl_valid_read_42 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_2][0]),
+ sizeof(double),
+ (void *)(& array_1[0][__gen_e_acsl_range_2][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_42) ;
+ else {
+ __gen_e_acsl_forall_2 = 0;
+ goto e_acsl_end_loop2;
+ }
+ }
+ __gen_e_acsl_range_2 ++;
+ }
+ e_acsl_end_loop2: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[0][3 .. 5][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall_2,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0][3 .. 5][0])",
+ "tests/memory/separated.c",60);
+ __gen_e_acsl_forall_3 = 1;
+ __gen_e_acsl_range_3 = 6;
+ while (1) {
+ if (__gen_e_acsl_range_3 <= 9) ; else break;
+ {
+ int __gen_e_acsl_valid_read_43;
+ __gen_e_acsl_valid_read_43 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_3][0]),
+ sizeof(double),
+ (void *)(& array_1[0][__gen_e_acsl_range_3][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_43) ;
+ else {
+ __gen_e_acsl_forall_3 = 0;
+ goto e_acsl_end_loop3;
+ }
+ }
+ __gen_e_acsl_range_3 ++;
+ }
+ e_acsl_end_loop3: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[0][6 .. 9][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall_3,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0][6 .. 9][0])",
+ "tests/memory/separated.c",60);
+ __gen_e_acsl_forall_4 = 1;
+ __gen_e_acsl_range_4 = 6;
+ while (1) {
+ if (__gen_e_acsl_range_4 <= 9) ; else break;
+ {
+ int __gen_e_acsl_forall_5;
+ int __gen_e_acsl_range_5;
+ __gen_e_acsl_forall_5 = 1;
+ __gen_e_acsl_range_5 = 3;
+ while (1) {
+ if (__gen_e_acsl_range_5 <= 5) ; else break;
+ {
+ int __gen_e_acsl_forall_6;
+ int __gen_e_acsl_range_6;
+ __gen_e_acsl_forall_6 = 1;
+ __gen_e_acsl_range_6 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_6 <= 2) ; else break;
+ {
+ int __gen_e_acsl_valid_read_44;
+ int __gen_e_acsl_valid_read_45;
+ int __gen_e_acsl_valid_read_46;
+ int __gen_e_acsl_separated_19;
+ __gen_e_acsl_valid_read_44 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_6][0]),
+ sizeof(double),
+ (void *)(& array_1[0][__gen_e_acsl_range_6][0]),
+ (void *)0);
+ /*@ assert
+ E_ACSL: separated_guard:
+ \valid_read(&array_1[0][range_6][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_44,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0][range_6][0])",
+ "tests/memory/separated.c",60);
+ __gen_e_acsl_valid_read_45 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_5][0]),
+ sizeof(double),
+ (void *)(& array_1[0][__gen_e_acsl_range_5][0]),
+ (void *)0);
+ /*@ assert
+ E_ACSL: separated_guard:
+ \valid_read(&array_1[0][range_5][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_45,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0][range_5][0])",
+ "tests/memory/separated.c",60);
+ __gen_e_acsl_valid_read_46 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_4][0]),
+ sizeof(double),
+ (void *)(& array_1[0][__gen_e_acsl_range_4][0]),
+ (void *)0);
+ /*@ assert
+ E_ACSL: separated_guard:
+ \valid_read(&array_1[0][range_4][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_46,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0][range_4][0])",
+ "tests/memory/separated.c",60);
+ __gen_e_acsl_separated_19 = __e_acsl_separated((size_t)3,
+ & array_1[0][__gen_e_acsl_range_6][0],
+ sizeof(double),
+ & array_1[0][__gen_e_acsl_range_5][0],
+ sizeof(double),
+ & array_1[0][__gen_e_acsl_range_4][0],
+ sizeof(double));
+ if (__gen_e_acsl_separated_19) ;
+ else {
+ __gen_e_acsl_forall_6 = 0;
+ goto e_acsl_end_loop4;
+ }
+ }
+ __gen_e_acsl_range_6 ++;
+ }
+ e_acsl_end_loop4: ;
+ if (__gen_e_acsl_forall_6) ;
+ else {
+ __gen_e_acsl_forall_5 = 0;
+ goto e_acsl_end_loop5;
+ }
+ }
+ __gen_e_acsl_range_5 ++;
+ }
+ e_acsl_end_loop5: ;
+ if (__gen_e_acsl_forall_5) ;
+ else {
+ __gen_e_acsl_forall_4 = 0;
+ goto e_acsl_end_loop6;
+ }
+ }
+ __gen_e_acsl_range_4 ++;
+ }
+ e_acsl_end_loop6: ;
+ __e_acsl_assert(__gen_e_acsl_forall_4,"Assertion","main",
+ "\\separated(\n &array_1[0][0 .. 2][0], &array_1[0][3 .. 5][0], &array_1[0][6 .. 9][0]\n )",
+ "tests/memory/separated.c",60);
+ }
+ /*@
+ assert
+ \separated(
+ &array_1[0][0 .. 2][0], &array_1[0][3 .. 5][0], &array_1[0][6 .. 9][0]
+ );
+ */
+ ;
+ {
+ int __gen_e_acsl_forall_7;
+ int __gen_e_acsl_range_7;
+ int __gen_e_acsl_forall_8;
+ int __gen_e_acsl_range_8;
+ int __gen_e_acsl_forall_9;
+ int __gen_e_acsl_range_9;
+ int __gen_e_acsl_forall_10;
+ int __gen_e_acsl_range_10;
+ __gen_e_acsl_forall_7 = 1;
+ __gen_e_acsl_range_7 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_7 <= 2) ; else break;
+ {
+ int __gen_e_acsl_valid_read_47;
+ __gen_e_acsl_valid_read_47 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_7][0]),
+ sizeof(double),
+ (void *)(& array_1[0][__gen_e_acsl_range_7][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_47) ;
+ else {
+ __gen_e_acsl_forall_7 = 0;
+ goto e_acsl_end_loop7;
+ }
+ }
+ __gen_e_acsl_range_7 ++;
+ }
+ e_acsl_end_loop7: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[0][0 .. 2][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall_7,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0][0 .. 2][0])",
+ "tests/memory/separated.c",61);
+ __gen_e_acsl_forall_8 = 1;
+ __gen_e_acsl_range_8 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_8 <= 2) ; else break;
+ {
+ int __gen_e_acsl_valid_read_48;
+ __gen_e_acsl_valid_read_48 = __e_acsl_valid_read((void *)(& array_1[1][__gen_e_acsl_range_8][0]),
+ sizeof(double),
+ (void *)(& array_1[1][__gen_e_acsl_range_8][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_48) ;
+ else {
+ __gen_e_acsl_forall_8 = 0;
+ goto e_acsl_end_loop8;
+ }
+ }
+ __gen_e_acsl_range_8 ++;
+ }
+ e_acsl_end_loop8: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[1][0 .. 2][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall_8,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[1][0 .. 2][0])",
+ "tests/memory/separated.c",61);
+ __gen_e_acsl_forall_9 = 1;
+ __gen_e_acsl_range_9 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_9 <= 2) ; else break;
+ {
+ int __gen_e_acsl_valid_read_49;
+ __gen_e_acsl_valid_read_49 = __e_acsl_valid_read((void *)(& array_1[2][__gen_e_acsl_range_9][0]),
+ sizeof(double),
+ (void *)(& array_1[2][__gen_e_acsl_range_9][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_49) ;
+ else {
+ __gen_e_acsl_forall_9 = 0;
+ goto e_acsl_end_loop9;
+ }
+ }
+ __gen_e_acsl_range_9 ++;
+ }
+ e_acsl_end_loop9: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[2][0 .. 2][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall_9,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[2][0 .. 2][0])",
+ "tests/memory/separated.c",61);
+ __gen_e_acsl_forall_10 = 1;
+ __gen_e_acsl_range_10 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_10 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_11;
+ int __gen_e_acsl_range_11;
+ __gen_e_acsl_forall_11 = 1;
+ __gen_e_acsl_range_11 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_11 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_12;
+ int __gen_e_acsl_range_12;
+ __gen_e_acsl_forall_12 = 1;
+ __gen_e_acsl_range_12 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_12 <= 2) ; else break;
+ {
+ int __gen_e_acsl_valid_read_50;
+ int __gen_e_acsl_valid_read_51;
+ int __gen_e_acsl_valid_read_52;
+ int __gen_e_acsl_separated_20;
+ __gen_e_acsl_valid_read_50 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_12][0]),
+ sizeof(double),
+ (void *)(& array_1[0][__gen_e_acsl_range_12][0]),
+ (void *)0);
+ /*@ assert
+ E_ACSL: separated_guard:
+ \valid_read(&array_1[0][range_12][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_50,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0][range_12][0])",
+ "tests/memory/separated.c",61);
+ __gen_e_acsl_valid_read_51 = __e_acsl_valid_read((void *)(& array_1[1][__gen_e_acsl_range_11][0]),
+ sizeof(double),
+ (void *)(& array_1[1][__gen_e_acsl_range_11][0]),
+ (void *)0);
+ /*@ assert
+ E_ACSL: separated_guard:
+ \valid_read(&array_1[1][range_11][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_51,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[1][range_11][0])",
+ "tests/memory/separated.c",61);
+ __gen_e_acsl_valid_read_52 = __e_acsl_valid_read((void *)(& array_1[2][__gen_e_acsl_range_10][0]),
+ sizeof(double),
+ (void *)(& array_1[2][__gen_e_acsl_range_10][0]),
+ (void *)0);
+ /*@ assert
+ E_ACSL: separated_guard:
+ \valid_read(&array_1[2][range_10][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_52,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[2][range_10][0])",
+ "tests/memory/separated.c",61);
+ __gen_e_acsl_separated_20 = __e_acsl_separated((size_t)3,
+ & array_1[0][__gen_e_acsl_range_12][0],
+ sizeof(double),
+ & array_1[1][__gen_e_acsl_range_11][0],
+ sizeof(double),
+ & array_1[2][__gen_e_acsl_range_10][0],
+ sizeof(double));
+ if (__gen_e_acsl_separated_20) ;
+ else {
+ __gen_e_acsl_forall_12 = 0;
+ goto e_acsl_end_loop10;
+ }
+ }
+ __gen_e_acsl_range_12 ++;
+ }
+ e_acsl_end_loop10: ;
+ if (__gen_e_acsl_forall_12) ;
+ else {
+ __gen_e_acsl_forall_11 = 0;
+ goto e_acsl_end_loop11;
+ }
+ }
+ __gen_e_acsl_range_11 ++;
+ }
+ e_acsl_end_loop11: ;
+ if (__gen_e_acsl_forall_11) ;
+ else {
+ __gen_e_acsl_forall_10 = 0;
+ goto e_acsl_end_loop12;
+ }
+ }
+ __gen_e_acsl_range_10 ++;
+ }
+ e_acsl_end_loop12: ;
+ __e_acsl_assert(__gen_e_acsl_forall_10,"Assertion","main",
+ "\\separated(\n &array_1[0][0 .. 2][0], &array_1[1][0 .. 2][0], &array_1[2][0 .. 2][0]\n )",
+ "tests/memory/separated.c",61);
+ }
+ /*@
+ assert
+ \separated(
+ &array_1[0][0 .. 2][0], &array_1[1][0 .. 2][0], &array_1[2][0 .. 2][0]
+ );
+ */
+ ;
+ {
+ int __gen_e_acsl_forall_13;
+ int __gen_e_acsl_range_14;
+ int __gen_e_acsl_forall_15;
+ int __gen_e_acsl_range_16;
+ int __gen_e_acsl_forall_17;
+ int __gen_e_acsl_range_18;
+ __gen_e_acsl_forall_13 = 1;
+ __gen_e_acsl_range_14 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_14 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_14;
+ int __gen_e_acsl_range_13;
+ __gen_e_acsl_forall_14 = 1;
+ __gen_e_acsl_range_13 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_13 <= 2) ; else break;
+ {
+ int __gen_e_acsl_valid_read_53;
+ __gen_e_acsl_valid_read_53 = __e_acsl_valid_read((void *)(& array_1[__gen_e_acsl_range_13][__gen_e_acsl_range_14][0]),
+ sizeof(double),
+ (void *)(& array_1[__gen_e_acsl_range_13][__gen_e_acsl_range_14][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_53) ;
+ else {
+ __gen_e_acsl_forall_14 = 0;
+ goto e_acsl_end_loop13;
+ }
+ }
+ __gen_e_acsl_range_13 ++;
+ }
+ e_acsl_end_loop13: ;
+ if (__gen_e_acsl_forall_14) ;
+ else {
+ __gen_e_acsl_forall_13 = 0;
+ goto e_acsl_end_loop14;
+ }
+ }
+ __gen_e_acsl_range_14 ++;
+ }
+ e_acsl_end_loop14: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[0 .. 2][0 .. 2][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall_13,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0 .. 2][0 .. 2][0])",
+ "tests/memory/separated.c",62);
+ __gen_e_acsl_forall_15 = 1;
+ __gen_e_acsl_range_16 = 3;
+ while (1) {
+ if (__gen_e_acsl_range_16 <= 5) ; else break;
+ {
+ int __gen_e_acsl_forall_16;
+ int __gen_e_acsl_range_15;
+ __gen_e_acsl_forall_16 = 1;
+ __gen_e_acsl_range_15 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_15 <= 2) ; else break;
+ {
+ int __gen_e_acsl_valid_read_54;
+ __gen_e_acsl_valid_read_54 = __e_acsl_valid_read((void *)(& array_1[__gen_e_acsl_range_15][__gen_e_acsl_range_16][0]),
+ sizeof(double),
+ (void *)(& array_1[__gen_e_acsl_range_15][__gen_e_acsl_range_16][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_54) ;
+ else {
+ __gen_e_acsl_forall_16 = 0;
+ goto e_acsl_end_loop15;
+ }
+ }
+ __gen_e_acsl_range_15 ++;
+ }
+ e_acsl_end_loop15: ;
+ if (__gen_e_acsl_forall_16) ;
+ else {
+ __gen_e_acsl_forall_15 = 0;
+ goto e_acsl_end_loop16;
+ }
+ }
+ __gen_e_acsl_range_16 ++;
+ }
+ e_acsl_end_loop16: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[0 .. 2][3 .. 5][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall_15,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0 .. 2][3 .. 5][0])",
+ "tests/memory/separated.c",62);
+ __gen_e_acsl_forall_17 = 1;
+ __gen_e_acsl_range_18 = 3;
+ while (1) {
+ if (__gen_e_acsl_range_18 <= 5) ; else break;
+ {
+ int __gen_e_acsl_forall_18;
+ int __gen_e_acsl_range_17;
+ __gen_e_acsl_forall_18 = 1;
+ __gen_e_acsl_range_17 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_17 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_19;
+ int __gen_e_acsl_range_20;
+ __gen_e_acsl_forall_19 = 1;
+ __gen_e_acsl_range_20 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_20 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_20;
+ int __gen_e_acsl_range_19;
+ __gen_e_acsl_forall_20 = 1;
+ __gen_e_acsl_range_19 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_19 <= 2) ; else break;
+ {
+ int __gen_e_acsl_valid_read_55;
+ int __gen_e_acsl_valid_read_56;
+ int __gen_e_acsl_separated_21;
+ __gen_e_acsl_valid_read_55 = __e_acsl_valid_read
+ ((void *)(& array_1[__gen_e_acsl_range_19][__gen_e_acsl_range_20][0]),
+ sizeof(double),
+ (void *)(& array_1[__gen_e_acsl_range_19][__gen_e_acsl_range_20][0]),
+ (void *)0);
+ /*@ assert
+ E_ACSL: separated_guard:
+ \valid_read(&array_1[range_19][range_20][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_55,"RTE",
+ "main",
+ "separated_guard: \\valid_read(&array_1[range_19][range_20][0])",
+ "tests/memory/separated.c",62);
+ __gen_e_acsl_valid_read_56 = __e_acsl_valid_read
+ ((void *)(& array_1[__gen_e_acsl_range_17][__gen_e_acsl_range_18][0]),
+ sizeof(double),
+ (void *)(& array_1[__gen_e_acsl_range_17][__gen_e_acsl_range_18][0]),
+ (void *)0);
+ /*@ assert
+ E_ACSL: separated_guard:
+ \valid_read(&array_1[range_17][range_18][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_56,"RTE",
+ "main",
+ "separated_guard: \\valid_read(&array_1[range_17][range_18][0])",
+ "tests/memory/separated.c",62);
+ __gen_e_acsl_separated_21 = __e_acsl_separated((size_t)2,
+ & array_1[__gen_e_acsl_range_19][__gen_e_acsl_range_20][0],
+ sizeof(double),
+ & array_1[__gen_e_acsl_range_17][__gen_e_acsl_range_18][0],
+ sizeof(double));
+ if (__gen_e_acsl_separated_21) ;
+ else {
+ __gen_e_acsl_forall_20 = 0;
+ goto e_acsl_end_loop17;
+ }
+ }
+ __gen_e_acsl_range_19 ++;
+ }
+ e_acsl_end_loop17: ;
+ if (__gen_e_acsl_forall_20) ;
+ else {
+ __gen_e_acsl_forall_19 = 0;
+ goto e_acsl_end_loop18;
+ }
+ }
+ __gen_e_acsl_range_20 ++;
+ }
+ e_acsl_end_loop18: ;
+ if (__gen_e_acsl_forall_19) ;
+ else {
+ __gen_e_acsl_forall_18 = 0;
+ goto e_acsl_end_loop19;
+ }
+ }
+ __gen_e_acsl_range_17 ++;
+ }
+ e_acsl_end_loop19: ;
+ if (__gen_e_acsl_forall_18) ;
+ else {
+ __gen_e_acsl_forall_17 = 0;
+ goto e_acsl_end_loop20;
+ }
+ }
+ __gen_e_acsl_range_18 ++;
+ }
+ e_acsl_end_loop20: ;
+ __e_acsl_assert(__gen_e_acsl_forall_17,"Assertion","main",
+ "\\separated(&array_1[0 .. 2][0 .. 2][0], &array_1[0 .. 2][3 .. 5][0])",
+ "tests/memory/separated.c",62);
+ }
+ /*@
+ assert
+ \separated(&array_1[0 .. 2][0 .. 2][0], &array_1[0 .. 2][3 .. 5][0]); */
+ ;
+ {
+ int __gen_e_acsl_forall_21;
+ int __gen_e_acsl_range_22;
+ int __gen_e_acsl_forall_23;
+ int __gen_e_acsl_range_24;
+ int __gen_e_acsl_forall_25;
+ int __gen_e_acsl_range_26;
+ __gen_e_acsl_forall_21 = 1;
+ __gen_e_acsl_range_22 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_22 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_22;
+ int __gen_e_acsl_range_21;
+ __gen_e_acsl_forall_22 = 1;
+ __gen_e_acsl_range_21 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_21 <= 3) ; else break;
+ {
+ int __gen_e_acsl_valid_read_57;
+ __gen_e_acsl_valid_read_57 = __e_acsl_valid_read((void *)(& array_1[__gen_e_acsl_range_21][__gen_e_acsl_range_22][0]),
+ sizeof(double),
+ (void *)(& array_1[__gen_e_acsl_range_21][__gen_e_acsl_range_22][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_57) ;
+ else {
+ __gen_e_acsl_forall_22 = 0;
+ goto e_acsl_end_loop21;
+ }
+ }
+ __gen_e_acsl_range_21 ++;
+ }
+ e_acsl_end_loop21: ;
+ if (__gen_e_acsl_forall_22) ;
+ else {
+ __gen_e_acsl_forall_21 = 0;
+ goto e_acsl_end_loop22;
+ }
+ }
+ __gen_e_acsl_range_22 ++;
+ }
+ e_acsl_end_loop22: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[0 .. 3][0 .. 2][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall_21,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0 .. 3][0 .. 2][0])",
+ "tests/memory/separated.c",63);
+ __gen_e_acsl_forall_23 = 1;
+ __gen_e_acsl_range_24 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_24 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_24;
+ int __gen_e_acsl_range_23;
+ __gen_e_acsl_forall_24 = 1;
+ __gen_e_acsl_range_23 = 3;
+ while (1) {
+ if (__gen_e_acsl_range_23 <= 5) ; else break;
+ {
+ int __gen_e_acsl_valid_read_58;
+ __gen_e_acsl_valid_read_58 = __e_acsl_valid_read((void *)(& array_1[__gen_e_acsl_range_23][__gen_e_acsl_range_24][0]),
+ sizeof(double),
+ (void *)(& array_1[__gen_e_acsl_range_23][__gen_e_acsl_range_24][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_58) ;
+ else {
+ __gen_e_acsl_forall_24 = 0;
+ goto e_acsl_end_loop23;
+ }
+ }
+ __gen_e_acsl_range_23 ++;
+ }
+ e_acsl_end_loop23: ;
+ if (__gen_e_acsl_forall_24) ;
+ else {
+ __gen_e_acsl_forall_23 = 0;
+ goto e_acsl_end_loop24;
+ }
+ }
+ __gen_e_acsl_range_24 ++;
+ }
+ e_acsl_end_loop24: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[3 .. 5][0 .. 2][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall_23,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[3 .. 5][0 .. 2][0])",
+ "tests/memory/separated.c",63);
+ __gen_e_acsl_forall_25 = 1;
+ __gen_e_acsl_range_26 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_26 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_26;
+ int __gen_e_acsl_range_25;
+ __gen_e_acsl_forall_26 = 1;
+ __gen_e_acsl_range_25 = 3;
+ while (1) {
+ if (__gen_e_acsl_range_25 <= 5) ; else break;
+ {
+ int __gen_e_acsl_forall_27;
+ int __gen_e_acsl_range_28;
+ __gen_e_acsl_forall_27 = 1;
+ __gen_e_acsl_range_28 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_28 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_28;
+ int __gen_e_acsl_range_27;
+ __gen_e_acsl_forall_28 = 1;
+ __gen_e_acsl_range_27 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_27 <= 3) ; else break;
+ {
+ int __gen_e_acsl_valid_read_59;
+ int __gen_e_acsl_valid_read_60;
+ int __gen_e_acsl_separated_22;
+ __gen_e_acsl_valid_read_59 = __e_acsl_valid_read
+ ((void *)(& array_1[__gen_e_acsl_range_27][__gen_e_acsl_range_28][0]),
+ sizeof(double),
+ (void *)(& array_1[__gen_e_acsl_range_27][__gen_e_acsl_range_28][0]),
+ (void *)0);
+ /*@ assert
+ E_ACSL: separated_guard:
+ \valid_read(&array_1[range_27][range_28][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_59,"RTE",
+ "main",
+ "separated_guard: \\valid_read(&array_1[range_27][range_28][0])",
+ "tests/memory/separated.c",63);
+ __gen_e_acsl_valid_read_60 = __e_acsl_valid_read
+ ((void *)(& array_1[__gen_e_acsl_range_25][__gen_e_acsl_range_26][0]),
+ sizeof(double),
+ (void *)(& array_1[__gen_e_acsl_range_25][__gen_e_acsl_range_26][0]),
+ (void *)0);
+ /*@ assert
+ E_ACSL: separated_guard:
+ \valid_read(&array_1[range_25][range_26][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_60,"RTE",
+ "main",
+ "separated_guard: \\valid_read(&array_1[range_25][range_26][0])",
+ "tests/memory/separated.c",63);
+ __gen_e_acsl_separated_22 = __e_acsl_separated((size_t)2,
+ & array_1[__gen_e_acsl_range_27][__gen_e_acsl_range_28][0],
+ sizeof(double),
+ & array_1[__gen_e_acsl_range_25][__gen_e_acsl_range_26][0],
+ sizeof(double));
+ if (__gen_e_acsl_separated_22) ;
+ else {
+ __gen_e_acsl_forall_28 = 0;
+ goto e_acsl_end_loop25;
+ }
+ }
+ __gen_e_acsl_range_27 ++;
+ }
+ e_acsl_end_loop25: ;
+ if (__gen_e_acsl_forall_28) ;
+ else {
+ __gen_e_acsl_forall_27 = 0;
+ goto e_acsl_end_loop26;
+ }
+ }
+ __gen_e_acsl_range_28 ++;
+ }
+ e_acsl_end_loop26: ;
+ if (__gen_e_acsl_forall_27) ;
+ else {
+ __gen_e_acsl_forall_26 = 0;
+ goto e_acsl_end_loop27;
+ }
+ }
+ __gen_e_acsl_range_25 ++;
+ }
+ e_acsl_end_loop27: ;
+ if (__gen_e_acsl_forall_26) ;
+ else {
+ __gen_e_acsl_forall_25 = 0;
+ goto e_acsl_end_loop28;
+ }
+ }
+ __gen_e_acsl_range_26 ++;
+ }
+ e_acsl_end_loop28: ;
+ __e_acsl_assert(! __gen_e_acsl_forall_25,"Assertion","main",
+ "!\\separated(&array_1[0 .. 3][0 .. 2][0], &array_1[3 .. 5][0 .. 2][0])",
+ "tests/memory/separated.c",63);
+ }
+ /*@
+ assert
+ ¬\separated(&array_1[0 .. 3][0 .. 2][0], &array_1[3 .. 5][0 .. 2][0]);
+ */
+ ;
+ {
+ int __gen_e_acsl_forall_29;
+ int __gen_e_acsl_range_32;
+ int __gen_e_acsl_forall_31;
+ int __gen_e_acsl_range_34;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[0 .. 3][2 .. 0][0]);
+ */
+ __e_acsl_assert(1,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[0 .. 3][2 .. 0][0])",
+ "tests/memory/separated.c",64);
+ __gen_e_acsl_forall_29 = 1;
+ __gen_e_acsl_range_32 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_32 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_30;
+ int __gen_e_acsl_range_31;
+ __gen_e_acsl_forall_30 = 1;
+ __gen_e_acsl_range_31 = 3;
+ while (1) {
+ if (__gen_e_acsl_range_31 <= 5) ; else break;
+ {
+ int __gen_e_acsl_valid_read_61;
+ __gen_e_acsl_valid_read_61 = __e_acsl_valid_read((void *)(& array_1[__gen_e_acsl_range_31][__gen_e_acsl_range_32][0]),
+ sizeof(double),
+ (void *)(& array_1[__gen_e_acsl_range_31][__gen_e_acsl_range_32][0]),
+ (void *)0);
+ if (__gen_e_acsl_valid_read_61) ;
+ else {
+ __gen_e_acsl_forall_30 = 0;
+ goto e_acsl_end_loop29;
+ }
+ }
+ __gen_e_acsl_range_31 ++;
+ }
+ e_acsl_end_loop29: ;
+ if (__gen_e_acsl_forall_30) ;
+ else {
+ __gen_e_acsl_forall_29 = 0;
+ goto e_acsl_end_loop30;
+ }
+ }
+ __gen_e_acsl_range_32 ++;
+ }
+ e_acsl_end_loop30: ;
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read(&array_1[3 .. 5][0 .. 2][0]);
+ */
+ __e_acsl_assert(__gen_e_acsl_forall_29,"RTE","main",
+ "separated_guard: \\valid_read(&array_1[3 .. 5][0 .. 2][0])",
+ "tests/memory/separated.c",64);
+ __gen_e_acsl_forall_31 = 1;
+ __gen_e_acsl_range_34 = 0;
+ while (1) {
+ if (__gen_e_acsl_range_34 <= 2) ; else break;
+ {
+ int __gen_e_acsl_forall_32;
+ int __gen_e_acsl_range_33;
+ __gen_e_acsl_forall_32 = 1;
+ __gen_e_acsl_range_33 = 3;
+ while (1) {
+ if (__gen_e_acsl_range_33 <= 5) ; else break;
+ if (1) ;
+ else {
+ __gen_e_acsl_forall_32 = 0;
+ goto e_acsl_end_loop31;
+ }
+ __gen_e_acsl_range_33 ++;
+ }
+ e_acsl_end_loop31: ;
+ if (__gen_e_acsl_forall_32) ;
+ else {
+ __gen_e_acsl_forall_31 = 0;
+ goto e_acsl_end_loop32;
+ }
+ }
+ __gen_e_acsl_range_34 ++;
+ }
+ e_acsl_end_loop32: ;
+ __e_acsl_assert(__gen_e_acsl_forall_31,"Assertion","main",
+ "\\separated(&array_1[0 .. 3][2 .. 0][0], &array_1[3 .. 5][0 .. 2][0])",
+ "tests/memory/separated.c",64);
+ }
+ /*@
+ assert
+ \separated(&array_1[0 .. 3][2 .. 0][0], &array_1[3 .. 5][0 .. 2][0]); */
+ ;
+ __e_acsl_delete_block((void *)(array_1));
+ }
__retres = 0;
__e_acsl_memory_clean();
return __retres;
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 74e130d7182ee876c8f3b1bc3fb688967cb221a4..c4eecf13293934aa893ac8472a4b90df152140b2 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
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-[e-acsl] tests/memory/ranges_in_builtins.c:64: Warning:
+[e-acsl] tests/memory/ranges_in_builtins.c:67: Warning:
E-ACSL construct `arithmetic over set of pointers or arrays'
is not yet supported.
Ignoring annotation.
@@ -8,13 +8,15 @@
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:
+[eva:alarm] tests/memory/ranges_in_builtins.c:52: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/ranges_in_builtins.c:52: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/memory/ranges_in_builtins.c:57: Warning:
accessing uninitialized left-value. assert \initialized(&s.b);
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle
index beb1260483ced4c4fd7fec20e74713d99c944702..dd7095867a867791209b2f41797c646d32ef2dcc 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle
@@ -14,13 +14,13 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:25: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/separated.c:34: Warning:
+[eva:alarm] tests/memory/separated.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/separated.c:35: Warning:
+[eva:alarm] tests/memory/separated.c:27: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/separated.c:44: Warning:
+[eva:alarm] tests/memory/separated.c:36: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/separated.c:45: Warning:
+[eva:alarm] tests/memory/separated.c:37: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:46: Warning:
function __e_acsl_assert: precondition got status unknown.
@@ -28,3 +28,33 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:48: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/separated.c:49: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/separated.c:50: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/separated.c:51: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/separated.c:52: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/separated.c:60: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/separated.c:60: Warning:
+ assertion 'E_ACSL,separated_guard' got status unknown.
+[eva:alarm] tests/memory/separated.c:61: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/separated.c:61: Warning:
+ assertion 'E_ACSL,separated_guard' got status unknown.
+[eva:alarm] tests/memory/separated.c:62: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/separated.c:62: Warning:
+ assertion 'E_ACSL,separated_guard' got status unknown.
+[eva:alarm] tests/memory/separated.c:62: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/separated.c:63: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/separated.c:63: Warning:
+ assertion 'E_ACSL,separated_guard' got status unknown.
+[eva:alarm] tests/memory/separated.c:63: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/separated.c:63: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/separated.c:64: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
index 3b0511fa9b1b81d990817fb3c5eb74072f572a8d..202dc5fc2e2511398bc35cb4db26897e44e77296 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
@@ -432,16 +432,109 @@ void *__gen_e_acsl_memcpy(void * __restrict dest,
{
void *__gen_e_acsl_at;
void *__retres;
- __e_acsl_store_block((void *)(& dest),(size_t)8);
- __e_acsl_temporal_pull_parameter((void *)(& dest),0U,8UL);
- __e_acsl_temporal_reset_parameters();
- __e_acsl_temporal_reset_return();
- __e_acsl_temporal_save_nreferent_parameter((void *)(& dest),0U);
- __e_acsl_temporal_memcpy(dest,(void *)src,n);
+ {
+ unsigned long __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ unsigned long __gen_e_acsl__3;
+ unsigned long __gen_e_acsl_if;
+ int __gen_e_acsl_valid_read;
+ unsigned long __gen_e_acsl_size_2;
+ unsigned long __gen_e_acsl__4;
+ unsigned long __gen_e_acsl_if_2;
+ int __gen_e_acsl_valid_read_2;
+ unsigned long __gen_e_acsl_size_3;
+ unsigned long __gen_e_acsl__5;
+ unsigned long __gen_e_acsl_if_3;
+ unsigned long __gen_e_acsl_size_4;
+ unsigned long __gen_e_acsl__6;
+ unsigned long __gen_e_acsl_if_4;
+ int __gen_e_acsl_separated;
+ __e_acsl_store_block((void *)(& src),(size_t)8);
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
+ __e_acsl_temporal_pull_parameter((void *)(& dest),0U,8UL);
+ __e_acsl_temporal_pull_parameter((void *)(& src),1U,8UL);
+ __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init(__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__2));
+ __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_));
+ __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size = 1UL * __gen_e_acsl__3;
+ if (__gen_e_acsl_size <= 0UL) __gen_e_acsl_if = 0UL;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)dest +
+ 1 * 0),
+ __gen_e_acsl_if,dest,
+ (void *)(& dest));
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read((char *)dest + (0 .. n - 1));
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","memcpy",
+ "separated_guard: \\valid_read((char *)dest + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",95);
+ __gen_e_acsl__4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_2 = 1UL * __gen_e_acsl__4;
+ if (__gen_e_acsl_size_2 <= 0UL) __gen_e_acsl_if_2 = 0UL;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)((char *)src +
+ 1 * 0),
+ __gen_e_acsl_if_2,
+ (void *)src,
+ (void *)(& src));
+ /*@ assert
+ E_ACSL: separated_guard: \valid_read((char *)src + (0 .. n - 1));
+ */
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","memcpy",
+ "separated_guard: \\valid_read((char *)src + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",95);
+ __gen_e_acsl__5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__5;
+ if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_3 = 0UL;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size_4 = 1UL * __gen_e_acsl__6;
+ if (__gen_e_acsl_size_4 <= 0UL) __gen_e_acsl_if_4 = 0UL;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_separated = __e_acsl_separated((size_t)2,
+ (char *)dest + 1 * 0,
+ __gen_e_acsl_if_3,
+ (char *)src + 1 * 0,
+ __gen_e_acsl_if_4);
+ __e_acsl_assert(__gen_e_acsl_separated,"Precondition","memcpy",
+ "\\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",95);
+ __e_acsl_temporal_reset_parameters();
+ __e_acsl_temporal_reset_return();
+ __e_acsl_temporal_save_nreferent_parameter((void *)(& dest),0U);
+ __e_acsl_temporal_save_nreferent_parameter((void *)(& src),1U);
+ __e_acsl_temporal_memcpy(dest,(void *)src,n);
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
__gen_e_acsl_at = dest;
__retres = memcpy(dest,src,n);
__e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","memcpy",
"\\result == \\old(dest)","FRAMAC_SHARE/libc/string.h",99);
+ __e_acsl_delete_block((void *)(& src));
__e_acsl_delete_block((void *)(& dest));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle
index 101a07c7fb68b6985cbe8896de359855582c12bd..e91a2fc3fa0ca04f001d5e2fd86af2e94f0cb603 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle
@@ -5,8 +5,6 @@
[e-acsl] Warning: annotating undefined function `memset':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:92: Warning:
- E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:115: Warning:
E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
@@ -22,8 +20,6 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:93: Warning:
E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
- E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:92: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
@@ -32,6 +28,8 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] FRAMAC_SHARE/libc/string.h:95: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/string.h:98: Warning:
function __gen_e_acsl_memcpy: postcondition 'copied_contents' got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/string.h:118: Warning: