diff --git a/share/libc/argz.c b/share/libc/argz.c
index fdf81545c9a8136127b9ea21e3584b963a0552d3..23f6b4a509c6329e03919bce467d022aa0eccde6 100644
--- a/share/libc/argz.c
+++ b/share/libc/argz.c
@@ -43,7 +43,12 @@ void argz_stringify (char *argz, size_t len, int sep) {
}
}
-/*@ assigns *to, *to_len \from buf[0 .. buf_len - 1]; */
+/*@
+ assigns *to \from *to, indirect:*to_len, indirect:buf_len;
+ assigns *to_len \from *to_len, buf_len;
+ assigns *to[0 .. \old(*to_len) + buf_len]
+ \from *to[0 .. \old(*to_len)], buf[0 .. buf_len];
+ */
static void str_append (char **to, size_t *to_len, const char *buf,
const size_t buf_len) {
size_t new_len = *to_len + buf_len;
diff --git a/tests/libc/oracle/argz_c.res.oracle b/tests/libc/oracle/argz_c.res.oracle
index 5351b22e36e6ed43c5e5350e2450c2ffd276e69b..5e0b1929b42c7aa9d766a2fbcef20238c149fbcb 100644
--- a/tests/libc/oracle/argz_c.res.oracle
+++ b/tests/libc/oracle/argz_c.res.oracle
@@ -65,24 +65,24 @@
[eva] computing for function argz_create <- main.
Called from argz_c.c:20.
-[eva] FRAMAC_SHARE/libc/argz.c:241: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:241:
- function strlen: precondition 'valid_string_s' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:241: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:241: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:246: Call to builtin malloc
+[eva] FRAMAC_SHARE/libc/argz.c:246: Call to builtin strlen
[eva] FRAMAC_SHARE/libc/argz.c:246:
- allocating variable __malloc_argz_create_l246
+ function strlen: precondition 'valid_string_s' got status valid.
+[eva] FRAMAC_SHARE/libc/argz.c:246: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:246: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:251: Call to builtin malloc
+[eva] FRAMAC_SHARE/libc/argz.c:251:
+ allocating variable __malloc_argz_create_l251
[eva] computing for function stpcpy <- argz_create <- main.
- Called from FRAMAC_SHARE/libc/argz.c:251.
+ Called from FRAMAC_SHARE/libc/argz.c:256.
[eva] Recording results for stpcpy
[eva] Done for function stpcpy
[eva] computing for function stpcpy <- argz_create <- main.
- Called from FRAMAC_SHARE/libc/argz.c:251.
+ Called from FRAMAC_SHARE/libc/argz.c:256.
[eva] Recording results for stpcpy
[eva] Done for function stpcpy
[eva] computing for function stpcpy <- argz_create <- main.
- Called from FRAMAC_SHARE/libc/argz.c:251.
+ Called from FRAMAC_SHARE/libc/argz.c:256.
[eva] Recording results for stpcpy
[eva] Done for function stpcpy
[eva] Recording results for argz_create
@@ -96,12 +96,12 @@
[eva] argz_c.c:23: function free: precondition 'freeable' got status valid.
[eva] computing for function argz_create_sep <- main.
Called from argz_c.c:25.
-[eva] FRAMAC_SHARE/libc/argz.c:197: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:197:
+[eva] FRAMAC_SHARE/libc/argz.c:202: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:202:
function strlen: precondition 'valid_string_s' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:203: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/argz.c:203:
- allocating variable __malloc_argz_create_sep_l203
+[eva] FRAMAC_SHARE/libc/argz.c:208: Call to builtin malloc
+[eva] FRAMAC_SHARE/libc/argz.c:208:
+ allocating variable __malloc_argz_create_sep_l208
[eva] Recording results for argz_create_sep
[eva] Done for function argz_create_sep
[eva] computing for function exit <- main.
@@ -115,11 +115,11 @@
[eva] Done for function __FC_assert
[eva] computing for function argz_count <- main.
Called from argz_c.c:28.
-[eva] FRAMAC_SHARE/libc/argz.c:261: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:261:
+[eva] FRAMAC_SHARE/libc/argz.c:266: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:266:
function strlen: precondition 'valid_string_s' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:261: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:261: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:266: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:266: Call to builtin strlen
[eva] Recording results for argz_count
[eva] Done for function argz_count
[eva] computing for function __FC_assert <- main.
@@ -129,22 +129,22 @@
[eva] Done for function __FC_assert
[eva] computing for function argz_add <- main.
Called from argz_c.c:30.
-[eva] FRAMAC_SHARE/libc/argz.c:283: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:283:
+[eva] FRAMAC_SHARE/libc/argz.c:288: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:288:
function strlen: precondition 'valid_string_s' got status valid.
[eva] computing for function argz_append <- argz_add <- main.
- Called from FRAMAC_SHARE/libc/argz.c:283.
-[eva] FRAMAC_SHARE/libc/argz.c:272: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:272:
+ Called from FRAMAC_SHARE/libc/argz.c:288.
+[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:277:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:272:
- allocating variable __realloc_argz_append_l272
-[eva] FRAMAC_SHARE/libc/argz.c:274: Call to builtin memcpy
-[eva] FRAMAC_SHARE/libc/argz.c:274:
+[eva] FRAMAC_SHARE/libc/argz.c:277:
+ allocating variable __realloc_argz_append_l277
+[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
+[eva] FRAMAC_SHARE/libc/argz.c:279:
function memcpy: precondition 'valid_dest' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:274:
+[eva] FRAMAC_SHARE/libc/argz.c:279:
function memcpy: precondition 'valid_src' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:274:
+[eva] FRAMAC_SHARE/libc/argz.c:279:
function memcpy: precondition 'separation' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
@@ -162,14 +162,14 @@
[eva] Done for function __FC_assert
[eva] computing for function argz_add_sep <- main.
Called from argz_c.c:33.
-[eva] FRAMAC_SHARE/libc/argz.c:288: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:288:
+[eva] FRAMAC_SHARE/libc/argz.c:293: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:293:
function strlen: precondition 'valid_string_s' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:294: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:294:
+[eva] FRAMAC_SHARE/libc/argz.c:299: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:299:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:294:
- allocating variable __realloc_argz_add_sep_l294
+[eva] FRAMAC_SHARE/libc/argz.c:299:
+ allocating variable __realloc_argz_add_sep_l299
[eva] Recording results for argz_add_sep
[eva] Done for function argz_add_sep
[eva] computing for function exit <- main.
@@ -182,12 +182,12 @@
[eva] Done for function __FC_assert
[eva] computing for function argz_count <- main.
Called from argz_c.c:36.
-[eva] FRAMAC_SHARE/libc/argz.c:261: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:261: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:261: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:261: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:261: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:261: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:266: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:266: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:266: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:266: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:266: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:266: Call to builtin strlen
[eva] Recording results for argz_count
[eva] Done for function argz_count
[eva] computing for function __FC_assert <- main.
@@ -197,10 +197,10 @@
[eva] Done for function __FC_assert
[eva] computing for function argz_append <- main.
Called from argz_c.c:38.
-[eva] FRAMAC_SHARE/libc/argz.c:272: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:272:
- allocating variable __realloc_argz_append_l272_0
-[eva] FRAMAC_SHARE/libc/argz.c:274: Call to builtin memcpy
+[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:277:
+ allocating variable __realloc_argz_append_l277_0
+[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
[eva] Done for function argz_append
[eva] computing for function exit <- main.
@@ -213,13 +213,13 @@
[eva] Done for function __FC_assert
[eva] computing for function argz_add <- main.
Called from argz_c.c:41.
-[eva] FRAMAC_SHARE/libc/argz.c:283: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:288: Call to builtin strlen
[eva] computing for function argz_append <- argz_add <- main.
- Called from FRAMAC_SHARE/libc/argz.c:283.
-[eva] FRAMAC_SHARE/libc/argz.c:272: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:272:
- allocating variable __realloc_argz_append_l272_1
-[eva] FRAMAC_SHARE/libc/argz.c:274: Call to builtin memcpy
+ Called from FRAMAC_SHARE/libc/argz.c:288.
+[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:277:
+ allocating variable __realloc_argz_append_l277_1
+[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
[eva] Done for function argz_append
[eva] Recording results for argz_add
@@ -234,53 +234,53 @@
[eva] Done for function __FC_assert
[eva] computing for function argz_replace <- main.
Called from argz_c.c:45.
-[eva] FRAMAC_SHARE/libc/argz.c:73: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:73:
+[eva] FRAMAC_SHARE/libc/argz.c:78: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:78:
function strlen: precondition 'valid_string_s' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:73: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:73:
+[eva] FRAMAC_SHARE/libc/argz.c:78: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:78:
function strlen: precondition 'valid_string_s' got status valid.
[eva] computing for function argz_next <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:75.
+ Called from FRAMAC_SHARE/libc/argz.c:80.
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function strstr <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:76.
+ Called from FRAMAC_SHARE/libc/argz.c:81.
[eva] Recording results for strstr
[eva] Done for function strstr
[eva] computing for function argz_next <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:75.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
-[eva] FRAMAC_SHARE/libc/argz.c:130:
+ Called from FRAMAC_SHARE/libc/argz.c:80.
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
+[eva] FRAMAC_SHARE/libc/argz.c:135:
function strchr: precondition 'valid_string_s' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:202:
cannot evaluate ACSL term, unsupported logic var p
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function strstr <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:76.
+ Called from FRAMAC_SHARE/libc/argz.c:81.
[eva] Recording results for strstr
[eva] Done for function strstr
[eva] computing for function argz_next <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:75.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
+ Called from FRAMAC_SHARE/libc/argz.c:80.
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function strstr <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:76.
+ Called from FRAMAC_SHARE/libc/argz.c:81.
[eva] Recording results for strstr
[eva] Done for function strstr
[eva] computing for function argz_next <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:75.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
+ Called from FRAMAC_SHARE/libc/argz.c:80.
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function strstr <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:76.
+ Called from FRAMAC_SHARE/libc/argz.c:81.
[eva] Recording results for strstr
[eva] Done for function strstr
[eva] computing for function strndup <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:80.
+ Called from FRAMAC_SHARE/libc/argz.c:85.
[eva:loop-unroll:auto] FRAMAC_SHARE/libc/string.c:336: Automatic loop unrolling.
[eva] FRAMAC_SHARE/libc/string.c:339: Call to builtin malloc
[eva] FRAMAC_SHARE/libc/string.c:339: allocating variable __malloc_strndup_l339
@@ -294,143 +294,143 @@
[eva] Recording results for strndup
[eva] Done for function strndup
[eva] computing for function str_append <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:83.
-[eva] FRAMAC_SHARE/libc/argz.c:50: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:50:
+ Called from FRAMAC_SHARE/libc/argz.c:88.
+[eva] FRAMAC_SHARE/libc/argz.c:55: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:55:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:50: allocating variable __realloc_str_append_l50
+[eva] FRAMAC_SHARE/libc/argz.c:55: allocating variable __realloc_str_append_l55
[eva] computing for function mempcpy <- str_append <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:53.
+ Called from FRAMAC_SHARE/libc/argz.c:58.
[eva:loop-unroll:auto] FRAMAC_SHARE/libc/string.c:54: Automatic loop unrolling.
[eva] Recording results for mempcpy
[eva] Done for function mempcpy
-[eva] FRAMAC_SHARE/libc/argz.c:57: Call to builtin free
-[eva] FRAMAC_SHARE/libc/argz.c:57:
+[eva] FRAMAC_SHARE/libc/argz.c:62: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:62:
function free: precondition 'freeable' got status valid.
[eva] Recording results for str_append
[eva] Done for function str_append
[eva] computing for function strstr <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:85.
+ Called from FRAMAC_SHARE/libc/argz.c:90.
[eva] Recording results for strstr
[eva] Done for function strstr
-[eva] FRAMAC_SHARE/libc/argz.c:90: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:90:
+[eva] FRAMAC_SHARE/libc/argz.c:95: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:95:
function strlen: precondition 'valid_string_s' got status valid.
[eva] computing for function str_append <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:90.
-[eva] FRAMAC_SHARE/libc/argz.c:50: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:50:
- allocating variable __realloc_str_append_l50_0
+ Called from FRAMAC_SHARE/libc/argz.c:95.
+[eva] FRAMAC_SHARE/libc/argz.c:55: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:55:
+ allocating variable __realloc_str_append_l55_0
[eva] computing for function mempcpy <- str_append <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:53.
+ Called from FRAMAC_SHARE/libc/argz.c:58.
[eva] Recording results for mempcpy
[eva] Done for function mempcpy
-[eva] FRAMAC_SHARE/libc/argz.c:57: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:62: Call to builtin free
[eva] Recording results for str_append
[eva] Done for function str_append
[eva] computing for function argz_append <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:99.
-[eva] FRAMAC_SHARE/libc/argz.c:272: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:272:
- allocating variable __realloc_argz_append_l272_2
-[eva] FRAMAC_SHARE/libc/argz.c:274: Call to builtin memcpy
+ Called from FRAMAC_SHARE/libc/argz.c:104.
+[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:277:
+ allocating variable __realloc_argz_append_l277_2
+[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
[eva] Done for function argz_append
[eva] computing for function argz_add <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:103.
-[eva] FRAMAC_SHARE/libc/argz.c:283: Call to builtin strlen
+ Called from FRAMAC_SHARE/libc/argz.c:108.
+[eva] FRAMAC_SHARE/libc/argz.c:288: Call to builtin strlen
[eva] computing for function argz_append <- argz_add <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:283.
-[eva] FRAMAC_SHARE/libc/argz.c:272: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:272:
- allocating variable __realloc_argz_append_l272_3
-[eva] FRAMAC_SHARE/libc/argz.c:274: Call to builtin memcpy
+ Called from FRAMAC_SHARE/libc/argz.c:288.
+[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:277:
+ allocating variable __realloc_argz_append_l277_3
+[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
[eva] Done for function argz_append
[eva] Recording results for argz_add
[eva] Done for function argz_add
-[eva] FRAMAC_SHARE/libc/argz.c:104: Call to builtin free
-[eva] FRAMAC_SHARE/libc/argz.c:104:
+[eva] FRAMAC_SHARE/libc/argz.c:109: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:109:
function free: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:104: Call to builtin free
-[eva] FRAMAC_SHARE/libc/argz.c:104: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:109: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:109: Call to builtin free
[eva] computing for function argz_next <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:75.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
+ Called from FRAMAC_SHARE/libc/argz.c:80.
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function strstr <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:76.
+ Called from FRAMAC_SHARE/libc/argz.c:81.
[eva] Recording results for strstr
[eva] Done for function strstr
[eva] computing for function argz_add <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:111.
-[eva] FRAMAC_SHARE/libc/argz.c:283: Call to builtin strlen
+ Called from FRAMAC_SHARE/libc/argz.c:116.
+[eva] FRAMAC_SHARE/libc/argz.c:288: Call to builtin strlen
[eva] computing for function argz_append <- argz_add <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:283.
-[eva] FRAMAC_SHARE/libc/argz.c:272: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:272:
- allocating variable __realloc_argz_append_l272_4
-[eva] FRAMAC_SHARE/libc/argz.c:274: Call to builtin memcpy
+ Called from FRAMAC_SHARE/libc/argz.c:288.
+[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:277:
+ allocating variable __realloc_argz_append_l277_4
+[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
[eva] Done for function argz_append
[eva] Recording results for argz_add
[eva] Done for function argz_add
[eva] computing for function argz_next <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:75.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
+ Called from FRAMAC_SHARE/libc/argz.c:80.
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function strstr <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:76.
+ Called from FRAMAC_SHARE/libc/argz.c:81.
[eva] Recording results for strstr
[eva] Done for function strstr
[eva] computing for function argz_add <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:111.
-[eva] FRAMAC_SHARE/libc/argz.c:283: Call to builtin strlen
+ Called from FRAMAC_SHARE/libc/argz.c:116.
+[eva] FRAMAC_SHARE/libc/argz.c:288: Call to builtin strlen
[eva] computing for function argz_append <- argz_add <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:283.
-[eva] FRAMAC_SHARE/libc/argz.c:272: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:272:
- allocating variable __realloc_argz_append_l272_5
-[eva] FRAMAC_SHARE/libc/argz.c:274: Call to builtin memcpy
+ Called from FRAMAC_SHARE/libc/argz.c:288.
+[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:277:
+ allocating variable __realloc_argz_append_l277_5
+[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
[eva] Done for function argz_append
[eva] Recording results for argz_add
[eva] Done for function argz_add
[eva] computing for function argz_next <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:75.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
+ Called from FRAMAC_SHARE/libc/argz.c:80.
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function strstr <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:76.
+ Called from FRAMAC_SHARE/libc/argz.c:81.
[eva] Recording results for strstr
[eva] Done for function strstr
[eva] computing for function argz_add <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:111.
-[eva] FRAMAC_SHARE/libc/argz.c:283: Call to builtin strlen
+ Called from FRAMAC_SHARE/libc/argz.c:116.
+[eva] FRAMAC_SHARE/libc/argz.c:288: Call to builtin strlen
[eva] computing for function argz_append <- argz_add <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:283.
-[eva] FRAMAC_SHARE/libc/argz.c:272: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:272:
- allocating variable __realloc_argz_append_l272_6
-[eva] FRAMAC_SHARE/libc/argz.c:274: Call to builtin memcpy
+ Called from FRAMAC_SHARE/libc/argz.c:288.
+[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:277:
+ allocating variable __realloc_argz_append_l277_6
+[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
[eva] Done for function argz_append
[eva] Recording results for argz_add
[eva] Done for function argz_add
[eva] computing for function argz_next <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:75.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
+ Called from FRAMAC_SHARE/libc/argz.c:80.
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function strstr <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:76.
+ Called from FRAMAC_SHARE/libc/argz.c:81.
[eva] Recording results for strstr
[eva] Done for function strstr
[eva] computing for function strndup <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:80.
+ Called from FRAMAC_SHARE/libc/argz.c:85.
[eva] FRAMAC_SHARE/libc/string.c:339: Call to builtin malloc
[eva] FRAMAC_SHARE/libc/string.c:339:
allocating variable __malloc_strndup_l339_0
@@ -438,65 +438,65 @@
[eva] Recording results for strndup
[eva] Done for function strndup
[eva] computing for function str_append <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:83.
-[eva] FRAMAC_SHARE/libc/argz.c:50: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:50:
- allocating variable __realloc_str_append_l50_1
+ Called from FRAMAC_SHARE/libc/argz.c:88.
+[eva] FRAMAC_SHARE/libc/argz.c:55: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:55:
+ allocating variable __realloc_str_append_l55_1
[eva] computing for function mempcpy <- str_append <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:53.
+ Called from FRAMAC_SHARE/libc/argz.c:58.
[eva] Recording results for mempcpy
[eva] Done for function mempcpy
-[eva] FRAMAC_SHARE/libc/argz.c:57: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:62: Call to builtin free
[eva] Recording results for str_append
[eva] Done for function str_append
[eva] computing for function strstr <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:85.
+ Called from FRAMAC_SHARE/libc/argz.c:90.
[eva] Recording results for strstr
[eva] Done for function strstr
-[eva] FRAMAC_SHARE/libc/argz.c:90: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:95: Call to builtin strlen
[eva] computing for function str_append <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:90.
-[eva] FRAMAC_SHARE/libc/argz.c:50: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:50:
- allocating variable __realloc_str_append_l50_2
+ Called from FRAMAC_SHARE/libc/argz.c:95.
+[eva] FRAMAC_SHARE/libc/argz.c:55: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:55:
+ allocating variable __realloc_str_append_l55_2
[eva] computing for function mempcpy <- str_append <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:53.
+ Called from FRAMAC_SHARE/libc/argz.c:58.
[eva] Recording results for mempcpy
[eva] Done for function mempcpy
-[eva] FRAMAC_SHARE/libc/argz.c:57: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:62: Call to builtin free
[eva] Recording results for str_append
[eva] Done for function str_append
[eva] computing for function argz_add <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:103.
-[eva] FRAMAC_SHARE/libc/argz.c:283: Call to builtin strlen
+ Called from FRAMAC_SHARE/libc/argz.c:108.
+[eva] FRAMAC_SHARE/libc/argz.c:288: Call to builtin strlen
[eva] computing for function argz_append <- argz_add <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:283.
-[eva] FRAMAC_SHARE/libc/argz.c:272: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:272:
- allocating variable __realloc_argz_append_l272_7
-[eva] FRAMAC_SHARE/libc/argz.c:274: Call to builtin memcpy
+ Called from FRAMAC_SHARE/libc/argz.c:288.
+[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:277:
+ allocating variable __realloc_argz_append_l277_7
+[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
[eva] Done for function argz_append
[eva] Recording results for argz_add
[eva] Done for function argz_add
-[eva] FRAMAC_SHARE/libc/argz.c:104: Call to builtin free
-[eva] FRAMAC_SHARE/libc/argz.c:104: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:109: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:109: Call to builtin free
[eva] computing for function argz_next <- argz_replace <- main.
- Called from FRAMAC_SHARE/libc/argz.c:75.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
+ Called from FRAMAC_SHARE/libc/argz.c:80.
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
[eva] Recording results for argz_next
[eva] Done for function argz_next
-[eva] FRAMAC_SHARE/libc/argz.c:116: Call to builtin free
-[eva] FRAMAC_SHARE/libc/argz.c:116:
- function free: precondition 'freeable' got status valid.
[eva] FRAMAC_SHARE/libc/argz.c:121: Call to builtin free
[eva] FRAMAC_SHARE/libc/argz.c:121:
function free: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:121: Call to builtin free
-[eva] FRAMAC_SHARE/libc/argz.c:121: Call to builtin free
-[eva] FRAMAC_SHARE/libc/argz.c:121: Call to builtin free
-[eva] FRAMAC_SHARE/libc/argz.c:121: Call to builtin free
-[eva] FRAMAC_SHARE/libc/argz.c:121: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:126: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:126:
+ function free: precondition 'freeable' got status valid.
+[eva] FRAMAC_SHARE/libc/argz.c:126: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:126: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:126: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:126: Call to builtin free
+[eva] FRAMAC_SHARE/libc/argz.c:126: Call to builtin free
[eva] Recording results for argz_replace
[eva] Done for function argz_replace
[eva] computing for function exit <- main.
@@ -523,18 +523,18 @@
[eva] Done for function __FC_assert
[eva] computing for function argz_next <- main.
Called from argz_c.c:52.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function argz_delete <- main.
Called from argz_c.c:54.
-[eva] FRAMAC_SHARE/libc/argz.c:185: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:185:
+[eva] FRAMAC_SHARE/libc/argz.c:190: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:190:
function strlen: precondition 'valid_string_s' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:187: Call to builtin memmove
-[eva] FRAMAC_SHARE/libc/argz.c:187:
+[eva] FRAMAC_SHARE/libc/argz.c:192: Call to builtin memmove
+[eva] FRAMAC_SHARE/libc/argz.c:192:
function memmove: precondition 'valid_dest' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:187:
+[eva] FRAMAC_SHARE/libc/argz.c:192:
function memmove: precondition 'valid_src' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:141:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
@@ -551,12 +551,12 @@
[eva] Done for function argz_next
[eva] computing for function argz_next <- main.
Called from argz_c.c:58.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function argz_next <- main.
Called from argz_c.c:58.
-[eva] FRAMAC_SHARE/libc/argz.c:130: Call to builtin strchr
+[eva] FRAMAC_SHARE/libc/argz.c:135: Call to builtin strchr
[eva] Recording results for argz_next
[eva] Done for function argz_next
[eva] computing for function __FC_assert <- main.
@@ -566,8 +566,8 @@
[eva] Done for function __FC_assert
[eva] computing for function argz_delete <- main.
Called from argz_c.c:61.
-[eva] FRAMAC_SHARE/libc/argz.c:185: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:187: Call to builtin memmove
+[eva] FRAMAC_SHARE/libc/argz.c:190: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:192: Call to builtin memmove
[eva] Recording results for argz_delete
[eva] Done for function argz_delete
[eva] computing for function __FC_assert <- main.
@@ -581,23 +581,23 @@
[eva] Done for function argz_next
[eva] computing for function argz_insert <- main.
Called from argz_c.c:64.
-[eva] FRAMAC_SHARE/libc/argz.c:154: Call to builtin strlen
-[eva] FRAMAC_SHARE/libc/argz.c:154:
+[eva] FRAMAC_SHARE/libc/argz.c:159: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/argz.c:159:
function strlen: precondition 'valid_string_s' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:158: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:158:
+[eva] FRAMAC_SHARE/libc/argz.c:163: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:163:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:158:
- allocating variable __realloc_argz_insert_l158
-[eva] FRAMAC_SHARE/libc/argz.c:162: Call to builtin memmove
-[eva] FRAMAC_SHARE/libc/argz.c:162:
+[eva] FRAMAC_SHARE/libc/argz.c:163:
+ allocating variable __realloc_argz_insert_l163
+[eva] FRAMAC_SHARE/libc/argz.c:167: Call to builtin memmove
+[eva] FRAMAC_SHARE/libc/argz.c:167:
function memmove: precondition 'valid_dest' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:162:
+[eva] FRAMAC_SHARE/libc/argz.c:167:
function memmove: precondition 'valid_src' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:163: Call to builtin memmove
-[eva] FRAMAC_SHARE/libc/argz.c:163:
+[eva] FRAMAC_SHARE/libc/argz.c:168: Call to builtin memmove
+[eva] FRAMAC_SHARE/libc/argz.c:168:
function memmove: precondition 'valid_dest' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:163:
+[eva] FRAMAC_SHARE/libc/argz.c:168:
function memmove: precondition 'valid_src' got status valid.
[eva] Recording results for argz_insert
[eva] Done for function argz_insert
@@ -612,14 +612,14 @@
[eva] computing for function argz_insert <- main.
Called from argz_c.c:67.
[eva] computing for function argz_add <- argz_insert <- main.
- Called from FRAMAC_SHARE/libc/argz.c:143.
-[eva] FRAMAC_SHARE/libc/argz.c:283: Call to builtin strlen
+ Called from FRAMAC_SHARE/libc/argz.c:148.
+[eva] FRAMAC_SHARE/libc/argz.c:288: Call to builtin strlen
[eva] computing for function argz_append <- argz_add <- argz_insert <- main.
- Called from FRAMAC_SHARE/libc/argz.c:283.
-[eva] FRAMAC_SHARE/libc/argz.c:272: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:272:
- allocating variable __realloc_argz_append_l272_8
-[eva] FRAMAC_SHARE/libc/argz.c:274: Call to builtin memcpy
+ Called from FRAMAC_SHARE/libc/argz.c:288.
+[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
+[eva] FRAMAC_SHARE/libc/argz.c:277:
+ allocating variable __realloc_argz_append_l277_8
+[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
[eva] Done for function argz_append
[eva] Recording results for argz_add
@@ -642,45 +642,45 @@
[eva:final-states] Values at end of function mempcpy:
i ∈ {0; 3}
__retres ∈
- {{ (void *)&__realloc_str_append_l50[3] ;
- (void *)&__realloc_str_append_l50_0[3] ;
- (void *)&__realloc_str_append_l50_1[3] ;
- (void *)&__realloc_str_append_l50_2[3] }}
- __realloc_str_append_l50[0] ∈ {98}
+ {{ (void *)&__realloc_str_append_l55[3] ;
+ (void *)&__realloc_str_append_l55_0[3] ;
+ (void *)&__realloc_str_append_l55_1[3] ;
+ (void *)&__realloc_str_append_l55_2[3] }}
+ __realloc_str_append_l55[0] ∈ {98}
[1] ∈ {108}
[2] ∈ {97}
[3] ∈ UNINITIALIZED
- __realloc_str_append_l50_1[0] ∈ {98}
+ __realloc_str_append_l55_1[0] ∈ {98}
[1] ∈ {108}
[2] ∈ {97}
[3] ∈ UNINITIALIZED
[eva:final-states] Values at end of function argz_append:
dst ∈
- {{ NULL ; &__realloc_argz_append_l272_2[0] ;
- &__realloc_argz_append_l272_3[0] ; &__realloc_argz_append_l272_4[0] ;
- &__realloc_argz_append_l272_5[0] ; &__realloc_argz_append_l272_6[0] ;
- &__realloc_argz_append_l272_7[0] }}
+ {{ NULL ; &__realloc_argz_append_l277_2[0] ;
+ &__realloc_argz_append_l277_3[0] ; &__realloc_argz_append_l277_4[0] ;
+ &__realloc_argz_append_l277_5[0] ; &__realloc_argz_append_l277_6[0] ;
+ &__realloc_argz_append_l277_7[0] }}
dst_len ∈ {0; 7; 11; 14; 17; 19; 23}
new_argz_len ∈ {7; 10; 11; 14; 17; 18; 19; 21; 23; 24}
new_argz ∈
- {{ NULL ; &__realloc_argz_append_l272[0] ;
- &__realloc_argz_append_l272_0[0] ;
- &__realloc_argz_append_l272_1[0] ;
- &__realloc_argz_append_l272_2[0] ;
- &__realloc_argz_append_l272_3[0] ;
- &__realloc_argz_append_l272_4[0] ;
- &__realloc_argz_append_l272_5[0] ;
- &__realloc_argz_append_l272_6[0] ;
- &__realloc_argz_append_l272_7[0] ;
- &__realloc_argz_append_l272_8[0] }}
+ {{ NULL ; &__realloc_argz_append_l277[0] ;
+ &__realloc_argz_append_l277_0[0] ;
+ &__realloc_argz_append_l277_1[0] ;
+ &__realloc_argz_append_l277_2[0] ;
+ &__realloc_argz_append_l277_3[0] ;
+ &__realloc_argz_append_l277_4[0] ;
+ &__realloc_argz_append_l277_5[0] ;
+ &__realloc_argz_append_l277_6[0] ;
+ &__realloc_argz_append_l277_7[0] ;
+ &__realloc_argz_append_l277_8[0] }}
argz ∈
- {{ &__malloc_argz_create_sep_l203[0] ; &__realloc_argz_append_l272[0] ;
- &__realloc_argz_add_sep_l294[0] ; &__realloc_argz_append_l272_0[0] ;
- &__realloc_argz_append_l272_1[0] ; &__realloc_argz_insert_l158[0] ;
- &__realloc_argz_append_l272_8[0] }}
+ {{ &__malloc_argz_create_sep_l208[0] ; &__realloc_argz_append_l277[0] ;
+ &__realloc_argz_add_sep_l299[0] ; &__realloc_argz_append_l277_0[0] ;
+ &__realloc_argz_append_l277_1[0] ; &__realloc_argz_insert_l163[0] ;
+ &__realloc_argz_append_l277_8[0] }}
len ∈ {7; 10; 16; 18; 21; 24}
__retres ∈ {0; 12}
- __realloc_argz_append_l272[0] ∈ {97}
+ __realloc_argz_append_l277[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -690,7 +690,7 @@
[7] ∈ {101}
[8] ∈ {102}
[9] ∈ {0}
- __realloc_argz_append_l272_0[0] ∈ {97}
+ __realloc_argz_append_l277_0[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -708,7 +708,7 @@
[15] ∈ {0}
[16] ∈ {107}
[17] ∈ {0}
- __realloc_argz_append_l272_1[0] ∈ {97}
+ __realloc_argz_append_l277_1[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -729,14 +729,14 @@
[18] ∈ {101}
[19] ∈ {102}
[20] ∈ {0}
- __realloc_argz_append_l272_2[0] ∈ {97}
+ __realloc_argz_append_l277_2[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
[4] ∈ {99}
[5] ∈ {100}
[6] ∈ {0}
- __realloc_argz_append_l272_3[0] ∈ {97}
+ __realloc_argz_append_l277_3[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -747,7 +747,7 @@
[8] ∈ {108}
[9] ∈ {97}
[10] ∈ {0}
- __realloc_argz_append_l272_4[0] ∈ {97}
+ __realloc_argz_append_l277_4[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -761,7 +761,7 @@
[11] ∈ {103}
[12] ∈ {104}
[13] ∈ {0}
- __realloc_argz_append_l272_5[0] ∈ {97}
+ __realloc_argz_append_l277_5[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -778,7 +778,7 @@
[14] ∈ {105}
[15] ∈ {106}
[16] ∈ {0}
- __realloc_argz_append_l272_6[0] ∈ {97}
+ __realloc_argz_append_l277_6[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -797,7 +797,7 @@
[16] ∈ {0}
[17] ∈ {107}
[18] ∈ {0}
- __realloc_argz_append_l272_7[0] ∈ {97}
+ __realloc_argz_append_l277_7[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -820,7 +820,7 @@
[20] ∈ {108}
[21] ∈ {97}
[22] ∈ {0}
- __realloc_argz_append_l272_8[0] ∈ {109}
+ __realloc_argz_append_l277_8[0] ∈ {109}
[1] ∈ {110}
[2] ∈ {111}
[3] ∈ {0}
@@ -845,8 +845,8 @@
[23] ∈ {0}
[eva:final-states] Values at end of function stpcpy:
i ∈ {2; 4}
- __retres ∈ {{ &__malloc_argz_create_l246{[4], [7], [12]} }}
- __malloc_argz_create_l246[0] ∈ {116}
+ __retres ∈ {{ &__malloc_argz_create_l251{[4], [7], [12]} }}
+ __malloc_argz_create_l251[0] ∈ {116}
[1] ∈ {104}
[2] ∈ {105}
[3] ∈ {115}
@@ -862,54 +862,54 @@
[eva:final-states] Values at end of function str_append:
new_len ∈ {3}
new_to ∈
- {{ NULL ; &__realloc_str_append_l50[0] ;
- &__realloc_str_append_l50_0[0] ; &__realloc_str_append_l50_1[0] ;
- &__realloc_str_append_l50_2[0] }}
+ {{ NULL ; &__realloc_str_append_l55[0] ;
+ &__realloc_str_append_l55_0[0] ; &__realloc_str_append_l55_1[0] ;
+ &__realloc_str_append_l55_2[0] }}
to_len ∈ {0; 3}
to ∈
- {{ NULL ; &__realloc_str_append_l50[0] ; &__realloc_str_append_l50_0[0] ;
- &__realloc_str_append_l50_1[0] ; &__realloc_str_append_l50_2[0] }}
- __realloc_str_append_l50[0] ∈ {98}
+ {{ NULL ; &__realloc_str_append_l55[0] ; &__realloc_str_append_l55_0[0] ;
+ &__realloc_str_append_l55_1[0] ; &__realloc_str_append_l55_2[0] }}
+ __realloc_str_append_l55[0] ∈ {98}
[1] ∈ {108}
[2] ∈ {97}
[3] ∈ {0}
- __realloc_str_append_l50_0[0] ∈ {98}
+ __realloc_str_append_l55_0[0] ∈ {98}
[1] ∈ {108}
[2] ∈ {97}
[3] ∈ {0}
- __realloc_str_append_l50_1[0] ∈ {98}
+ __realloc_str_append_l55_1[0] ∈ {98}
[1] ∈ {108}
[2] ∈ {97}
[3] ∈ {0}
- __realloc_str_append_l50_2[0] ∈ {98}
+ __realloc_str_append_l55_2[0] ∈ {98}
[1] ∈ {108}
[2] ∈ {97}
[3] ∈ {0}
[eva:final-states] Values at end of function argz_next:
entry ∈
{{ NULL ;
- &__realloc_argz_append_l272_1{[2], [4], [7], [10], [13], [16],
+ &__realloc_argz_append_l277_1{[2], [4], [7], [10], [13], [16],
[18], [21]} ;
- &__realloc_argz_append_l272_7{[2], [5]} }}
+ &__realloc_argz_append_l277_7{[2], [5]} }}
__retres ∈
{{ NULL ;
- &__realloc_argz_append_l272_1{[0], [2], [4], [7], [10], [13],
+ &__realloc_argz_append_l277_1{[0], [2], [4], [7], [10], [13],
[16], [18]} ;
- &__realloc_argz_append_l272_7{[0], [2], [5]} }}
+ &__realloc_argz_append_l277_7{[0], [2], [5]} }}
[eva:final-states] Values at end of function argz_add:
dst ∈
- {{ &__realloc_argz_append_l272_2[0] ; &__realloc_argz_append_l272_3[0] ;
- &__realloc_argz_append_l272_4[0] ; &__realloc_argz_append_l272_5[0] ;
- &__realloc_argz_append_l272_6[0] ;
- &__realloc_argz_append_l272_7[0] }}
+ {{ &__realloc_argz_append_l277_2[0] ; &__realloc_argz_append_l277_3[0] ;
+ &__realloc_argz_append_l277_4[0] ; &__realloc_argz_append_l277_5[0] ;
+ &__realloc_argz_append_l277_6[0] ;
+ &__realloc_argz_append_l277_7[0] }}
dst_len ∈ {7; 11; 14; 17; 19; 23}
argz ∈
- {{ &__malloc_argz_create_sep_l203[0] ; &__realloc_argz_append_l272[0] ;
- &__realloc_argz_append_l272_0[0] ;
- &__realloc_argz_append_l272_1[0] ; &__realloc_argz_insert_l158[0] ;
- &__realloc_argz_append_l272_8[0] }}
+ {{ &__malloc_argz_create_sep_l208[0] ; &__realloc_argz_append_l277[0] ;
+ &__realloc_argz_append_l277_0[0] ;
+ &__realloc_argz_append_l277_1[0] ; &__realloc_argz_insert_l163[0] ;
+ &__realloc_argz_append_l277_8[0] }}
len ∈ {7; 10; 18; 21; 24}
- __realloc_argz_append_l272[0] ∈ {97}
+ __realloc_argz_append_l277[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -919,7 +919,7 @@
[7] ∈ {101}
[8] ∈ {102}
[9] ∈ {0}
- __realloc_argz_append_l272_1[0] ∈ {97}
+ __realloc_argz_append_l277_1[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -940,7 +940,7 @@
[18] ∈ {101}
[19] ∈ {102}
[20] ∈ {0}
- __realloc_argz_append_l272_3[0] ∈ {97}
+ __realloc_argz_append_l277_3[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -951,7 +951,7 @@
[8] ∈ {108}
[9] ∈ {97}
[10] ∈ {0}
- __realloc_argz_append_l272_4[0] ∈ {97}
+ __realloc_argz_append_l277_4[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -965,7 +965,7 @@
[11] ∈ {103}
[12] ∈ {104}
[13] ∈ {0}
- __realloc_argz_append_l272_5[0] ∈ {97}
+ __realloc_argz_append_l277_5[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -982,7 +982,7 @@
[14] ∈ {105}
[15] ∈ {106}
[16] ∈ {0}
- __realloc_argz_append_l272_6[0] ∈ {97}
+ __realloc_argz_append_l277_6[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -1001,7 +1001,7 @@
[16] ∈ {0}
[17] ∈ {107}
[18] ∈ {0}
- __realloc_argz_append_l272_7[0] ∈ {97}
+ __realloc_argz_append_l277_7[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -1024,7 +1024,7 @@
[20] ∈ {108}
[21] ∈ {97}
[22] ∈ {0}
- __realloc_argz_append_l272_8[0] ∈ {109}
+ __realloc_argz_append_l277_8[0] ∈ {109}
[1] ∈ {110}
[2] ∈ {111}
[3] ∈ {0}
@@ -1049,10 +1049,10 @@
[23] ∈ {0}
[eva:final-states] Values at end of function argz_add_sep:
nlen ∈ {6}
- argz ∈ {{ NULL ; &__realloc_argz_add_sep_l294[0] }}
+ argz ∈ {{ NULL ; &__realloc_argz_add_sep_l299[0] }}
len ∈ {10; 16}
__retres ∈ {0; 12}
- __realloc_argz_add_sep_l294[0] ∈ {97}
+ __realloc_argz_add_sep_l299[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -1070,8 +1070,8 @@
[15] ∈ {0}
[eva:final-states] Values at end of function argz_count:
argz ∈
- {{ &__malloc_argz_create_sep_l203[7] ;
- &__realloc_argz_add_sep_l294[16] }}
+ {{ &__malloc_argz_create_sep_l208[7] ;
+ &__realloc_argz_add_sep_l299[16] }}
len ∈ {0}
count ∈ {3; 6}
[eva:final-states] Values at end of function argz_create:
@@ -1079,11 +1079,11 @@
argc ∈ {3}
tlen ∈ {13}
ap ∈ {{ &argv[3] }} or UNINITIALIZED
- p ∈ {{ &__malloc_argz_create_l246[13] }} or UNINITIALIZED
- argz ∈ {{ NULL ; &__malloc_argz_create_l246[0] }}
+ p ∈ {{ &__malloc_argz_create_l251[13] }} or UNINITIALIZED
+ argz ∈ {{ NULL ; &__malloc_argz_create_l251[0] }}
len ∈ {13} or UNINITIALIZED
__retres ∈ {0; 12}
- __malloc_argz_create_l246[0] ∈ {116}
+ __malloc_argz_create_l251[0] ∈ {116}
[1] ∈ {104}
[2] ∈ {105}
[3] ∈ {115}
@@ -1099,10 +1099,10 @@
[eva:final-states] Values at end of function argz_create_sep:
__fc_heap_status ∈ [--..--]
nlen ∈ {7; 8}
- argz ∈ {{ NULL ; &__malloc_argz_create_sep_l203[0] }}
+ argz ∈ {{ NULL ; &__malloc_argz_create_sep_l208[0] }}
len ∈ {7; 13}
__retres ∈ {0; 12}
- __malloc_argz_create_sep_l203[0] ∈ {97}
+ __malloc_argz_create_sep_l208[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
@@ -1112,7 +1112,7 @@
[7] ∈ UNINITIALIZED
[eva:final-states] Values at end of function argz_delete:
len ∈ {17; 21}
- __realloc_argz_append_l272_7[0] ∈ {97}
+ __realloc_argz_append_l277_7[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {99}
[3] ∈ {100}
@@ -1137,15 +1137,15 @@
[22] ∈ {0}
[eva:final-states] Values at end of function argz_insert:
before ∈
- {{ NULL ; &__realloc_argz_append_l272_7[0] ;
- &__realloc_argz_insert_l158[0] }}
+ {{ NULL ; &__realloc_argz_append_l277_7[0] ;
+ &__realloc_argz_insert_l163[0] }}
argz ∈
- {{ &__realloc_argz_append_l272_7[0] ; &__realloc_argz_insert_l158[0] ;
- &__realloc_argz_append_l272_8[0] }}
+ {{ &__realloc_argz_append_l277_7[0] ; &__realloc_argz_insert_l163[0] ;
+ &__realloc_argz_append_l277_8[0] }}
len ∈ {17; 21; 24}
- p ∈ {{ &__realloc_argz_append_l272_7[0] }} or ESCAPINGADDR
+ p ∈ {{ &__realloc_argz_append_l277_7[0] }} or ESCAPINGADDR
__retres ∈ {0; 12}
- __realloc_argz_insert_l158[0] ∈ {109}
+ __realloc_argz_insert_l163[0] ∈ {109}
[1] ∈ {110}
[2] ∈ {111}
[3] ∈ {0}
@@ -1166,7 +1166,7 @@
[18] ∈ {108}
[19] ∈ {97}
[20] ∈ {0}
- __realloc_argz_append_l272_8[0] ∈ {109}
+ __realloc_argz_append_l277_8[0] ∈ {109}
[1] ∈ {110}
[2] ∈ {111}
[3] ∈ {0}
@@ -1198,17 +1198,17 @@
__malloc_strndup_l339 ∈ {0}
__malloc_strndup_l339_0 ∈ {0}
[eva:final-states] Values at end of function strstr:
- __retres ∈ {{ NULL ; &__realloc_argz_append_l272_1{[7], [18]} }}
+ __retres ∈ {{ NULL ; &__realloc_argz_append_l277_1{[7], [18]} }}
[eva:final-states] Values at end of function argz_replace:
__fc_errno ∈ [--..--]
__fc_heap_status ∈ [--..--]
er ∈ {0; 12}
argz ∈
- {{ &__realloc_argz_append_l272_1[0] ;
- &__realloc_argz_append_l272_7[0] }}
+ {{ &__realloc_argz_append_l277_1[0] ;
+ &__realloc_argz_append_l277_7[0] }}
len ∈ {21; 23}
replace_count ∈ {2; 3}
- __realloc_argz_append_l272_7[0] ∈ {97}
+ __realloc_argz_append_l277_7[0] ∈ {97}
[1] ∈ {0}
[2] ∈ {98}
[3] ∈ {0}
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 825d7c5ddf07f1a2d857b8d4ade2fef0df9b25bf..1b655d0805bdd8b671356cd57c0fea4218b484b5 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2471,9 +2471,11 @@ void argz_stringify(char *argz, size_t len, int sep)
return;
}
-/*@ assigns *to, *to_len;
- assigns *to \from *(buf + (0 .. buf_len - 1));
- assigns *to_len \from *(buf + (0 .. buf_len - 1));
+/*@ assigns *to, *to_len, *(*(to + (0 .. \old(*to_len) + buf_len)));
+ assigns *to \from *to, (indirect: *to_len), (indirect: buf_len);
+ assigns *to_len \from *to_len, buf_len;
+ assigns *(*(to + (0 .. \old(*to_len) + buf_len)))
+ \from *(*(to + (0 .. \old(*to_len)))), *(buf + (0 .. buf_len));
*/
static void str_append(char **to, size_t *to_len, char const *buf,
size_t const buf_len)