From 7ce18d3c8324ca534118b6c14aac09e5222973b6 Mon Sep 17 00:00:00 2001
From: Boris Yakobowski <boris.yakobowski@cea.fr>
Date: Thu, 16 Nov 2017 23:12:59 +0100
Subject: [PATCH] [Tests] do not use Frama_C_foo directly
Instead, include the proper libc headers, with the specifications.
Otherwise, in the next commits(s), we won't have preconditions to evaluate, and the tests
will be come unsound
Changes:
- share/libc/stdlib.c: previous version of calloc in stdlib. used Frama_C_memset, which is idiotic since
- for non-free we now *have* a builtin for calloc
- stdlib.c is meant for people with non-free builtins
- same thing for tests/libs/string_c.c: the builtin was used
- nonfree/imprecise.c:
sizeof(v3), where v3 is an abstract struct, is evaluated slightly less precisely now.
We don't care as long as it does not crash.
- nonfree/strchr.c:
the test is buggy, the behavior was undefined
---
share/libc/__fc_builtin.h | 9 -
share/libc/stdlib.c | 8 +-
tests/libc/oracle/fc_libc.0.res.oracle | 73 ++-
tests/libc/oracle/fc_libc.1.res.oracle | 281 +++++----
tests/libc/oracle/stdlib_c.2.res.oracle | 80 +--
tests/libc/oracle/string_c.res.oracle | 57 +-
tests/libc/string_c.c | 2 +-
tests/libc/string_c_strchr.c | 2 +-
tests/non-free/alloc_weak.c | 2 +-
tests/non-free/{fam.i => fam.c} | 4 +-
tests/non-free/free.c | 46 ++
tests/non-free/free.i | 46 --
tests/non-free/gcc_zero_length_array.c | 2 +-
tests/non-free/imprecise-malloc-free.c | 27 +
tests/non-free/imprecise-malloc-free.i | 27 -
tests/non-free/imprecise.c | 10 +-
tests/non-free/memchr.c | 10 +-
tests/non-free/memcpy.c | 70 +--
tests/non-free/memcpy2.c | 10 +-
.../{memcpy_invalid.i => memcpy_invalid.c} | 8 +-
tests/non-free/memset.c | 73 +++
tests/non-free/memset.i | 73 ---
tests/non-free/oracle/fam.res.oracle | 20 +-
tests/non-free/oracle/free.res.oracle | 145 ++---
.../oracle/imprecise-malloc-free.res.oracle | 114 ++--
tests/non-free/oracle/imprecise.res.oracle | 263 +++++----
tests/non-free/oracle/memchr.res.oracle | 98 ++--
tests/non-free/oracle/memcpy.res.oracle | 535 ++++++++++++------
tests/non-free/oracle/memcpy2.res.oracle | 6 +-
.../non-free/oracle/memcpy_invalid.res.oracle | 38 +-
tests/non-free/oracle/memset.res.oracle | 154 ++---
.../non-free/oracle/precise_memset.res.oracle | 140 ++---
tests/non-free/oracle/strchr.res.oracle | 184 +++---
tests/non-free/oracle/strlen.res.oracle | 54 +-
tests/non-free/oracle/strnlen2.res.oracle | 98 ++--
tests/non-free/oracle/wcslen.res.oracle | 54 +-
tests/non-free/precise_memset.c | 40 +-
tests/non-free/realloc.c | 2 +-
tests/non-free/realloc_multiple.c | 2 +-
tests/non-free/strchr.c | 12 +-
tests/non-free/strlen.c | 34 +-
tests/non-free/strlen_align.c | 2 +-
tests/non-free/strnlen2.c | 32 +-
tests/non-free/wcslen.c | 34 +-
44 files changed, 1582 insertions(+), 1399 deletions(-)
rename tests/non-free/{fam.i => fam.c} (83%)
create mode 100644 tests/non-free/free.c
delete mode 100644 tests/non-free/free.i
create mode 100644 tests/non-free/imprecise-malloc-free.c
delete mode 100644 tests/non-free/imprecise-malloc-free.i
rename tests/non-free/{memcpy_invalid.i => memcpy_invalid.c} (62%)
create mode 100644 tests/non-free/memset.c
delete mode 100644 tests/non-free/memset.i
diff --git a/share/libc/__fc_builtin.h b/share/libc/__fc_builtin.h
index bfde1bc25c8..ec857d07f13 100644
--- a/share/libc/__fc_builtin.h
+++ b/share/libc/__fc_builtin.h
@@ -162,15 +162,6 @@ extern float Frama_C_float_interval(float min, float max);
*/
extern double Frama_C_double_interval(double min, double max);
-
-/*@ assigns ((char *)dest)[0..n-1] \from ((char *)src)[0..n-1];
- assigns \result \from dest;
-*/
-extern void* Frama_C_memcpy(void *dest, const void *src, size_t n);
-
-/*@ assigns ((char*)p)[0 .. s-1] \from c ; assigns \result \from p; */
-extern void* Frama_C_memset(void *p, int c, size_t s);
-
/*@ // Signals an error;
requires \false;
assigns \nothing;
diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index d98ffad873c..a760c3ac895 100644
--- a/share/libc/stdlib.c
+++ b/share/libc/stdlib.c
@@ -24,7 +24,7 @@
#include "stdlib.h"
#include "__fc_builtin.h"
#include "ctype.h"
-
+#include "string.h"
int abs (int i)
{
if (i < 0)
@@ -89,10 +89,6 @@ void *malloc(size_t size) {
#endif
#endif
-extern void Frama_C_free(void*base);
-void free(void *p) {
- if (p) Frama_C_free(p);
-}
void *calloc(size_t nmemb, size_t size)
{
@@ -102,6 +98,6 @@ void *calloc(size_t nmemb, size_t size)
return 0;
}
char *p = malloc(l);
- if (p) Frama_C_memset(p, 0, l);
+ if (p) memset(p, 0, l);
return p;
}
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 4eefa9b1c87..6049dbd1767 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -141,7 +141,7 @@ tests/libc/fc_libc.c:148:[value] assertion got status valid.
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
-[metrics] Defined functions (65)
+[metrics] Defined functions (64)
======================
Frama_C_double_interval (0 call); Frama_C_float_interval (0 call);
Frama_C_interval (0 call); Frama_C_nondet (5 calls);
@@ -149,20 +149,20 @@ tests/libc/fc_libc.c:148:[value] assertion got status valid.
__finitef (0 call); abs (0 call); atoi (0 call); calloc (0 call);
char_equal_ignore_case (1 call); fabs (0 call); fabsf (0 call);
feholdexcept (0 call); fesetenv (0 call); fetestexcept (0 call);
- free (0 call); imaxabs (0 call); imaxdiv (0 call); isalnum (0 call);
- isalpha (0 call); isblank (0 call); iscntrl (0 call); isdigit (3 calls);
- isgraph (0 call); islower (0 call); isprint (0 call); ispunct (0 call);
- isspace (1 call); isupper (0 call); isxdigit (0 call); localeconv (0 call);
- main (0 call); malloc (3 calls); memchr (0 call); memcmp (0 call);
- memcpy (2 calls); memmove (0 call); memrchr (0 call); memset (0 call);
- setlocale (0 call); strcasecmp (0 call); strcat (0 call); strchr (0 call);
- strcmp (0 call); strcpy (0 call); strdup (0 call); strerror (0 call);
- strlen (4 calls); strncat (0 call); strncmp (0 call); strncpy (0 call);
- strndup (0 call); strrchr (0 call); strstr (0 call); tolower (0 call);
- toupper (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
- wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
+ imaxabs (0 call); imaxdiv (0 call); isalnum (0 call); isalpha (0 call);
+ isblank (0 call); iscntrl (0 call); isdigit (3 calls); isgraph (0 call);
+ islower (0 call); isprint (0 call); ispunct (0 call); isspace (1 call);
+ isupper (0 call); isxdigit (0 call); localeconv (0 call); main (0 call);
+ malloc (3 calls); memchr (0 call); memcmp (0 call); memcpy (2 calls);
+ memmove (0 call); memrchr (0 call); memset (1 call); setlocale (0 call);
+ strcasecmp (0 call); strcat (0 call); strchr (0 call); strcmp (0 call);
+ strcpy (0 call); strdup (0 call); strerror (0 call); strlen (4 calls);
+ strncat (0 call); strncmp (0 call); strncpy (0 call); strndup (0 call);
+ strrchr (0 call); strstr (0 call); tolower (0 call); toupper (0 call);
+ wcscat (0 call); wcscpy (0 call); wcslen (2 calls); wcsncat (0 call);
+ wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
- Undefined functions (250)
+ Undefined functions (251)
=========================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_abort (1 call); Frama_C_char_interval (0 call);
@@ -195,21 +195,22 @@ tests/libc/fc_libc.c:148:[value] assertion got status valid.
fgets (0 call); fileno (0 call); fileno_unlocked (0 call);
flockfile (0 call); floor (0 call); floorf (0 call); fmod (0 call);
fopen (0 call); fputc (0 call); fputs (0 call); fread (0 call);
- freopen (0 call); fseek (0 call); fsetpos (0 call); ftell (0 call);
- ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call); getc (0 call);
- getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
- getenv (0 call); getitimer (0 call); getopt (0 call); getopt_long (0 call);
- getopt_long_only (0 call); getpriority (0 call); getrlimit (0 call);
- getrusage (0 call); gets (0 call); getsockopt (0 call);
- gettimeofday (0 call); getuid (0 call); gmtime (0 call); htonl (0 call);
- htons (0 call); iconv (0 call); iconv_close (0 call); iconv_open (0 call);
- inet_addr (0 call); inet_ntoa (0 call); inet_ntop (0 call);
- inet_pton (0 call); isascii (0 call); labs (0 call); ldiv (0 call);
- listen (0 call); llabs (0 call); lldiv (0 call); localtime (0 call);
- log (0 call); log10 (0 call); log10f (0 call); logf (0 call);
- longjmp (0 call); lrand48 (0 call); mblen (0 call); mbstowcs (0 call);
- mbtowc (0 call); memoverlap (1 call); mktime (0 call); nan (0 call);
- nanf (0 call); nanl (0 call); ntohl (0 call); ntohs (0 call); open (0 call);
+ free (0 call); freopen (0 call); fseek (0 call); fsetpos (0 call);
+ ftell (0 call); ftrylockfile (0 call); funlockfile (0 call);
+ fwrite (0 call); getc (0 call); getc_unlocked (0 call); getchar (0 call);
+ getchar_unlocked (0 call); getenv (0 call); getitimer (0 call);
+ getopt (0 call); getopt_long (0 call); getopt_long_only (0 call);
+ getpriority (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
+ getsockopt (0 call); gettimeofday (0 call); getuid (0 call);
+ gmtime (0 call); htonl (0 call); htons (0 call); iconv (0 call);
+ iconv_close (0 call); iconv_open (0 call); inet_addr (0 call);
+ inet_ntoa (0 call); inet_ntop (0 call); inet_pton (0 call);
+ isascii (0 call); labs (0 call); ldiv (0 call); listen (0 call);
+ llabs (0 call); lldiv (0 call); localtime (0 call); log (0 call);
+ log10 (0 call); log10f (0 call); logf (0 call); longjmp (0 call);
+ lrand48 (0 call); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+ memoverlap (1 call); mktime (0 call); nan (0 call); nanf (0 call);
+ nanl (0 call); ntohl (0 call); ntohs (0 call); open (0 call);
openat (0 call); opendir (0 call); openlog (0 call); perror (0 call);
poll (0 call); pow (0 call); powf (0 call); putc (0 call);
putc_unlocked (0 call); putchar (0 call); putchar_unlocked (0 call);
@@ -248,18 +249,18 @@ tests/libc/fc_libc.c:148:[value] assertion got status valid.
Global metrics
==============
- Sloc = 613
- Decision point = 120
+ Sloc = 610
+ Decision point = 119
Global variables = 33
- If = 118
+ If = 117
Loop = 31
Goto = 36
Assignment = 245
- Exit point = 65
+ Exit point = 64
Function = 315
- Function call = 31
+ Function call = 30
Pointer dereferencing = 87
- Cyclomatic complexity = 185
+ Cyclomatic complexity = 183
/* Generated by Frama-C */
#include "__fc_builtin.h"
#include "__fc_define_fd_set_t.h"
@@ -391,8 +392,6 @@ FILE __fc_initial_stderr =
{.__fc_FILE_id = (unsigned int)2, .__fc_FILE_data = 0U};
FILE __fc_initial_stdin =
{.__fc_FILE_id = (unsigned int)0, .__fc_FILE_data = 0U};
-extern void Frama_C_free(void *base);
-
/*@ assigns Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 1808f75bedd..11127a5e511 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -369,19 +369,6 @@ float Frama_C_float_interval(float min, float max);
double Frama_C_double_interval(double min, double max);
-/*@ assigns *((char *)dest + (0 .. n - 1)), \result;
- assigns *((char *)dest + (0 .. n - 1))
- \from *((char *)src + (0 .. n - 1));
- assigns \result \from dest;
- */
-extern void *Frama_C_memcpy(void *dest, void const *src, size_t n);
-
-/*@ assigns *((char *)p + (0 .. s - 1)), \result;
- assigns *((char *)p + (0 .. s - 1)) \from c;
- assigns \result \from p;
- */
-extern void *Frama_C_memset(void *p, int c, size_t s);
-
/*@ requires \false;
assigns \nothing; */
extern __attribute__((__noreturn__)) void Frama_C_abort(void);
@@ -2212,7 +2199,26 @@ void *calloc(size_t nmemb, size_t size);
void *malloc(size_t size);
-void free(void *p);
+/*@ requires freeable: p ≡ \null ∨ \freeable(p);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
+
+ behavior deallocation:
+ assumes p ≢ \null;
+ ensures \allocable(\old(p));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+
+ behavior no_deallocation:
+ assumes p ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_deallocation, deallocation;
+ disjoint behaviors no_deallocation, deallocation;
+ */
+extern void free(void *p);
/*@ requires ptr ≡ \null ∨ \freeable(ptr);
assigns __fc_heap_status, \result;
@@ -2411,6 +2417,115 @@ extern size_t mbstowcs(wchar_t *pwcs, char const *s, size_t n);
*/
extern size_t wcstombs(char *s, wchar_t const *pwcs, size_t n);
+int memcmp(void const *s1, void const *s2, size_t n);
+
+void *memchr(void const *s, int c, size_t n);
+
+void *memcpy(void *dest, void const *src, size_t n);
+
+void *memmove(void *dest, void const *src, size_t n);
+
+void *memset(void *s, int c, size_t n);
+
+size_t strlen(char const *s);
+
+/*@ requires valid_string_src: valid_read_nstring(s, n);
+ ensures \result ≡ strlen(\old(s)) ∨ \result ≡ \old(n);
+ assigns \result;
+ assigns \result \from *(s + (0 ..));
+ */
+extern size_t strnlen(char const *s, size_t n);
+
+int strcmp(char const *s1, char const *s2);
+
+int strncmp(char const *s1, char const *s2, size_t n);
+
+/*@ requires valid_string_s1: valid_read_string(s1);
+ requires valid_string_s2: valid_read_string(s2);
+ assigns \result;
+ assigns \result \from *(s1 + (0 ..)), *(s2 + (0 ..));
+ */
+extern int strcoll(char const *s1, char const *s2);
+
+char *strchr(char const *s, int c);
+
+char *strrchr(char const *s, int c);
+
+/*@ requires valid_string_src: valid_read_string(s);
+ requires valid_string_reject: valid_read_string(reject);
+ ensures 0 ≤ \result ≤ strlen(\old(s));
+ assigns \result;
+ assigns \result \from *(s + (0 ..)), *(reject + (0 ..));
+ */
+extern size_t strcspn(char const *s, char const *reject);
+
+/*@ requires valid_string_src: valid_read_string(s);
+ requires valid_string_accept: valid_read_string(accept);
+ ensures 0 ≤ \result ≤ strlen(\old(s));
+ assigns \result;
+ assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
+ */
+extern size_t strspn(char const *s, char const *accept);
+
+/*@ requires valid_string_src: valid_read_string(s);
+ requires valid_string_accept: valid_read_string(accept);
+ ensures
+ \result ≡ (char *)0 ∨ \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result \from s, *(s + (0 ..)), *(accept + (0 ..));
+ */
+extern char *strpbrk(char const *s, char const *accept);
+
+char *strstr(char const *haystack, char const *needle);
+
+/*@ requires valid_string_src: valid_string_or_null(s);
+ requires valid_string_delim: valid_read_string(delim);
+ ensures
+ \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result \from s, *(s + (0 ..)), *(delim + (0 ..));
+ */
+extern char *strtok(char *s, char const *delim);
+
+/*@ requires valid_string_src: \valid(stringp) ∧ valid_string(*stringp);
+ requires valid_string_delim: valid_read_string(delim);
+ assigns *stringp, \result;
+ assigns *stringp \from *(delim + (..)), *(*(stringp + (..)));
+ assigns \result \from *(delim + (..)), *(*(stringp + (..)));
+ */
+extern char *strsep(char **stringp, char const *delim);
+
+char *strerror(int errnum);
+
+char *strcpy(char *dest, char const *src);
+
+char *strncpy(char *dest, char const *src, size_t n);
+
+char *strcat(char *dest, char const *src);
+
+char *strncat(char *dest, char const *src, size_t n);
+
+/*@ requires valid_dest: \valid(dest + (0 .. n - 1));
+ requires valid_string_src: valid_read_string(src);
+ assigns *(dest + (0 .. n - 1)), \result;
+ assigns *(dest + (0 .. n - 1)) \from *(src + (0 ..)), n;
+ assigns \result \from dest;
+ */
+extern size_t strxfrm(char *dest, char const *src, size_t n);
+
+char *strdup(char const *s);
+
+char *strndup(char const *s, size_t n);
+
+/*@ requires \valid((char *)s + (0 .. n - 1));
+ ensures \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
+ assigns *((char *)s + (0 .. n - 1));
+ assigns *((char *)s + (0 .. n - 1)) \from \nothing;
+ */
+extern void bzero(void *s, size_t n);
+
+int strcasecmp(char const *s1, char const *s2);
+
/*@ requires abs_representable: i > -2147483647 - 1;
assigns \result;
assigns \result \from i;
@@ -2516,33 +2631,6 @@ void *malloc(size_t size)
return tmp;
}
-extern void Frama_C_free(void *base);
-
-/*@ requires freeable: p ≡ \null ∨ \freeable(p);
- assigns __fc_heap_status;
- assigns __fc_heap_status \from __fc_heap_status;
- frees p;
-
- behavior deallocation:
- assumes p ≢ \null;
- ensures \allocable(\old(p));
- assigns __fc_heap_status;
- assigns __fc_heap_status \from __fc_heap_status;
-
- behavior no_deallocation:
- assumes p ≡ \null;
- assigns \nothing;
- allocates \nothing;
-
- complete behaviors no_deallocation, deallocation;
- disjoint behaviors no_deallocation, deallocation;
- */
-void free(void *p)
-{
- if (p) Frama_C_free(p);
- return;
-}
-
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status
\from (indirect: nmemb), (indirect: size), __fc_heap_status;
@@ -2579,120 +2667,11 @@ void *calloc(size_t nmemb, size_t size)
goto return_label;
}
char *p = malloc(l);
- if (p) Frama_C_memset((void *)p,0,l);
+ if (p) memset((void *)p,0,l);
__retres = (void *)p;
return_label: return __retres;
}
-int memcmp(void const *s1, void const *s2, size_t n);
-
-void *memchr(void const *s, int c, size_t n);
-
-void *memcpy(void *dest, void const *src, size_t n);
-
-void *memmove(void *dest, void const *src, size_t n);
-
-void *memset(void *s, int c, size_t n);
-
-size_t strlen(char const *s);
-
-/*@ requires valid_string_src: valid_read_nstring(s, n);
- ensures \result ≡ strlen(\old(s)) ∨ \result ≡ \old(n);
- assigns \result;
- assigns \result \from *(s + (0 ..));
- */
-extern size_t strnlen(char const *s, size_t n);
-
-int strcmp(char const *s1, char const *s2);
-
-int strncmp(char const *s1, char const *s2, size_t n);
-
-/*@ requires valid_string_s1: valid_read_string(s1);
- requires valid_string_s2: valid_read_string(s2);
- assigns \result;
- assigns \result \from *(s1 + (0 ..)), *(s2 + (0 ..));
- */
-extern int strcoll(char const *s1, char const *s2);
-
-char *strchr(char const *s, int c);
-
-char *strrchr(char const *s, int c);
-
-/*@ requires valid_string_src: valid_read_string(s);
- requires valid_string_reject: valid_read_string(reject);
- ensures 0 ≤ \result ≤ strlen(\old(s));
- assigns \result;
- assigns \result \from *(s + (0 ..)), *(reject + (0 ..));
- */
-extern size_t strcspn(char const *s, char const *reject);
-
-/*@ requires valid_string_src: valid_read_string(s);
- requires valid_string_accept: valid_read_string(accept);
- ensures 0 ≤ \result ≤ strlen(\old(s));
- assigns \result;
- assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
- */
-extern size_t strspn(char const *s, char const *accept);
-
-/*@ requires valid_string_src: valid_read_string(s);
- requires valid_string_accept: valid_read_string(accept);
- ensures
- \result ≡ (char *)0 ∨ \base_addr(\result) ≡ \base_addr(\old(s));
- assigns \result;
- assigns \result \from s, *(s + (0 ..)), *(accept + (0 ..));
- */
-extern char *strpbrk(char const *s, char const *accept);
-
-char *strstr(char const *haystack, char const *needle);
-
-/*@ requires valid_string_src: valid_string_or_null(s);
- requires valid_string_delim: valid_read_string(delim);
- ensures
- \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
- assigns \result;
- assigns \result \from s, *(s + (0 ..)), *(delim + (0 ..));
- */
-extern char *strtok(char *s, char const *delim);
-
-/*@ requires valid_string_src: \valid(stringp) ∧ valid_string(*stringp);
- requires valid_string_delim: valid_read_string(delim);
- assigns *stringp, \result;
- assigns *stringp \from *(delim + (..)), *(*(stringp + (..)));
- assigns \result \from *(delim + (..)), *(*(stringp + (..)));
- */
-extern char *strsep(char **stringp, char const *delim);
-
-char *strerror(int errnum);
-
-char *strcpy(char *dest, char const *src);
-
-char *strncpy(char *dest, char const *src, size_t n);
-
-char *strcat(char *dest, char const *src);
-
-char *strncat(char *dest, char const *src, size_t n);
-
-/*@ requires valid_dest: \valid(dest + (0 .. n - 1));
- requires valid_string_src: valid_read_string(src);
- assigns *(dest + (0 .. n - 1)), \result;
- assigns *(dest + (0 .. n - 1)) \from *(src + (0 ..)), n;
- assigns \result \from dest;
- */
-extern size_t strxfrm(char *dest, char const *src, size_t n);
-
-char *strdup(char const *s);
-
-char *strndup(char const *s, size_t n);
-
-/*@ requires \valid((char *)s + (0 .. n - 1));
- ensures \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
- assigns *((char *)s + (0 .. n - 1));
- assigns *((char *)s + (0 .. n - 1)) \from \nothing;
- */
-extern void bzero(void *s, size_t n);
-
-int strcasecmp(char const *s1, char const *s2);
-
/*@ requires valid_dst: \valid((char *)dest + (0 .. n - 1));
requires valid_src: \valid_read((char *)src + (0 .. n - 1));
requires
diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle
index 0ed0f81f56a..272ad32b7b2 100644
--- a/tests/libc/oracle/stdlib_c.2.res.oracle
+++ b/tests/libc/oracle/stdlib_c.2.res.oracle
@@ -13,15 +13,20 @@
[value] computing for function calloc <- main.
Called from tests/libc/stdlib_c.c:14.
[value] computing for function malloc <- calloc <- main.
- Called from share/libc/stdlib.c:104.
+ Called from share/libc/stdlib.c:100.
share/libc/stdlib.c:84:[value] allocating variable __malloc_malloc_l84
share/libc/stdlib.c:84:[kernel] warning: Neither code nor specification for function Frama_C_malloc_by_stack, generating default assigns from the prototype
share/libc/stdlib.h:340:[value] warning: function malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-share/libc/stdlib.h:345:[value] function malloc, behavior no_allocation: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/libc/stdlib.h:345:[value] warning: function malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+share/libc/stdlib.h:345:[value] function malloc, behavior no_allocation: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] Recording results for malloc
[value] Done for function malloc
-share/libc/stdlib.c:105:[value] Call to builtin memset(({{ (void *)&__malloc_malloc_l84 }},{0},{4}))
+[value] computing for function memset <- calloc <- main.
+ Called from share/libc/stdlib.c:101.
+[value] using specification for function memset
+share/libc/stdlib.c:101:[value] function memset: precondition got status valid.
+share/libc/string.h:85:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
+[value] Done for function memset
share/libc/stdlib.h:319:[value] warning: function calloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
share/libc/stdlib.h:320:[value] warning: function calloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
share/libc/stdlib.h:321:[value] warning: function calloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
@@ -37,13 +42,14 @@ tests/libc/stdlib_c.c:20:[value] function Frama_C_size_t_interval: precondition
[value] computing for function calloc <- main.
Called from tests/libc/stdlib_c.c:21.
[value] computing for function malloc <- calloc <- main.
- Called from share/libc/stdlib.c:104.
+ Called from share/libc/stdlib.c:100.
share/libc/stdlib.c:84:[value] allocating variable __malloc_malloc_l84_0
[value] Recording results for malloc
[value] Done for function malloc
-share/libc/stdlib.c:105:[value] Call to builtin memset(({{ (void *)&__malloc_malloc_l84_0 }},{0},
- [0..4294967292],0%4))
-share/libc/stdlib.c:105:[value] warning: out of bounds write. assert \valid(p + (0 .. l - 1));
+[value] computing for function memset <- calloc <- main.
+ Called from share/libc/stdlib.c:101.
+share/libc/stdlib.c:101:[value] warning: function memset: precondition got status unknown.
+[value] Done for function memset
share/libc/stdlib.h:327:[value] function calloc, behavior no_allocation: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] Recording results for calloc
[value] Done for function calloc
@@ -58,61 +64,69 @@ tests/libc/stdlib_c.c:31:[value] entering loop for the first time
[value] computing for function calloc <- main.
Called from tests/libc/stdlib_c.c:32.
[value] computing for function malloc <- calloc <- main.
- Called from share/libc/stdlib.c:104.
+ Called from share/libc/stdlib.c:100.
share/libc/stdlib.c:84:[value] allocating variable __malloc_malloc_l84_1
[value] Recording results for malloc
[value] Done for function malloc
-share/libc/stdlib.c:105:[value] Call to builtin memset(({{ (void *)&__malloc_malloc_l84_1 }},{0},{4}))
+[value] computing for function memset <- calloc <- main.
+ Called from share/libc/stdlib.c:101.
+[value] Done for function memset
[value] Recording results for calloc
[value] Done for function calloc
[value] computing for function calloc <- main.
Called from tests/libc/stdlib_c.c:32.
[value] computing for function malloc <- calloc <- main.
- Called from share/libc/stdlib.c:104.
+ Called from share/libc/stdlib.c:100.
[value] Recording results for malloc
[value] Done for function malloc
-share/libc/stdlib.c:105:[value] Call to builtin memset(({{ (void *)&__malloc_w_malloc_l84_1 }},{0},{4; 8}))
+[value] computing for function memset <- calloc <- main.
+ Called from share/libc/stdlib.c:101.
+[value] Done for function memset
[value] Recording results for calloc
[value] Done for function calloc
tests/libc/stdlib_c.c:33:[value] warning: out of bounds write. assert \valid(s + (unsigned int)(i - 1));
[value] computing for function calloc <- main.
Called from tests/libc/stdlib_c.c:32.
[value] computing for function malloc <- calloc <- main.
- Called from share/libc/stdlib.c:104.
+ Called from share/libc/stdlib.c:100.
[value] Recording results for malloc
[value] Done for function malloc
-share/libc/stdlib.c:105:[value] Call to builtin memset(({{ (void *)&__malloc_w_malloc_l84_1 }},{0},
- {4; 8; 12}))
+[value] computing for function memset <- calloc <- main.
+ Called from share/libc/stdlib.c:101.
+[value] Done for function memset
[value] Recording results for calloc
[value] Done for function calloc
[value] computing for function calloc <- main.
Called from tests/libc/stdlib_c.c:32.
[value] computing for function malloc <- calloc <- main.
- Called from share/libc/stdlib.c:104.
+ Called from share/libc/stdlib.c:100.
[value] Recording results for malloc
[value] Done for function malloc
-share/libc/stdlib.c:105:[value] Call to builtin memset(({{ (void *)&__malloc_w_malloc_l84_1 }},{0},
- [0..4294967292],0%4))
+[value] computing for function memset <- calloc <- main.
+ Called from share/libc/stdlib.c:101.
+[value] Done for function memset
[value] Recording results for calloc
[value] Done for function calloc
[value] computing for function calloc <- main.
Called from tests/libc/stdlib_c.c:32.
[value] computing for function malloc <- calloc <- main.
- Called from share/libc/stdlib.c:104.
+ Called from share/libc/stdlib.c:100.
[value] Recording results for malloc
[value] Done for function malloc
-share/libc/stdlib.c:105:[value] Call to builtin memset(({{ (void *)&__malloc_w_malloc_l84_1 }},{0},
- [0..4294967292],0%4))
+[value] computing for function memset <- calloc <- main.
+ Called from share/libc/stdlib.c:101.
+[value] Done for function memset
[value] Recording results for calloc
[value] Done for function calloc
[value] computing for function calloc <- main.
Called from tests/libc/stdlib_c.c:32.
[value] computing for function malloc <- calloc <- main.
- Called from share/libc/stdlib.c:104.
+ Called from share/libc/stdlib.c:100.
[value] Recording results for malloc
[value] Done for function malloc
-share/libc/stdlib.c:105:[value] Call to builtin memset(({{ (void *)&__malloc_w_malloc_l84_1 }},{0},
- [0..4294967292],0%4))
+[value] computing for function memset <- calloc <- main.
+ Called from share/libc/stdlib.c:101.
+[value] Done for function memset
[value] Recording results for calloc
[value] Done for function calloc
[value] Recording results for main
@@ -129,13 +143,9 @@ share/libc/stdlib.c:105:[value] Call to builtin memset(({{ (void *)&__malloc_w_m
{{ NULL ; (void *)&__malloc_malloc_l84 ;
(void *)&__malloc_malloc_l84_0 ;
(void *)&__malloc_w_malloc_l84_1 }}
- __malloc_malloc_l84[0..3] ∈ {0} or UNINITIALIZED
- __malloc_malloc_l84_0[0..4294967291] ∈ {0} or UNINITIALIZED
- __malloc_w_malloc_l84_1[0]# ∈ {0; 42} or UNINITIALIZED%32, bits 0 to 7
- [1]# ∈ {0; 42} or UNINITIALIZED%32, bits 8 to 15
- [2]# ∈ {0; 42} or UNINITIALIZED%32, bits 16 to 23
- [bits 24 to 34359738335]# ∈
- {0; 42} or UNINITIALIZED repeated %32, bits 24 to 34359738335
+ __malloc_malloc_l84[0..3] ∈ [--..--] or UNINITIALIZED
+ __malloc_malloc_l84_0[0..4294967291] ∈ [--..--] or UNINITIALIZED
+ __malloc_w_malloc_l84_1[0..4294967291] ∈ [--..--] or UNINITIALIZED
[value:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
p ∈ {{ NULL ; (int *)&__malloc_malloc_l84 }}
@@ -143,10 +153,6 @@ share/libc/stdlib.c:105:[value] Call to builtin memset(({{ (void *)&__malloc_w_m
q ∈ {{ NULL ; (int *)&__malloc_malloc_l84_0 }}
r ∈ {0}
__retres ∈ {0}
- __malloc_malloc_l84[0..3] ∈ {0} or UNINITIALIZED
- __malloc_malloc_l84_0[0..4294967291] ∈ {0} or UNINITIALIZED
- __malloc_w_malloc_l84_1[0]# ∈ {0; 42} or UNINITIALIZED%32, bits 0 to 7
- [1]# ∈ {0; 42} or UNINITIALIZED%32, bits 8 to 15
- [2]# ∈ {0; 42} or UNINITIALIZED%32, bits 16 to 23
- [bits 24 to 34359738335]# ∈
- {0; 42} or UNINITIALIZED repeated %32, bits 24 to 34359738335
+ __malloc_malloc_l84[0..3] ∈ [--..--] or UNINITIALIZED
+ __malloc_malloc_l84_0[0..4294967291] ∈ [--..--] or UNINITIALIZED
+ __malloc_w_malloc_l84_1[0..4294967291] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index 6be6efd7967..bd2309b00fa 100644
--- a/tests/libc/oracle/string_c.res.oracle
+++ b/tests/libc/oracle/string_c.res.oracle
@@ -11,18 +11,51 @@
__fc_wctomb_state ∈ [--..--]
[value] computing for function test_memcpy <- main.
Called from tests/libc/string_c.c:264.
-tests/libc/string_c.c:10:[value] Call to builtin memcpy(({{ (void *)&dest }},{{ (void const *)&src }},{6}))
+[value] computing for function memcpy <- test_memcpy <- main.
+ Called from tests/libc/string_c.c:10.
+tests/libc/string_c.c:10:[value] function memcpy: precondition 'valid_dst' got status valid.
+tests/libc/string_c.c:10:[value] function memcpy: precondition 'valid_src' got status valid.
+tests/libc/string_c.c:10:[value] function memcpy: precondition got status valid.
+share/libc/string.h:65:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
+share/libc/string.h:65:[value] warning: function memcpy: postcondition got status unknown.
+share/libc/string.h:66:[value] function memcpy: postcondition got status valid.
+[value] Recording results for memcpy
+[value] Done for function memcpy
tests/libc/string_c.c:11:[value] assertion got status valid.
tests/libc/string_c.c:12:[value] assertion got status valid.
tests/libc/string_c.c:13:[value] assertion got status valid.
tests/libc/string_c.c:14:[value] assertion got status valid.
-tests/libc/string_c.c:16:[value] Call to builtin memcpy(({{ (void *)&dest }},{{ (void const *)&src2 }},{5}))
+[value] computing for function memcpy <- test_memcpy <- main.
+ Called from tests/libc/string_c.c:16.
+tests/libc/string_c.c:16:[value] function memcpy: precondition 'valid_dst' got status valid.
+tests/libc/string_c.c:16:[value] function memcpy: precondition 'valid_src' got status valid.
+tests/libc/string_c.c:16:[value] function memcpy: precondition got status valid.
+[value] Recording results for memcpy
+[value] Done for function memcpy
tests/libc/string_c.c:17:[value] assertion got status valid.
tests/libc/string_c.c:18:[value] assertion got status valid.
-tests/libc/string_c.c:19:[value] Call to builtin memcpy(({{ (void *)&dest }},{0},{0}))
-tests/libc/string_c.c:20:[value] Call to builtin memcpy(({0},{0},{0}))
+[value] computing for function memcpy <- test_memcpy <- main.
+ Called from tests/libc/string_c.c:19.
+tests/libc/string_c.c:19:[value] function memcpy: precondition 'valid_dst' got status valid.
+tests/libc/string_c.c:19:[value] function memcpy: precondition 'valid_src' got status valid.
+tests/libc/string_c.c:19:[value] function memcpy: precondition got status valid.
+[value] Recording results for memcpy
+[value] Done for function memcpy
+[value] computing for function memcpy <- test_memcpy <- main.
+ Called from tests/libc/string_c.c:20.
+tests/libc/string_c.c:20:[value] function memcpy: precondition 'valid_dst' got status valid.
+tests/libc/string_c.c:20:[value] function memcpy: precondition 'valid_src' got status valid.
+tests/libc/string_c.c:20:[value] function memcpy: precondition got status valid.
+[value] Recording results for memcpy
+[value] Done for function memcpy
tests/libc/string_c.c:21:[value] assertion got status valid.
-tests/libc/string_c.c:23:[value] Call to builtin memcpy(({{ (void *)&dest }},{{ (void const *)&x }},{4}))
+[value] computing for function memcpy <- test_memcpy <- main.
+ Called from tests/libc/string_c.c:23.
+tests/libc/string_c.c:23:[value] function memcpy: precondition 'valid_dst' got status valid.
+tests/libc/string_c.c:23:[value] function memcpy: precondition 'valid_src' got status valid.
+tests/libc/string_c.c:23:[value] function memcpy: precondition got status valid.
+[value] Recording results for memcpy
+[value] Done for function memcpy
tests/libc/string_c.c:24:[value] assertion got status valid.
tests/libc/string_c.c:25:[value] assertion got status valid.
[value] Recording results for test_memcpy
@@ -656,6 +689,15 @@ tests/libc/string_c.c:259:[value] assertion got status valid.
p1 ∈ {{ "hallo" ; "hallo" ; "a\000b" ; "a\000b" }}
p2 ∈ {{ (unsigned char const *)&hello ; "a\000c" ; "a\000c" }}
__retres ∈ {-4; -1; 0}
+[value:final-states] Values at end of function memcpy:
+ res ∈ {{ NULL ; &dest[0] }}
+ dest[0] ∈ {65; 97; 104}
+ [1] ∈ {0; 56; 101}
+ [2] ∈ {9; 98; 108}
+ [3] ∈ {0; 18; 108}
+ [4] ∈ {0; 111}
+ [5] ∈ {0}
+ __retres ∈ {{ NULL ; (void *)&dest }}
[value:final-states] Values at end of function memmove:
s ∈ {{ &buf{[0], [2]} }}
d ∈ {{ &buf{[0], [2], [3]} }}
@@ -738,7 +780,10 @@ tests/libc/string_c.c:259:[value] assertion got status valid.
res3 ∈ {0}
res4 ∈ {-1}
[value:final-states] Values at end of function test_memcpy:
- dest[bits 0 to 31] ∈ {302594113}
+ dest[0] ∈ {65}
+ [1] ∈ {56}
+ [2] ∈ {9}
+ [3] ∈ {18}
[4..5] ∈ {0}
src[0] ∈ {104}
[1] ∈ {101}
diff --git a/tests/libc/string_c.c b/tests/libc/string_c.c
index 83bc233d754..4ad8948216b 100644
--- a/tests/libc/string_c.c
+++ b/tests/libc/string_c.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-no-val-builtins-auto -slevel 1000 -val-builtin memcpy:Frama_C_memcpy"
+ STDOPT: #"-no-val-builtins-auto -slevel 1000"
*/ // slevel is used to unroll loops
#include "string.c"
diff --git a/tests/libc/string_c_strchr.c b/tests/libc/string_c_strchr.c
index 9384567294f..8b00949275f 100644
--- a/tests/libc/string_c_strchr.c
+++ b/tests/libc/string_c_strchr.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-cpp-extra-args=-includeshare/libc/string.c -slevel-function strchr:256,main:256 -val-builtin memcpy:Frama_C_memcpy -val-slevel-merge-after-loop main -no-val-builtins-auto"
+ STDOPT: #"-cpp-extra-args=-includeshare/libc/string.c -slevel-function strchr:256,main:256 -val-slevel-merge-after-loop main -no-val-builtins-auto"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
diff --git a/tests/non-free/alloc_weak.c b/tests/non-free/alloc_weak.c
index 090cdc0309c..42cd64cdac3 100644
--- a/tests/non-free/alloc_weak.c
+++ b/tests/non-free/alloc_weak.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-val-builtin memcpy:Frama_C_memcpy,malloc:Frama_C_malloc_by_stack"
+ STDOPT: #""
*/
#include <stdlib.h>
diff --git a/tests/non-free/fam.i b/tests/non-free/fam.c
similarity index 83%
rename from tests/non-free/fam.i
rename to tests/non-free/fam.c
index ad61b3dcbb5..bd928c9b097 100644
--- a/tests/non-free/fam.i
+++ b/tests/non-free/fam.c
@@ -1,3 +1,5 @@
+#include "string.h"
+
typedef unsigned char uint8_t ;
typedef struct {
uint8_t length;
@@ -11,5 +13,5 @@ void main (void) {
TcpOption * option = buf + 10;
option->length = 5;
Frama_C_show_each(option->value);
- Frama_C_memcpy(option->value, value, 2);
+ memcpy(option->value, value, 2);
}
diff --git a/tests/non-free/free.c b/tests/non-free/free.c
new file mode 100644
index 00000000000..13a1c8e783d
--- /dev/null
+++ b/tests/non-free/free.c
@@ -0,0 +1,46 @@
+/* run.config*
+ STDOPT: #" -val-builtin malloc:Frama_C_malloc_fresh"
+*/
+#include "stdlib.h"
+volatile v;
+
+void main1() {
+ int *p = malloc(40);
+ p[1] = 1;
+ int *q = malloc(40);
+ q[2] = 2;
+ int *r = v ? p : q;
+ Frama_C_dump_each();
+ free(r);
+
+ int *u = malloc(40);
+ u[3] = 3;
+ free(u);
+
+ int* t = 0;
+ free(t);
+
+ int* s = malloc(40);
+ s[4] = 4;
+ s = v ? 0 : s;
+ free(s);
+}
+
+
+
+void main2() {
+ int *p;
+ int i = 1;
+
+ p = malloc(i * sizeof (int));
+ if (p != 0) {
+ *p = i;
+ }
+ free(p); /* we must not backward-propagate information about p
+ before and after the call, because it became dangling. */
+}
+
+void main() {
+ if (v) main1 ();
+ else if (v) main2();
+}
diff --git a/tests/non-free/free.i b/tests/non-free/free.i
deleted file mode 100644
index 0dea07aeacc..00000000000
--- a/tests/non-free/free.i
+++ /dev/null
@@ -1,46 +0,0 @@
-void Frama_C_free(void*);
-void* Frama_C_malloc_fresh(unsigned long);
-volatile v;
-
-void main1() {
- int *p = Frama_C_malloc_fresh(40);
- p[1] = 1;
- int *q = Frama_C_malloc_fresh(40);
- q[2] = 2;
- int *r = v ? p : q;
- Frama_C_dump_each();
- Frama_C_free(r);
-
- int *u = Frama_C_malloc_fresh(40);
- u[3] = 3;
- Frama_C_free(u);
-
- int* t = 0;
- Frama_C_free(t);
-
- int* s = Frama_C_malloc_fresh(40);
- s[4] = 4;
- s = v ? 0 : s;
- Frama_C_free(s);
-}
-
-
-
-
-
-void main2() {
- int *p;
- int i = 1;
-
- p = Frama_C_malloc_fresh(i * sizeof (int));
- if (p != 0) {
- *p = i;
- }
- Frama_C_free(p); /* we must not backward-propagate information about p
- before and after the call, because it became dangling. */
-}
-
-void main() {
- if (v) main1 ();
- else if (v) main2();
-}
diff --git a/tests/non-free/gcc_zero_length_array.c b/tests/non-free/gcc_zero_length_array.c
index c11dc83e7e5..5995a8b7630 100644
--- a/tests/non-free/gcc_zero_length_array.c
+++ b/tests/non-free/gcc_zero_length_array.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-machdep gcc_x86_32 -val-builtin malloc:Frama_C_malloc_fresh,free:Frama_C_free -slevel 11"
+ STDOPT: +"-machdep gcc_x86_32 -val-builtin malloc:Frama_C_malloc_fresh -slevel 11"
*/
#include <stdlib.h>
diff --git a/tests/non-free/imprecise-malloc-free.c b/tests/non-free/imprecise-malloc-free.c
new file mode 100644
index 00000000000..24b4a763744
--- /dev/null
+++ b/tests/non-free/imprecise-malloc-free.c
@@ -0,0 +1,27 @@
+/* run.config*
+ STDOPT: #" -val-mlevel 0 -no-val-malloc-returns-null"
+*/
+
+extern int i;
+
+#include "stdlib.h"
+
+
+void main() {
+ int size1, size2;
+ size1 = &size1 + i;
+ size2 = i + ((int)&size2 >> 1);
+ int *p = malloc((unsigned long)&i+(int)&i);
+ int *q = malloc(size1);
+ int *r = malloc(size2);
+
+ Frama_C_show_each(p, q, r);
+ Frama_C_show_each(p+(int)p);
+
+ *p = p+1;
+ *q = q+2;
+ *r = r+3;
+
+ free(p+(int)p);
+ free(q+(int)r);
+}
diff --git a/tests/non-free/imprecise-malloc-free.i b/tests/non-free/imprecise-malloc-free.i
deleted file mode 100644
index 9e84a2190bd..00000000000
--- a/tests/non-free/imprecise-malloc-free.i
+++ /dev/null
@@ -1,27 +0,0 @@
-/* run.config*
- STDOPT: #" -val-mlevel 0"
-*/
-
-extern int i;
-
-//@ ensures \result != \null;
-void* Frama_C_malloc_by_stack(unsigned long);
-
-void main() {
- int size1, size2;
- size1 = &size1 + i;
- size2 = i + ((int)&size2 >> 1);
- int *p = Frama_C_malloc_by_stack((unsigned long)&i+(int)&i);
- int *q = Frama_C_malloc_by_stack(size1);
- int *r = Frama_C_malloc_by_stack(size2);
-
- Frama_C_show_each(p, q, r);
- Frama_C_show_each(p+(int)p);
-
- *p = p+1;
- *q = q+2;
- *r = r+3;
-
- Frama_C_free(p+(int)p);
- Frama_C_free(q+(int)r);
-}
diff --git a/tests/non-free/imprecise.c b/tests/non-free/imprecise.c
index 06283171cb9..22371b22804 100644
--- a/tests/non-free/imprecise.c
+++ b/tests/non-free/imprecise.c
@@ -1,8 +1,8 @@
/* run.config*
STDOPT: +" -val-warn-copy-indeterminate=-cast_address -val -out -input -deps -calldeps -value-msg-key initial-state -absolute-valid-range 100-200 -inout -then -lib-entry"
*/
+#include "string.h"
struct s;
-
//@ assigns *p \from \nothing;
void f(struct s *p);
@@ -28,8 +28,8 @@ struct s v1, v2;
struct u v3, v5;
struct s* t[10];
-//@ assigns ((char*) p)[0..size-1] \from c; assigns \result \from p;
-void* Frama_C_memset(void *p, int c, unsigned long size);
+
+
void abstract_structs() {
char *p = &v1;
@@ -48,7 +48,7 @@ void abstract_structs() {
v1 = v2;
}
v2 = v1;
- Frama_C_memset(&v3, -5, sizeof(v3));
+ memset(&v3, -5, sizeof(v3));
int *p2 = ((int*)&v2)+1;
*p2 = &addr;
*t[5] = v2;
@@ -129,7 +129,7 @@ void paste_big () {
unsigned int i = v;
struct s_big s;
- Frama_C_memset(&s, 2, sizeof(s));
+ memset(&s, 2, sizeof(s));
struct s_big t_big[300];
//@ assert i < 300;
diff --git a/tests/non-free/memchr.c b/tests/non-free/memchr.c
index c62d696e831..b675d880fb5 100644
--- a/tests/non-free/memchr.c
+++ b/tests/non-free/memchr.c
@@ -1,4 +1,5 @@
#include "__fc_builtin.h"
+#include "string.h"
// NOTE: all unnamed assertions should be valid.
// Imprecise results should be defined using named
@@ -11,9 +12,8 @@
static volatile int nondet;
#define assert_bottom(exp,id) if (nondet) { exp; Frama_C_show_each_unreachable_ ## id(); }
-#define memchr Frama_C_memchr
-//@ assigns \result \from ((char*)s)[0..], c, n;
-void *Frama_C_memchr(const void *s, int c, size_t n);
+
+
// Definitions for C++ oracle checking
typedef int Ival;
@@ -158,7 +158,7 @@ void memchr_bitfields() {
s.c = 7;
CHAR_PTR(p);
p = &s;
- assert_bottom(Frama_C_memchr(p, c, 3),bitfields);
+ assert_bottom(memchr(p, c, 3),bitfields);
}
typedef struct {
@@ -181,7 +181,7 @@ void memchr_bitfields2() {
void init_array_nondet(char *a, int from, int to, int val1, int val2) {
int val = NONDET(val1, val2);
- Frama_C_memset(a + from, val, to-from+1);
+ memset(a + from, val, to-from+1);
from = to = val1 = val2 = -1; // reset to minimize oracle changes
}
diff --git a/tests/non-free/memcpy.c b/tests/non-free/memcpy.c
index a31ddae8d0b..80a507e9185 100644
--- a/tests/non-free/memcpy.c
+++ b/tests/non-free/memcpy.c
@@ -1,7 +1,7 @@
/* run.config*
STDOPT: +"-calldeps -slevel-function init:2000 -value-msg-key imprecision -plevel 150 -main main_all -inout -no-deps -absolute-valid-range 100000-100001 -then -load-module report -report"
*/
-#include "__fc_builtin.h"
+#include "string.h"
extern unsigned int i;
char src[20];
@@ -25,7 +25,7 @@ volatile maybe;
void buggy () {
char c;
char *p = maybe ? &c: "abc";
- Frama_C_memcpy(p,"d",1);
+ memcpy(p,"d",1);
}
int tm[1000];
@@ -44,13 +44,13 @@ void many() {
//@ assert p < 1000;
tm[0]=0;
- Frama_C_memcpy(&tm[p],s,4);
+ memcpy(&tm[p],s,4);
um[0]=0;
- Frama_C_memcpy(&um[p],s,2);
+ memcpy(&um[p],s,2);
typ ty = {1, 2};
ttyp[0] = ty;
- Frama_C_memcpy(&ttyp[p],&ty,sizeof(typ));
+ memcpy(&ttyp[p],&ty,sizeof(typ));
}
struct t1 { int x; int y; int* p; char padding[24];} v1,v2, v3, v4, v5;
@@ -65,14 +65,14 @@ void main (int a, int b){
init ();
//@ assert 5 <= b && b <= 15;
- Frama_C_memcpy(dst1+1, src+2, b);
+ memcpy(dst1+1, src+2, b);
- Frama_C_memcpy(dst2+1, src+2, 2*b);
+ memcpy(dst2+1, src+2, 2*b);
//@ assert 5 <= b && b <= 14;
- Frama_C_memcpy(dst3+5, src+2, b);
+ memcpy(dst3+5, src+2, b);
- Frama_C_memcpy(dst4+5, src+2, 2*b);
+ memcpy(dst4+5, src+2, 2*b);
v2 = v2;
v2.p = &v1.y;
@@ -80,29 +80,29 @@ void main (int a, int b){
v1.x = 5;
v1.y = 7;
- Frama_C_memcpy(&v2, &v1, sizeof(v1));
+ memcpy(&v2, &v1, sizeof(v1));
- Frama_C_memcpy(t+2, t, (1+!a)*sizeof(v1));
+ memcpy(t+2, t, (1+!a)*sizeof(v1));
- Frama_C_memcpy(&v3, t+(int)t, sizeof(v1));
+ memcpy(&v3, t+(int)t, sizeof(v1));
- Frama_C_memcpy(&v4 + (int)&v4, &v1, sizeof(v1)-20);
+ memcpy(&v4 + (int)&v4, &v1, sizeof(v1)-20);
v4.y = &t[0];
- Frama_C_memcpy(&v5 + (int)&v5, &v4, sizeof(v4)-20);
+ memcpy(&v5 + (int)&v5, &v4, sizeof(v4)-20);
if (maybe) {
int x=1;
while(1)
- Frama_C_memcpy((void *)&x, (void const*)&x, i);
+ memcpy((void *)&x, (void const*)&x, i);
}
char *p;
p = maybe ? &dst5[0] : &dst5[20];
- Frama_C_memcpy(p, &src[0], b);
+ memcpy(p, &src[0], b);
b = maybe;
//@ assert 1 <= b < 20;
p = maybe ? &dst5[40] : &dst5[70];
- Frama_C_memcpy(p, &src[0], b);
+ memcpy(p, &src[0], b);
// Destination pointer is unbounded
char ptop1[800];
@@ -111,7 +111,7 @@ void main (int a, int b){
pptop++;
if (maybe) break;
}
- Frama_C_memcpy(pptop, src, 4);
+ memcpy(pptop, src, 4);
char ptop2[800];
pptop = &ptop2[750];
@@ -119,7 +119,7 @@ void main (int a, int b){
pptop--;
if (maybe) break;
}
- Frama_C_memcpy(pptop, src+1, 4);
+ memcpy(pptop, src+1, 4);
char ptop3[800];
pptop = &ptop3[2];
@@ -128,7 +128,7 @@ void main (int a, int b){
if (maybe) pptop++;
if (maybe) break;
}
- Frama_C_memcpy(pptop, src+2, 4);
+ memcpy(pptop, src+2, 4);
char ptop4[800];
pptop = &ptop4[2];
@@ -137,20 +137,20 @@ void main (int a, int b){
if (maybe) pptop++;
if (maybe) break;
}
- Frama_C_memcpy(pptop, src+2, 5);
+ memcpy(pptop, src+2, 5);
// Size is a garbled mix
char garbledsize[100];
int* pgarbledsize = &garbledsize[10];
- Frama_C_memcpy(pgarbledsize, src, (unsigned int)garbledsize);
+ memcpy(pgarbledsize, src, (unsigned int)garbledsize);
// Sure size may be zero
char dstmaybesize1[15], dstmaybesize2[150];
int maybesize = maybe;
//@ assert 0 <= maybesize <= 22; // >= plevel / 10
- Frama_C_memcpy(dstmaybesize1, src, maybesize);
+ memcpy(dstmaybesize1, src, maybesize);
//@ assert 0 <= maybesize <= 6;
- Frama_C_memcpy(dstmaybesize2, src, maybesize);
+ memcpy(dstmaybesize2, src, maybesize);
}
@@ -169,25 +169,25 @@ void main_uninit () {
unsigned char b[50];
int r = 0;
if (maybe) {
- Frama_C_memcpy(b, a, 10);
+ memcpy(b, a, 10);
//@ assert !\initialized(&b[8]);
- Frama_C_memcpy(b, a, itv(0,25));
+ memcpy(b, a, itv(0,25));
//@ assert !\initialized(&b[11]);
}
else if (maybe) {
make_unknown(a, 10);
- Frama_C_memcpy(b, a, 10);
+ memcpy(b, a, 10);
//@ assert \initialized(&b[8]);
- Frama_C_memcpy(b, a, itv(0,25));
+ memcpy(b, a, itv(0,25));
r += b[11]; // initialisation unknown
}
else if (maybe) {
make_unknown(b, 10);
if (maybe) {
- Frama_C_memcpy(b, a, 10); // de-initialize b
+ memcpy(b, a, 10); // de-initialize b
//@ assert !\initialized(&b[8]);
} else {
- Frama_C_memcpy(b, a, itv(0,25)); // copy completely uninitialized in an unsure way
+ memcpy(b, a, itv(0,25)); // copy completely uninitialized in an unsure way
//@ assert !\initialized(&b[11]); // already NOT initialized
r += b[8]; // initialisation unknown
}
@@ -195,9 +195,9 @@ void main_uninit () {
else if (maybe) {
make_unknown(a, 10);
make_unknown(b, 10);
- Frama_C_memcpy(b, a, 10);
+ memcpy(b, a, 10);
//@ assert \initialized(&b[8]);
- Frama_C_memcpy(b, a, itv(0,25));
+ memcpy(b, a, itv(0,25));
r += b[11]; // initialisation unknown
}
}
@@ -206,7 +206,7 @@ void main_local() {
int* p, *q;
{ int y;
q = &y;
- Frama_C_memcpy(&p, &q, sizeof(int *));
+ memcpy(&p, &q, sizeof(int *));
q = 0;
}
Frama_C_dump_each();
@@ -217,8 +217,8 @@ void copy_0() {
locations. But there used to be a bug with the NULL base when
-absolute-valid-range is set. */
int l;
- Frama_C_memcpy(0, &l, 0);
- Frama_C_memcpy(&l, 0, 0);
+ memcpy(0, &l, 0);
+ memcpy(&l, 0, 0);
}
diff --git a/tests/non-free/memcpy2.c b/tests/non-free/memcpy2.c
index 71d3310c2e4..f491d2dba5b 100644
--- a/tests/non-free/memcpy2.c
+++ b/tests/non-free/memcpy2.c
@@ -1,5 +1,5 @@
-#include "share/libc/__fc_builtin.h"
-
+#include "__fc_builtin.h"
+#include "string.h"
int main(int c, char **v)
{
char t[512];
@@ -7,13 +7,13 @@ int main(int c, char **v)
int l;
l = Frama_C_interval(0,511);
- Frama_C_memcpy(t, s, l);
+ memcpy(t, s, l);
Frama_C_dump_each();
l = Frama_C_interval(0,512);
- Frama_C_memcpy(t, s, l);
+ memcpy(t, s, l);
l = Frama_C_interval(1,512);
- Frama_C_memcpy(t, s, l);
+ memcpy(t, s, l);
}
diff --git a/tests/non-free/memcpy_invalid.i b/tests/non-free/memcpy_invalid.c
similarity index 62%
rename from tests/non-free/memcpy_invalid.i
rename to tests/non-free/memcpy_invalid.c
index c8c9115d189..1d648591b49 100644
--- a/tests/non-free/memcpy_invalid.i
+++ b/tests/non-free/memcpy_invalid.c
@@ -1,14 +1,14 @@
/* run.config*
- OPT: -val @VALUECONFIG@ -journal-disable -val-builtin=memcpy:Frama_C_memcpy -calldeps
+ OPT: -val @VALUECONFIG@ -journal-disable -calldeps
*/
/*@ assigns \result \from min, max;
@ ensures min <= \result <= max;
*/
extern int Frama_C_interval(int min, int max);
-/*@ assigns ((char *)dst)[0 .. n - 1]
- \from ((char *)src)[0 .. n - 1]; */
-extern void *memcpy(void *dst, const void *src, unsigned long n);
+
+#include "string.h"
+
static void test(int max)
{
diff --git a/tests/non-free/memset.c b/tests/non-free/memset.c
new file mode 100644
index 00000000000..e1164acd60e
--- /dev/null
+++ b/tests/non-free/memset.c
@@ -0,0 +1,73 @@
+/* run.config*
+ STDOPT: #"-calldeps -value-msg-key imprecision -plevel 500" +"-inout -no-deps"
+*/
+
+#include "string.h"
+
+
+int t1[100];
+int t2[100];
+int t3[100];
+int t4[100];
+int t5[100];
+int t6[100];
+int t7[100];
+int t8[100];
+int t9[100];
+int t10[100];
+int t11[100];
+int t12[100];
+
+struct s {
+ char f1;
+ short f2;
+ int f3;
+ int f4[3];
+};
+
+struct s ts[5];
+
+volatile int vol;
+
+void main() {
+ void * dst = memset(t1, 0x11, sizeof(t1)); // basic
+ memset(t2+(int)t2, 0x12, sizeof(t2)); // garbled dest
+ memset(t3+10, 0x11, (unsigned long)t1); // garbled size
+
+ if (vol) {
+ memset(t4+1, 1, sizeof(t4)); // out of bounds
+ }
+
+ memset(t5, (int)t1, sizeof(t4)); // garbled char
+
+ int *p = vol ? t6+10 : t7;
+ memset(p, 0x22, 16); // multiple dest
+
+ p = vol ? (char*) 0 : t8;
+ memset(p, 0x22, 16); // one valid dest; TODO
+
+ p = t9+20;
+ while (1) {
+ if (vol) break;
+ p++;
+ }
+ memset(p, 0x8FE, 4); // imprecise dest
+
+ unsigned long s = 12;
+ if (vol) s += 24;
+ memset(t10+4, 0x88, s); // imprecise size
+
+ unsigned long s1 = 8;
+ if (vol) s1 += 8;
+ p = t11 + 2;
+ if (vol)
+ p++;
+ memset(p, 0x99, s1); // imprecise dest+size with juxtaposition
+
+ if (vol)
+ memset(ts, 254, sizeof(ts));
+
+ unsigned k = vol;
+ //@ assert Assume: k <= 12;
+ memset(t12+k*8, 1, 4); // Imprecise, because of double congruences
+}
diff --git a/tests/non-free/memset.i b/tests/non-free/memset.i
deleted file mode 100644
index eba8f318462..00000000000
--- a/tests/non-free/memset.i
+++ /dev/null
@@ -1,73 +0,0 @@
-/* run.config*
- STDOPT: #"-calldeps -value-msg-key imprecision -plevel 500" +"-inout -no-deps"
-*/
-
-//@ assigns *((char*)dst+(0..size-1)) \from v; assigns \result \from dst;
-void* Frama_C_memset(void * dst, int v, unsigned long size);
-
-int t1[100];
-int t2[100];
-int t3[100];
-int t4[100];
-int t5[100];
-int t6[100];
-int t7[100];
-int t8[100];
-int t9[100];
-int t10[100];
-int t11[100];
-int t12[100];
-
-struct s {
- char f1;
- short f2;
- int f3;
- int f4[3];
-};
-
-struct s ts[5];
-
-volatile int vol;
-
-void main() {
- void * dst = Frama_C_memset(t1, 0x11, sizeof(t1)); // basic
- Frama_C_memset(t2+(int)t2, 0x12, sizeof(t2)); // garbled dest
- Frama_C_memset(t3+10, 0x11, (unsigned long)t1); // garbled size
-
- if (vol) {
- Frama_C_memset(t4+1, 1, sizeof(t4)); // out of bounds
- }
-
- Frama_C_memset(t5, (int)t1, sizeof(t4)); // garbled char
-
- int *p = vol ? t6+10 : t7;
- Frama_C_memset(p, 0x22, 16); // multiple dest
-
- p = vol ? (char*) 0 : t8;
- Frama_C_memset(p, 0x22, 16); // one valid dest; TODO
-
- p = t9+20;
- while (1) {
- if (vol) break;
- p++;
- }
- Frama_C_memset(p, 0x8FE, 4); // imprecise dest
-
- unsigned long s = 12;
- if (vol) s += 24;
- Frama_C_memset(t10+4, 0x88, s); // imprecise size
-
- unsigned long s1 = 8;
- if (vol) s1 += 8;
- p = t11 + 2;
- if (vol)
- p++;
- Frama_C_memset(p, 0x99, s1); // imprecise dest+size with juxtaposition
-
- if (vol)
- Frama_C_memset(ts, 254, sizeof(ts));
-
- unsigned k = vol;
- //@ assert Assume: k <= 12;
- Frama_C_memset(t12+k*8, 1, 4); // Imprecise, because of double congruences
-}
diff --git a/tests/non-free/oracle/fam.res.oracle b/tests/non-free/oracle/fam.res.oracle
index 4ed53625dcd..07a8b4a2021 100644
--- a/tests/non-free/oracle/fam.res.oracle
+++ b/tests/non-free/oracle/fam.res.oracle
@@ -1,12 +1,12 @@
-[kernel] Parsing tests/non-free/fam.i (no preprocessing)
-tests/non-free/fam.i:14:[kernel] warning: Calling undeclared function Frama_C_memcpy. Old style K&R code?
+[kernel] Parsing tests/non-free/fam.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
-tests/non-free/fam.i:13:[value] Frama_C_show_each: {{ &buf + {11} }}
-tests/non-free/fam.i:14:[value] Call to builtin memcpy(({{ &buf[11] }},{{ &value[0] }},{2}))
+tests/non-free/fam.c:15:[value] Frama_C_show_each: {{ &buf + {11} }}
+tests/non-free/fam.c:16:[value] Call to builtin memcpy(({{ (void *)&buf[11] }},{{ (void const *)&value }},
+ {2}))
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
@@ -21,16 +21,14 @@ tests/non-free/fam.i:14:[value] Call to builtin memcpy(({{ &buf[11] }},{{ &value
[1] ∈ {20}
option ∈ {{ (TcpOption *)&buf[10] }}
[from] Computing for function main
-[from] Computing for function Frama_C_memcpy <-main
-tests/non-free/fam.i:14:[kernel] warning: Neither code nor specification for function Frama_C_memcpy, generating default assigns from the prototype
-[from] Done for function Frama_C_memcpy
+[from] Computing for function memcpy <-main
+[from] Done for function memcpy
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_memcpy:
- buf[11..99] FROM buf[11..99]; value[0..1]; x_2 (and SELF)
- value[0..1] FROM buf[11..99]; value[0..1]; x_2 (and SELF)
- \result FROM buf[11..99]; value[0..1]; x_2
+[from] Function memcpy:
+ buf[11..12] FROM value[0..1]
+ \result FROM dest
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
diff --git a/tests/non-free/oracle/free.res.oracle b/tests/non-free/oracle/free.res.oracle
index 7bd24fc4d70..57733e91056 100644
--- a/tests/non-free/oracle/free.res.oracle
+++ b/tests/non-free/oracle/free.res.oracle
@@ -1,80 +1,93 @@
-[kernel] Parsing tests/non-free/free.i (no preprocessing)
+[kernel] Parsing tests/non-free/free.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
v ∈ [--..--]
[value] computing for function main1 <- main.
- Called from tests/non-free/free.i:44.
-tests/non-free/free.i:6:[value] allocating variable __malloc_main1_l6
-tests/non-free/free.i:6:[kernel] warning: Neither code nor specification for function Frama_C_malloc_fresh, generating default assigns from the prototype
-tests/non-free/free.i:8:[value] allocating variable __malloc_main1_l8
-tests/non-free/free.i:11:[value] Frama_C_dump_each:
+ Called from tests/non-free/free.c:44.
+tests/non-free/free.c:8:[value] allocating variable __malloc_main1_l8
+tests/non-free/free.c:10:[value] allocating variable __malloc_main1_l10
+tests/non-free/free.c:13:[value] Frama_C_dump_each:
# Cvalue domain:
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
v ∈ [--..--]
- p ∈ {{ &__malloc_main1_l6[0] }}
- q ∈ {{ &__malloc_main1_l8[0] }}
- r ∈ {{ &__malloc_main1_l6[0] ; &__malloc_main1_l8[0] }}
- tmp_1 ∈ {{ &__malloc_main1_l6[0] ; &__malloc_main1_l8[0] }}
- __malloc_main1_l6[0] ∈ UNINITIALIZED
+ p ∈ {{ &__malloc_main1_l8[0] }}
+ q ∈ {{ &__malloc_main1_l10[0] }}
+ r ∈ {{ &__malloc_main1_l8[0] ; &__malloc_main1_l10[0] }}
+ tmp_1 ∈ {{ &__malloc_main1_l8[0] ; &__malloc_main1_l10[0] }}
+ __malloc_main1_l8[0] ∈ UNINITIALIZED
[1] ∈ {1}
[2..9] ∈ UNINITIALIZED
- __malloc_main1_l8[0..1] ∈ UNINITIALIZED
- [2] ∈ {2}
- [3..9] ∈ UNINITIALIZED
+ __malloc_main1_l10[0..1] ∈ UNINITIALIZED
+ [2] ∈ {2}
+ [3..9] ∈ UNINITIALIZED
==END OF DUMP==
-tests/non-free/free.i:12:[value:malloc] weak free on bases: {__malloc_main1_l6, __malloc_main1_l8}
-tests/non-free/free.i:14:[value] allocating variable __malloc_main1_l14
-tests/non-free/free.i:16:[value:malloc] strong free on bases: {__malloc_main1_l14}
-tests/non-free/free.i:19:[value:malloc] strong free on bases: {}
-tests/non-free/free.i:21:[value] allocating variable __malloc_main1_l21
-tests/non-free/free.i:24:[value:malloc] weak free on bases: {__malloc_main1_l21}
+tests/non-free/free.c:14:[value:malloc] weak free on bases: {__malloc_main1_l8, __malloc_main1_l10}
+tests/non-free/free.c:16:[value] allocating variable __malloc_main1_l16
+tests/non-free/free.c:18:[value:malloc] strong free on bases: {__malloc_main1_l16}
+tests/non-free/free.c:21:[value:malloc] strong free on bases: {}
+tests/non-free/free.c:23:[value] allocating variable __malloc_main1_l23
+tests/non-free/free.c:26:[value:malloc] weak free on bases: {__malloc_main1_l23}
[value] Recording results for main1
[value] Done for function main1
[value] computing for function main2 <- main.
- Called from tests/non-free/free.i:45.
-tests/non-free/free.i:35:[value] allocating variable __malloc_main2_l35
-tests/non-free/free.i:39:[value:malloc] strong free on bases: {__malloc_main2_l35}
+ Called from tests/non-free/free.c:45.
+tests/non-free/free.c:35:[value] allocating variable __malloc_main2_l35
+tests/non-free/free.c:39:[value:malloc] strong free on bases: {__malloc_main2_l35}
[value] Recording results for main2
[value] Done for function main2
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main1:
- p ∈ {{ &__malloc_main1_l6[0] }} or ESCAPINGADDR
- q ∈ {{ &__malloc_main1_l8[0] }} or ESCAPINGADDR
- r ∈ {{ &__malloc_main1_l6[0] ; &__malloc_main1_l8[0] }} or ESCAPINGADDR
+ __fc_heap_status ∈ [--..--]
+ p ∈ {{ &__malloc_main1_l8[0] }} or ESCAPINGADDR
+ q ∈ {{ &__malloc_main1_l10[0] }} or ESCAPINGADDR
+ r ∈ {{ &__malloc_main1_l8[0] ; &__malloc_main1_l10[0] }} or ESCAPINGADDR
u ∈ ESCAPINGADDR
t ∈ {0}
- s ∈ {{ NULL ; &__malloc_main1_l21[0] }} or ESCAPINGADDR
- __malloc_main1_l6[0] ∈ UNINITIALIZED
+ s ∈ {{ NULL ; &__malloc_main1_l23[0] }} or ESCAPINGADDR
+ __malloc_main1_l8[0] ∈ UNINITIALIZED
[1] ∈ {1}
[2..9] ∈ UNINITIALIZED
- __malloc_main1_l8[0..1] ∈ UNINITIALIZED
- [2] ∈ {2}
- [3..9] ∈ UNINITIALIZED
- __malloc_main1_l21[0..3] ∈ UNINITIALIZED
+ __malloc_main1_l10[0..1] ∈ UNINITIALIZED
+ [2] ∈ {2}
+ [3..9] ∈ UNINITIALIZED
+ __malloc_main1_l23[0..3] ∈ UNINITIALIZED
[4] ∈ {4}
[5..9] ∈ UNINITIALIZED
[value:final-states] Values at end of function main2:
+ __fc_heap_status ∈ [--..--]
p ∈ ESCAPINGADDR
i ∈ {1}
[value:final-states] Values at end of function main:
- __malloc_main1_l6[0] ∈ UNINITIALIZED
+ __fc_heap_status ∈ [--..--]
+ __malloc_main1_l8[0] ∈ UNINITIALIZED
[1] ∈ {1}
[2..9] ∈ UNINITIALIZED
- __malloc_main1_l8[0..1] ∈ UNINITIALIZED
- [2] ∈ {2}
- [3..9] ∈ UNINITIALIZED
- __malloc_main1_l21[0..3] ∈ UNINITIALIZED
+ __malloc_main1_l10[0..1] ∈ UNINITIALIZED
+ [2] ∈ {2}
+ [3..9] ∈ UNINITIALIZED
+ __malloc_main1_l23[0..3] ∈ UNINITIALIZED
[4] ∈ {4}
[5..9] ∈ UNINITIALIZED
[from] Computing for function main1
-[from] Computing for function Frama_C_malloc_fresh <-main1
-[from] Done for function Frama_C_malloc_fresh
-[from] Computing for function Frama_C_free <-main1
-tests/non-free/free.i:12:[kernel] warning: Neither code nor specification for function Frama_C_free, generating default assigns from the prototype
-[from] Done for function Frama_C_free
+[from] Computing for function malloc <-main1
+[from] Done for function malloc
+[from] Computing for function free <-main1
+[from] Done for function free
[from] Done for function main1
[from] Computing for function main2
[from] Done for function main2
@@ -82,35 +95,39 @@ tests/non-free/free.i:12:[kernel] warning: Neither code nor specification for fu
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_free:
- NO EFFECTS
-[from] Function Frama_C_malloc_fresh:
- \result FROM \nothing
+[from] Function free:
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+[from] Function malloc:
+ __fc_heap_status FROM __fc_heap_status; size (and SELF)
+ \result FROM __fc_heap_status; size
[from] Function main1:
- __malloc_main1_l6[1] FROM \nothing
- __malloc_main1_l8[2] FROM \nothing
- __malloc_main1_l14[3] FROM \nothing
- __malloc_main1_l21[4] FROM \nothing
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+ __malloc_main1_l8[1] FROM __fc_heap_status
+ __malloc_main1_l10[2] FROM __fc_heap_status
+ __malloc_main1_l16[3] FROM __fc_heap_status
+ __malloc_main1_l23[4] FROM __fc_heap_status
[from] Function main2:
- __malloc_main2_l35 FROM \nothing
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+ __malloc_main2_l35 FROM __fc_heap_status
[from] Function main:
- __malloc_main1_l6[1] FROM v (and SELF)
- __malloc_main1_l8[2] FROM v (and SELF)
- __malloc_main1_l14[3] FROM v (and SELF)
- __malloc_main1_l21[4] FROM v (and SELF)
- __malloc_main2_l35 FROM v (and SELF)
+ __fc_heap_status FROM __fc_heap_status; v (and SELF)
+ __malloc_main1_l8[1] FROM __fc_heap_status; v (and SELF)
+ __malloc_main1_l10[2] FROM __fc_heap_status; v (and SELF)
+ __malloc_main1_l16[3] FROM __fc_heap_status; v (and SELF)
+ __malloc_main1_l23[4] FROM __fc_heap_status; v (and SELF)
+ __malloc_main2_l35 FROM __fc_heap_status; v (and SELF)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main1:
- p; q; r; tmp_1; u; t; s; __malloc_main1_l6[1]; __malloc_main1_l8[2];
- __malloc_main1_l14[3]; __malloc_main1_l21[4]
+ __fc_heap_status; p; q; r; tmp_1; u; t; s; __malloc_main1_l8[1];
+ __malloc_main1_l10[2]; __malloc_main1_l16[3]; __malloc_main1_l23[4]
[inout] Inputs for function main1:
- v
+ __fc_heap_status; v
[inout] Out (internal) for function main2:
- p; i; __malloc_main2_l35
+ __fc_heap_status; p; i; __malloc_main2_l35
[inout] Inputs for function main2:
- \nothing
+ __fc_heap_status
[inout] Out (internal) for function main:
- __malloc_main1_l6[1]; __malloc_main1_l8[2]; __malloc_main1_l14[3];
- __malloc_main1_l21[4]; __malloc_main2_l35
+ __fc_heap_status; __malloc_main1_l8[1]; __malloc_main1_l10[2];
+ __malloc_main1_l16[3]; __malloc_main1_l23[4]; __malloc_main2_l35
[inout] Inputs for function main:
- v
+ __fc_heap_status; v
diff --git a/tests/non-free/oracle/imprecise-malloc-free.res.oracle b/tests/non-free/oracle/imprecise-malloc-free.res.oracle
index 1059547dd52..d6e48bd2a70 100644
--- a/tests/non-free/oracle/imprecise-malloc-free.res.oracle
+++ b/tests/non-free/oracle/imprecise-malloc-free.res.oracle
@@ -1,39 +1,44 @@
-[kernel] Parsing tests/non-free/imprecise-malloc-free.i (no preprocessing)
-tests/non-free/imprecise-malloc-free.i:25:[kernel] warning: Calling undeclared function Frama_C_free. Old style K&R code?
+[kernel] Parsing tests/non-free/imprecise-malloc-free.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
i ∈ [--..--]
-tests/non-free/imprecise-malloc-free.i:13:[value] warning: signed overflow. assert -2147483648 ≤ i + (int)((int)(&size2) >> 1);
-tests/non-free/imprecise-malloc-free.i:13:[value] warning: signed overflow. assert i + (int)((int)(&size2) >> 1) ≤ 2147483647;
-tests/non-free/imprecise-malloc-free.i:13:[value] Assigning imprecise value to size2.
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
+tests/non-free/imprecise-malloc-free.c:13:[value] warning: signed overflow. assert -2147483648 ≤ i + (int)((int)(&size2) >> 1);
+tests/non-free/imprecise-malloc-free.c:13:[value] warning: signed overflow. assert i + (int)((int)(&size2) >> 1) ≤ 2147483647;
+tests/non-free/imprecise-malloc-free.c:13:[value] Assigning imprecise value to size2.
The imprecision originates from Arithmetic
- {tests/non-free/imprecise-malloc-free.i:13}
-tests/non-free/imprecise-malloc-free.i:14:[value] allocating variable __malloc_main_l14
-tests/non-free/imprecise-malloc-free.i:14:[kernel] warning: No code nor implicit assigns clause for function Frama_C_malloc_by_stack, generating default assigns from the prototype
-tests/non-free/imprecise-malloc-free.i:15:[value] allocating variable __malloc_main_l15
-tests/non-free/imprecise-malloc-free.i:16:[value] allocating variable __malloc_main_l16
-tests/non-free/imprecise-malloc-free.i:18:[value] Frama_C_show_each:
+ {tests/non-free/imprecise-malloc-free.c:13}
+tests/non-free/imprecise-malloc-free.c:14:[value] allocating variable __malloc_main_l14
+tests/non-free/imprecise-malloc-free.c:15:[value] allocating variable __malloc_main_l15
+tests/non-free/imprecise-malloc-free.c:16:[value] allocating variable __malloc_main_l16
+tests/non-free/imprecise-malloc-free.c:18:[value] Frama_C_show_each:
{{ &__malloc_main_l14 }}, {{ &__malloc_main_l15 }}, {{ &__malloc_main_l16 }}
-tests/non-free/imprecise-malloc-free.i:19:[value] Frama_C_show_each:
+tests/non-free/imprecise-malloc-free.c:19:[value] Frama_C_show_each:
{{ garbled mix of &{__malloc_main_l14}
- (origin: Arithmetic {tests/non-free/imprecise-malloc-free.i:19}) }}
-tests/non-free/imprecise-malloc-free.i:21:[value] warning: out of bounds write. assert \valid(p);
-tests/non-free/imprecise-malloc-free.i:22:[value] warning: out of bounds write. assert \valid(q);
-tests/non-free/imprecise-malloc-free.i:23:[value] warning: out of bounds write. assert \valid(r);
-tests/non-free/imprecise-malloc-free.i:25:[value] warning: Wrong free: assert(pass a freeable address)
-tests/non-free/imprecise-malloc-free.i:25:[value:malloc] weak free on bases: {__malloc_main_l14}
-tests/non-free/imprecise-malloc-free.i:26:[value] warning: Wrong free: assert(pass a freeable address)
-tests/non-free/imprecise-malloc-free.i:26:[value:malloc] weak free on bases: {__malloc_main_l15, __malloc_main_l16}
+ (origin: Arithmetic {tests/non-free/imprecise-malloc-free.c:19}) }}
+tests/non-free/imprecise-malloc-free.c:21:[value] warning: out of bounds write. assert \valid(p);
+tests/non-free/imprecise-malloc-free.c:22:[value] warning: out of bounds write. assert \valid(q);
+tests/non-free/imprecise-malloc-free.c:23:[value] warning: out of bounds write. assert \valid(r);
+tests/non-free/imprecise-malloc-free.c:25:[value] warning: Wrong free: assert(pass a freeable address)
+tests/non-free/imprecise-malloc-free.c:25:[value:malloc] weak free on bases: {__malloc_main_l14}
+tests/non-free/imprecise-malloc-free.c:26:[value] warning: Wrong free: assert(pass a freeable address)
+tests/non-free/imprecise-malloc-free.c:26:[value:malloc] weak free on bases: {__malloc_main_l15, __malloc_main_l16}
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
size1 ∈ {{ &size1 + [-8589934592..8589934588],0%4 }}
size2 ∈
{{ garbled mix of &{size2}
- (origin: Arithmetic {tests/non-free/imprecise-malloc-free.i:13}) }}
+ (origin: Arithmetic {tests/non-free/imprecise-malloc-free.c:13}) }}
p ∈ {{ &__malloc_main_l14[0] }} or ESCAPINGADDR
q ∈ {{ &__malloc_main_l15[0] }} or ESCAPINGADDR
r ∈ {{ &__malloc_main_l16[0] }} or ESCAPINGADDR
@@ -44,61 +49,26 @@ tests/non-free/imprecise-malloc-free.i:26:[value:malloc] weak free on bases: {__
__malloc_main_l16[0] ∈ {{ (int)&__malloc_main_l16[3] }} or ESCAPINGADDR
[1..1073741823] ∈ UNINITIALIZED
[from] Computing for function main
-[from] Computing for function Frama_C_malloc_by_stack <-main
-[from] Done for function Frama_C_malloc_by_stack
-[from] Computing for function Frama_C_free <-main
-tests/non-free/imprecise-malloc-free.i:25:[kernel] warning: Neither code nor specification for function Frama_C_free, generating default assigns from the prototype
-[from] Done for function Frama_C_free
+[from] Computing for function malloc <-main
+[from] Done for function malloc
+[from] Computing for function free <-main
+[from] Done for function free
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_free:
- __malloc_main_l14[0..1073741823]
- FROM __malloc_main_l14[0..1073741823];
- __malloc_main_l15[0..1073741823];
- __malloc_main_l16[0..1073741823] (and SELF)
- __malloc_main_l15[0..1073741823]
- FROM __malloc_main_l14[0..1073741823];
- __malloc_main_l15[0..1073741823];
- __malloc_main_l16[0..1073741823] (and SELF)
- __malloc_main_l16[0..1073741823]
- FROM __malloc_main_l14[0..1073741823];
- __malloc_main_l15[0..1073741823];
- __malloc_main_l16[0..1073741823] (and SELF)
- \result FROM __malloc_main_l14[0..1073741823];
- __malloc_main_l15[0..1073741823];
- __malloc_main_l16[0..1073741823]
-[from] Function Frama_C_malloc_by_stack:
- \result FROM \nothing
+[from] Function free:
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+[from] Function malloc:
+ __fc_heap_status FROM __fc_heap_status; size (and SELF)
+ \result FROM __fc_heap_status; size
[from] Function main:
- __malloc_main_l14[0]
- FROM __malloc_main_l14[1..1073741823];
- __malloc_main_l15[1..1073741823];
- __malloc_main_l16[1..1073741823]
- [1..1073741823]
- FROM __malloc_main_l14[1..1073741823];
- __malloc_main_l15[1..1073741823];
- __malloc_main_l16[1..1073741823] (and SELF)
- __malloc_main_l15[0]
- FROM __malloc_main_l14[1..1073741823];
- __malloc_main_l15[1..1073741823];
- __malloc_main_l16[1..1073741823]
- [1..1073741823]
- FROM __malloc_main_l14[1..1073741823];
- __malloc_main_l15[1..1073741823];
- __malloc_main_l16[1..1073741823] (and SELF)
- __malloc_main_l16[0]
- FROM __malloc_main_l14[1..1073741823];
- __malloc_main_l15[1..1073741823];
- __malloc_main_l16[1..1073741823]
- [1..1073741823]
- FROM __malloc_main_l14[1..1073741823];
- __malloc_main_l15[1..1073741823];
- __malloc_main_l16[1..1073741823] (and SELF)
+ __fc_heap_status FROM i; __fc_heap_status (and SELF)
+ __malloc_main_l14[0] FROM __fc_heap_status
+ __malloc_main_l15[0] FROM i; __fc_heap_status
+ __malloc_main_l16[0] FROM i; __fc_heap_status
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- size1; size2; p; q; r; __malloc_main_l14[0]; __malloc_main_l15[0];
- __malloc_main_l16[0]
+ __fc_heap_status; size1; size2; p; q; r; __malloc_main_l14[0];
+ __malloc_main_l15[0]; __malloc_main_l16[0]
[inout] Inputs for function main:
- i; __malloc_main_l14[0..1073741823]; __malloc_main_l15[0..1073741823];
- __malloc_main_l16[0..1073741823]
+ i; __fc_heap_status
diff --git a/tests/non-free/oracle/imprecise.res.oracle b/tests/non-free/oracle/imprecise.res.oracle
index bd9294610f1..9371b28cf70 100644
--- a/tests/non-free/oracle/imprecise.res.oracle
+++ b/tests/non-free/oracle/imprecise.res.oracle
@@ -79,9 +79,8 @@ tests/non-free/imprecise.c:48:[value] warning: out of bounds read. assert \valid
tests/non-free/imprecise.c:50:[value] warning: out of bounds write. assert \valid(&v2);
tests/non-free/imprecise.c:50:[value] warning: accessing uninitialized left-value. assert \initialized(&v1);
tests/non-free/imprecise.c:50:[value] warning: out of bounds read. assert \valid_read(&v1);
-tests/non-free/imprecise.c:51:[value] Call to builtin memset(({{ (void *)&v3 }},{-5},[0..4294967295]))
-tests/non-free/imprecise.c:51:[value] warning: out of bounds write.
- assert \valid((char *)(&v3) + (0 .. (unsigned long)sizeof(v3) - 1));
+tests/non-free/imprecise.c:51:[value] Call to builtin memset(({{ (void *)&v3 }},{-5},[--..--]))
+tests/non-free/imprecise.c:51:[value] warning: out of bounds write. assert \valid((char *)(&v3) + (0 .. sizeof(v3) - 1));
tests/non-free/imprecise.c:53:[value] warning: out of bounds write. assert \valid(p2);
tests/non-free/imprecise.c:54:[value] warning: out of bounds write. assert \valid(t[5]);
tests/non-free/imprecise.c:54:[value] warning: accessing uninitialized left-value. assert \initialized(&v2);
@@ -126,8 +125,7 @@ tests/non-free/imprecise.c:76:[value] Frama_C_dump_each:
v2.[bits 0 to 31] ∈ [--..--] or UNINITIALIZED
.[bits 32 to 63] ∈ {{ (? *)&addr }}
.[bits 64 to ..] ∈ [--..--] or UNINITIALIZED
- v3.[bits 0 to 34359738359]# ∈ {0; 251} or UNINITIALIZED repeated %8
- .[bits 34359738360 to ..] ∈ {0} or UNINITIALIZED
+ v3.[bits 0 to ..]# ∈ {0; 251} or UNINITIALIZED repeated %8
v5.[bits 0 to 262143]# ∈ {0; 18; 19; 20} or UNINITIALIZED repeated %8
.[bits 262144 to 17179869183]# ∈
{0; 19; 20} or UNINITIALIZED repeated %8
@@ -163,8 +161,7 @@ tests/non-free/imprecise.c:78:[value] Frama_C_dump_each:
v2.[bits 0 to 31] ∈ [--..--] or UNINITIALIZED
.[bits 32 to 63] ∈ {{ (? *)&addr }}
.[bits 64 to ..] ∈ [--..--] or UNINITIALIZED
- v3.[bits 0 to 34359738359]# ∈ {0; 251} or UNINITIALIZED repeated %8
- .[bits 34359738360 to ..] ∈ {0} or UNINITIALIZED
+ v3.[bits 0 to ..]# ∈ {0; 251} or UNINITIALIZED repeated %8
v5.[bits 0 to 262143]# ∈ {0; 18; 19; 20} or UNINITIALIZED repeated %8
.[bits 262144 to 17179869183]# ∈
{0; 19; 20} or UNINITIALIZED repeated %8
@@ -233,27 +230,6 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
[from] Done for function main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function abstract_structs:
- NULL[rbits 800 to 1607] ∈
- {{ garbled mix of &{addr}
- (origin: Misaligned {tests/non-free/imprecise.c:54}) }} or ESCAPINGADDR
- v1.[bits 0 to 7] ∈ [--..--]
- .[bits 8 to ..] ∈ {0} or UNINITIALIZED
- v2.[bits 0 to 31] ∈ [--..--] or UNINITIALIZED
- .[bits 32 to 63] ∈ {{ (? *)&addr }}
- .[bits 64 to ..] ∈ [--..--] or UNINITIALIZED
- v3.[bits 0 to 34359738359]# ∈ {0; 251} or UNINITIALIZED repeated %8
- .[bits 34359738360 to ..] ∈ {0} or UNINITIALIZED
- v5.[bits 0 to 262143]# ∈ {0; 18; 19; 20} or UNINITIALIZED repeated %8
- .[bits 262144 to 17179869183]# ∈
- {0; 19; 20} or UNINITIALIZED repeated %8
- .[bits 17179869184 to ..]# ∈ {0; 20} or UNINITIALIZED repeated %8
- p ∈ {{ (char *)&v1 }}
- q ∈ {1}
- p2 ∈ {{ &v2 + {4} }}
- p4 ∈ {{ &v5 + [0..32767] }}
- p5 ∈ {{ &v5 + [0..2147483647] }}
- p6 ∈ {{ &v5 + [0..4294967295] }}
[value:final-states] Values at end of function cast_address:
p ∈ {{ &x }}
c1 ∈
@@ -284,6 +260,26 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
[299]{.i2; .[bits 48 to 63]} ∈ UNINITIALIZED
t_packed2{[0..298]; [299].i1} ∈ [--..--] or UNINITIALIZED
[299].i2 ∈ UNINITIALIZED
+[value:final-states] Values at end of function abstract_structs:
+ NULL[rbits 800 to 1607] ∈
+ {{ garbled mix of &{addr}
+ (origin: Misaligned {tests/non-free/imprecise.c:54}) }} or ESCAPINGADDR
+ v1.[bits 0 to 7] ∈ [--..--]
+ .[bits 8 to ..] ∈ {0} or UNINITIALIZED
+ v2.[bits 0 to 31] ∈ [--..--] or UNINITIALIZED
+ .[bits 32 to 63] ∈ {{ (? *)&addr }}
+ .[bits 64 to ..] ∈ [--..--] or UNINITIALIZED
+ v3.[bits 0 to ..]# ∈ {0; 251} or UNINITIALIZED repeated %8
+ v5.[bits 0 to 262143]# ∈ {0; 18; 19; 20} or UNINITIALIZED repeated %8
+ .[bits 262144 to 17179869183]# ∈
+ {0; 19; 20} or UNINITIALIZED repeated %8
+ .[bits 17179869184 to ..]# ∈ {0; 20} or UNINITIALIZED repeated %8
+ p ∈ {{ (char *)&v1 }}
+ q ∈ {1}
+ p2 ∈ {{ &v2 + {4} }}
+ p4 ∈ {{ &v5 + [0..32767] }}
+ p5 ∈ {{ &v5 + [0..2147483647] }}
+ p6 ∈ {{ &v5 + [0..4294967295] }}
[value:final-states] Values at end of function overlap:
t_char[0..99] ∈ [--..--] or UNINITIALIZED
[value:final-states] Values at end of function paste_big:
@@ -320,8 +316,7 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
v2.[bits 0 to 31] ∈ [--..--] or UNINITIALIZED
.[bits 32 to 63] ∈ {{ (? *)&addr }}
.[bits 64 to ..] ∈ [--..--] or UNINITIALIZED
- v3.[bits 0 to 34359738359]# ∈ {0; 251} or UNINITIALIZED repeated %8
- .[bits 34359738360 to ..] ∈ {0} or UNINITIALIZED
+ v3.[bits 0 to ..]# ∈ {0; 251} or UNINITIALIZED repeated %8
v5.[bits 0 to 262143]# ∈ {0; 18; 19; 20} or UNINITIALIZED repeated %8
.[bits 262144 to 17179869183]# ∈
{0; 19; 20} or UNINITIALIZED repeated %8
@@ -332,10 +327,6 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
alloced_return_gm_f1[bits 0 to ..] ∈
{{ garbled mix of &{addr; alloced_return_gm_f1}
(origin: Misaligned {tests/non-free/imprecise.c:54}) }}
-[from] Computing for function abstract_structs
-[from] Computing for function Frama_C_memset <-abstract_structs
-[from] Done for function Frama_C_memset
-[from] Done for function abstract_structs
[from] Computing for function cast_address
[from] Done for function cast_address
[from] Computing for function garbled_mix_null
@@ -350,6 +341,10 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
[from] Done for function invalid_assigns_imprecise
[from] Computing for function many_writes
[from] Done for function many_writes
+[from] Computing for function abstract_structs
+[from] Computing for function memset <-abstract_structs
+[from] Done for function memset
+[from] Done for function abstract_structs
[from] Computing for function overlap
[from] Done for function overlap
[from] Computing for function paste_big
@@ -362,19 +357,6 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_memset:
- v3.[bits 0 to 34359738359] FROM c (and SELF)
- s FROM c (and SELF)
- \result FROM p
-[from] Function abstract_structs:
- NULL[100..200] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
- v1.[bits 0 to 7] FROM v; v2[..]
- .[bits 8 to ..] FROM v; v2[..] (and SELF)
- v2{.[bits 0 to 31]; .[bits 64 to ..]}
- FROM v; v1.[bits 8 to ..]; v2[..] (and SELF)
- .[bits 32 to 63] FROM \nothing
- v3.[bits 0 to 34359738359] FROM \nothing (and SELF)
- v5.[bits 0 to ..] FROM v (and SELF)
[from] Function cast_address:
NO EFFECTS
[from] Function f:
@@ -405,6 +387,19 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
NULL[100..200] FROM \nothing (and SELF)
[from] Function many_writes:
NO EFFECTS
+[from] Function memset:
+ v3.[bits 0 to 34359738359] FROM c (and SELF)
+ s FROM c (and SELF)
+ \result FROM s
+[from] Function abstract_structs:
+ NULL[100..200] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
+ v1.[bits 0 to 7] FROM v; v2[..]
+ .[bits 8 to ..] FROM v; v2[..] (and SELF)
+ v2{.[bits 0 to 31]; .[bits 64 to ..]}
+ FROM v; v1.[bits 8 to ..]; v2[..] (and SELF)
+ .[bits 32 to 63] FROM \nothing
+ v3.[bits 0 to 34359738359] FROM \nothing (and SELF)
+ v5.[bits 0 to ..] FROM v (and SELF)
[from] Function overlap:
NO EFFECTS
[from] Function paste_big:
@@ -434,9 +429,6 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
alloced_return_gm_f1[bits 0 to ..] (and SELF)
[from] ====== END OF DEPENDENCIES ======
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to Frama_C_memset at tests/non-free/imprecise.c:51 (by abstract_structs):
- v3.[bits 0 to 34359738359] FROM c (and SELF)
- \result FROM p
[from] call to gm_f1 at tests/non-free/imprecise.c:75 (by garbled_mix_null):
\result FROM \nothing
[from] call to Frama_C_dump_each at tests/non-free/imprecise.c:76 (by garbled_mix_null):
@@ -455,9 +447,12 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
\result FROM \nothing
[from] call to f at tests/non-free/imprecise.c:11 (by invalid_assigns_imprecise):
NULL[100..200] FROM \nothing (and SELF)
-[from] call to Frama_C_memset at tests/non-free/imprecise.c:132 (by paste_big):
+[from] call to memset at tests/non-free/imprecise.c:51 (by abstract_structs):
+ v3.[bits 0 to ..] FROM c (and SELF)
+ \result FROM s
+[from] call to memset at tests/non-free/imprecise.c:132 (by paste_big):
s FROM c
- \result FROM p
+ \result FROM s
[from] call to Frama_C_dump_each at tests/non-free/imprecise.c:21 (by write_garbled):
\result FROM \nothing
[from] call to invalid_assigns_imprecise at tests/non-free/imprecise.c:143 (by main):
@@ -471,7 +466,7 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
v2{.[bits 0 to 31]; .[bits 64 to ..]}
FROM v; v1.[bits 8 to ..]; v2[..] (and SELF)
.[bits 32 to 63] FROM \nothing
- v3.[bits 0 to 34359738359] FROM \nothing (and SELF)
+ v3.[bits 0 to ..] FROM \nothing (and SELF)
v5.[bits 0 to ..] FROM v (and SELF)
[from] call to cast_address at tests/non-free/imprecise.c:146 (by main):
NO EFFECTS
@@ -504,7 +499,7 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
v2{.[bits 0 to 31]; .[bits 64 to ..]}
FROM v; v1.[bits 8 to ..]; v2[..] (and SELF)
.[bits 32 to 63] FROM \nothing
- v3.[bits 0 to 34359738359] FROM \nothing (and SELF)
+ v3.[bits 0 to ..] FROM \nothing (and SELF)
v5.[bits 0 to ..] FROM v (and SELF)
p_gm_null FROM \nothing
s1.[bits 0 to ..] FROM s2[..] (and SELF)
@@ -513,18 +508,6 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
v2[..]; t[5];
alloced_return_gm_f1[bits 0 to ..] (and SELF)
[from] ====== END OF CALLWISE DEPENDENCIES ======
-[inout] Out (internal) for function abstract_structs:
- NULL[..]; v1[..]; v2[..]; v3.[bits 0 to 34359738359]; v5.[bits 0 to ..];
- p; w1; w; q; p2; p4; p5; p6
-[inout] Inputs for function abstract_structs:
- v; v1[..]; v2[..]; t[5]
-[inout] InOut (internal) for function abstract_structs:
- Operational inputs:
- v; v1[..]; v2[..]; t[5]
- Operational inputs on termination:
- v; v1[..]; v2[..]; t[5]
- Sure outputs:
- v1.[bits 0 to 7]; v2.[bits 32 to 63]; p; q; p2; p4; p5; p6
[inout] Out (internal) for function cast_address:
p; c1; c2; c3
[inout] Inputs for function cast_address:
@@ -569,6 +552,18 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
v
Sure outputs:
\nothing
+[inout] Out (internal) for function abstract_structs:
+ NULL[..]; v1[..]; v2[..]; v3.[bits 0 to ..]; v5.[bits 0 to ..]; p;
+ w1; w; q; p2; p4; p5; p6
+[inout] Inputs for function abstract_structs:
+ v; v1[..]; v2[..]; t[5]
+[inout] InOut (internal) for function abstract_structs:
+ Operational inputs:
+ v; v1[..]; v2[..]; t[5]
+ Operational inputs on termination:
+ v; v1[..]; v2[..]; t[5]
+ Sure outputs:
+ v1.[bits 0 to 7]; v2.[bits 32 to 63]; p; q; p2; p4; p5; p6
[inout] Out (internal) for function overlap:
t_char[0..99]
[inout] Inputs for function overlap:
@@ -614,8 +609,8 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
Sure outputs:
i; j; k[0..4]; p
[inout] Out (internal) for function main:
- NULL[..]; addr; v1[..]; v2[..]; v3.[bits 0 to 34359738359];
- v5.[bits 0 to ..]; p_gm_null; s1[..]; alloced_return_gm_f1[bits 0 to ..]
+ NULL[..]; addr; v1[..]; v2[..]; v3.[bits 0 to ..]; v5.[bits 0 to ..];
+ p_gm_null; s1[..]; alloced_return_gm_f1[bits 0 to ..]
[inout] Inputs for function main:
NULL[100..200]; v; addr; v1[..]; v2[..]; t[5]; p_gm_null; s2[..];
alloced_return_gm_f1[bits 0 to ..]
@@ -711,9 +706,8 @@ tests/non-free/imprecise.c:48:[value] warning: out of bounds read. assert \valid
tests/non-free/imprecise.c:50:[value] warning: out of bounds write. assert \valid(&v2);
tests/non-free/imprecise.c:50:[value] warning: accessing uninitialized left-value. assert \initialized(&v1);
tests/non-free/imprecise.c:50:[value] warning: out of bounds read. assert \valid_read(&v1);
-tests/non-free/imprecise.c:51:[value] Call to builtin memset(({{ (void *)&v3 }},{-5},[0..4294967295]))
-tests/non-free/imprecise.c:51:[value] warning: out of bounds write.
- assert \valid((char *)(&v3) + (0 .. (unsigned long)sizeof(v3) - 1));
+tests/non-free/imprecise.c:51:[value] Call to builtin memset(({{ (void *)&v3 }},{-5},[--..--]))
+tests/non-free/imprecise.c:51:[value] warning: out of bounds write. assert \valid((char *)(&v3) + (0 .. sizeof(v3) - 1));
tests/non-free/imprecise.c:53:[value] warning: out of bounds write. assert \valid(p2);
tests/non-free/imprecise.c:54:[value] warning: out of bounds write. assert \valid(t[5]);
tests/non-free/imprecise.c:54:[value] warning: accessing uninitialized left-value. assert \initialized(&v2);
@@ -863,29 +857,6 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
[from] Done for function main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function abstract_structs:
- NULL[rbits 800 to 1607] ∈
- {{ garbled mix of &{addr}
- (origin: Misaligned {tests/non-free/imprecise.c:54}) }} or ESCAPINGADDR
- v1.[bits 0 to 7] ∈ [--..--]
- .[bits 8 to ..] ∈ [--..--] or UNINITIALIZED
- v2.[bits 0 to 31] ∈ [--..--] or UNINITIALIZED
- .[bits 32 to 63] ∈ {{ (? *)&addr }}
- .[bits 64 to ..] ∈ [--..--] or UNINITIALIZED
- v3.[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
- v5.[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
- p ∈ {{ (char *)&v1 }}
- q ∈ {1}
- p2 ∈ {{ &v2 + {4} }}
- p4 ∈ {{ &v5 + [0..32767] }}
- p5 ∈ {{ &v5 + [0..2147483647] }}
- p6 ∈ {{ &v5 + [0..4294967295] }}
- S_0_t[bits 0 to ..] ∈
- {{ garbled mix of &{addr}
- (origin: Misaligned {tests/non-free/imprecise.c:54}) }} or UNINITIALIZED
- S_1_t[bits 0 to ..] ∈
- {{ garbled mix of &{addr}
- (origin: Misaligned {tests/non-free/imprecise.c:54}) }} or UNINITIALIZED
[value:final-states] Values at end of function cast_address:
p ∈ {{ &x }}
c1 ∈
@@ -916,6 +887,29 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
[299]{.i2; .[bits 48 to 63]} ∈ UNINITIALIZED
t_packed2{[0..298]; [299].i1} ∈ [--..--] or UNINITIALIZED
[299].i2 ∈ UNINITIALIZED
+[value:final-states] Values at end of function abstract_structs:
+ NULL[rbits 800 to 1607] ∈
+ {{ garbled mix of &{addr}
+ (origin: Misaligned {tests/non-free/imprecise.c:54}) }} or ESCAPINGADDR
+ v1.[bits 0 to 7] ∈ [--..--]
+ .[bits 8 to ..] ∈ [--..--] or UNINITIALIZED
+ v2.[bits 0 to 31] ∈ [--..--] or UNINITIALIZED
+ .[bits 32 to 63] ∈ {{ (? *)&addr }}
+ .[bits 64 to ..] ∈ [--..--] or UNINITIALIZED
+ v3.[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
+ v5.[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
+ p ∈ {{ (char *)&v1 }}
+ q ∈ {1}
+ p2 ∈ {{ &v2 + {4} }}
+ p4 ∈ {{ &v5 + [0..32767] }}
+ p5 ∈ {{ &v5 + [0..2147483647] }}
+ p6 ∈ {{ &v5 + [0..4294967295] }}
+ S_0_t[bits 0 to ..] ∈
+ {{ garbled mix of &{addr}
+ (origin: Misaligned {tests/non-free/imprecise.c:54}) }} or UNINITIALIZED
+ S_1_t[bits 0 to ..] ∈
+ {{ garbled mix of &{addr}
+ (origin: Misaligned {tests/non-free/imprecise.c:54}) }} or UNINITIALIZED
[value:final-states] Values at end of function overlap:
t_char[0..99] ∈ [--..--] or UNINITIALIZED
[value:final-states] Values at end of function paste_big:
@@ -966,10 +960,6 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
S_1_t[bits 0 to ..] ∈
{{ garbled mix of &{addr}
(origin: Misaligned {tests/non-free/imprecise.c:54}) }} or UNINITIALIZED
-[from] Computing for function abstract_structs
-[from] Computing for function Frama_C_memset <-abstract_structs
-[from] Done for function Frama_C_memset
-[from] Done for function abstract_structs
[from] Computing for function cast_address
[from] Done for function cast_address
[from] Computing for function garbled_mix_null
@@ -984,6 +974,10 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
[from] Done for function invalid_assigns_imprecise
[from] Computing for function many_writes
[from] Done for function many_writes
+[from] Computing for function abstract_structs
+[from] Computing for function memset <-abstract_structs
+[from] Done for function memset
+[from] Done for function abstract_structs
[from] Computing for function overlap
[from] Done for function overlap
[from] Computing for function paste_big
@@ -996,21 +990,6 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_memset:
- v3.[bits 0 to 34359738359] FROM c (and SELF)
- s FROM c (and SELF)
- \result FROM p
-[from] Function abstract_structs:
- NULL[100..200] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
- v1.[bits 0 to 7] FROM v; v2[..]
- .[bits 8 to ..] FROM v; v2[..] (and SELF)
- v2{.[bits 0 to 31]; .[bits 64 to ..]}
- FROM v; v1.[bits 8 to ..]; v2[..] (and SELF)
- .[bits 32 to 63] FROM \nothing
- v3.[bits 0 to 34359738359] FROM \nothing (and SELF)
- v5.[bits 0 to ..] FROM v (and SELF)
- S_0_t[bits 0 to ..] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
- S_1_t[bits 0 to ..] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
[from] Function cast_address:
NO EFFECTS
[from] Function f:
@@ -1041,6 +1020,21 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
NULL[100..200] FROM \nothing (and SELF)
[from] Function many_writes:
NO EFFECTS
+[from] Function memset:
+ v3.[bits 0 to 34359738359] FROM c (and SELF)
+ s FROM c (and SELF)
+ \result FROM s
+[from] Function abstract_structs:
+ NULL[100..200] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
+ v1.[bits 0 to 7] FROM v; v2[..]
+ .[bits 8 to ..] FROM v; v2[..] (and SELF)
+ v2{.[bits 0 to 31]; .[bits 64 to ..]}
+ FROM v; v1.[bits 8 to ..]; v2[..] (and SELF)
+ .[bits 32 to 63] FROM \nothing
+ v3.[bits 0 to 34359738359] FROM \nothing (and SELF)
+ v5.[bits 0 to ..] FROM v (and SELF)
+ S_0_t[bits 0 to ..] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
+ S_1_t[bits 0 to ..] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
[from] Function overlap:
NO EFFECTS
[from] Function paste_big:
@@ -1072,9 +1066,6 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
S_1_t[bits 0 to ..] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
[from] ====== END OF DEPENDENCIES ======
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to Frama_C_memset at tests/non-free/imprecise.c:51 (by abstract_structs):
- v3.[bits 0 to 34359738359] FROM c (and SELF)
- \result FROM p
[from] call to gm_f1 at tests/non-free/imprecise.c:75 (by garbled_mix_null):
\result FROM \nothing
[from] call to Frama_C_dump_each at tests/non-free/imprecise.c:76 (by garbled_mix_null):
@@ -1093,9 +1084,12 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
\result FROM \nothing
[from] call to f at tests/non-free/imprecise.c:11 (by invalid_assigns_imprecise):
NULL[100..200] FROM \nothing (and SELF)
-[from] call to Frama_C_memset at tests/non-free/imprecise.c:132 (by paste_big):
+[from] call to memset at tests/non-free/imprecise.c:51 (by abstract_structs):
+ v3.[bits 0 to ..] FROM c (and SELF)
+ \result FROM s
+[from] call to memset at tests/non-free/imprecise.c:132 (by paste_big):
s FROM c
- \result FROM p
+ \result FROM s
[from] call to Frama_C_dump_each at tests/non-free/imprecise.c:21 (by write_garbled):
\result FROM \nothing
[from] call to invalid_assigns_imprecise at tests/non-free/imprecise.c:143 (by main):
@@ -1109,7 +1103,7 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
v2{.[bits 0 to 31]; .[bits 64 to ..]}
FROM v; v1.[bits 8 to ..]; v2[..] (and SELF)
.[bits 32 to 63] FROM \nothing
- v3.[bits 0 to 34359738359] FROM \nothing (and SELF)
+ v3.[bits 0 to ..] FROM \nothing (and SELF)
v5.[bits 0 to ..] FROM v (and SELF)
S_0_t[bits 0 to ..] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
S_1_t[bits 0 to ..] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
@@ -1144,7 +1138,7 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
v2{.[bits 0 to 31]; .[bits 64 to ..]}
FROM v; v1.[bits 8 to ..]; v2[..] (and SELF)
.[bits 32 to 63] FROM \nothing
- v3.[bits 0 to 34359738359] FROM \nothing (and SELF)
+ v3.[bits 0 to ..] FROM \nothing (and SELF)
v5.[bits 0 to ..] FROM v (and SELF)
p_gm_null FROM \nothing
s1.[bits 0 to ..] FROM s2[..] (and SELF)
@@ -1155,18 +1149,6 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
S_0_t[bits 0 to ..] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
S_1_t[bits 0 to ..] FROM v; v1.[bits 8 to ..]; v2[..]; t[5] (and SELF)
[from] ====== END OF CALLWISE DEPENDENCIES ======
-[inout] Out (internal) for function abstract_structs:
- NULL[..]; v1[..]; v2[..]; v3.[bits 0 to 34359738359]; v5.[bits 0 to ..];
- p; w1; w; q; p2; p4; p5; p6; S_0_t[..]; S_1_t[..]
-[inout] Inputs for function abstract_structs:
- v; v1[..]; v2[..]; t[5]
-[inout] InOut (internal) for function abstract_structs:
- Operational inputs:
- v; v1[..]; v2[..]; t[5]
- Operational inputs on termination:
- v; v1[..]; v2[..]; t[5]
- Sure outputs:
- v1.[bits 0 to 7]; v2.[bits 32 to 63]; p; q; p2; p4; p5; p6
[inout] Out (internal) for function cast_address:
p; c1; c2; c3
[inout] Inputs for function cast_address:
@@ -1211,6 +1193,18 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
v
Sure outputs:
\nothing
+[inout] Out (internal) for function abstract_structs:
+ NULL[..]; v1[..]; v2[..]; v3.[bits 0 to ..]; v5.[bits 0 to ..]; p;
+ w1; w; q; p2; p4; p5; p6; S_0_t[..]; S_1_t[..]
+[inout] Inputs for function abstract_structs:
+ v; v1[..]; v2[..]; t[5]
+[inout] InOut (internal) for function abstract_structs:
+ Operational inputs:
+ v; v1[..]; v2[..]; t[5]
+ Operational inputs on termination:
+ v; v1[..]; v2[..]; t[5]
+ Sure outputs:
+ v1.[bits 0 to 7]; v2.[bits 32 to 63]; p; q; p2; p4; p5; p6
[inout] Out (internal) for function overlap:
t_char[0..99]
[inout] Inputs for function overlap:
@@ -1256,9 +1250,8 @@ tests/non-free/imprecise.c:139:[value] warning: accessing uninitialized left-val
Sure outputs:
i; j; k[0..4]; p
[inout] Out (internal) for function main:
- NULL[..]; addr; v1[..]; v2[..]; v3.[bits 0 to 34359738359];
- v5.[bits 0 to ..]; p_gm_null; s1[..]; alloced_return_gm_f1[bits 0 to ..];
- S_0_t[..]; S_1_t[..]
+ NULL[..]; addr; v1[..]; v2[..]; v3.[bits 0 to ..]; v5.[bits 0 to ..];
+ p_gm_null; s1[..]; alloced_return_gm_f1[bits 0 to ..]; S_0_t[..]; S_1_t[..]
[inout] Inputs for function main:
NULL[100..200]; v; addr; v1[..]; v2[..]; t[5]; p_gm_null; s2[..];
alloced_return_gm_f1[bits 0 to ..]
diff --git a/tests/non-free/oracle/memchr.res.oracle b/tests/non-free/oracle/memchr.res.oracle
index 4ee572bbab3..97504f7f40f 100644
--- a/tests/non-free/oracle/memchr.res.oracle
+++ b/tests/non-free/oracle/memchr.res.oracle
@@ -24,6 +24,8 @@
[value] computing for function my_memchr <- memchr_small_sets <- main.
Called from tests/non-free/memchr.c:81.
tests/non-free/memchr.c:50:[value] Call to builtin Frama_C_memchr(({{ "abc" + {0; 1} }},{0},{4}))
+share/libc/string.h:46:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic function memchr
+share/libc/string.h:53:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic function memchr
tests/non-free/memchr.c:57:[value] Frama_C_show_each_mymemchr: {3}
[value] Recording results for my_memchr
[value] Done for function my_memchr
@@ -1129,6 +1131,14 @@ tests/non-free/memchr.c:641:[value] assertion got status valid.
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
+[value:final-states] Values at end of function memchr_bitfields:
+ c ∈ {0}
+ s.a ∈ {3}
+ .b ∈ {1}
+ .[bits 16 to 31] ∈ UNINITIALIZED
+ .c ∈ {7}
+ .[bits 49 to 63] ∈ UNINITIALIZED
+ p ∈ {{ (char *)&s }}
[value:final-states] Values at end of function init_array_nondet:
from ∈ {-1}
to ∈ {-1}
@@ -1147,14 +1157,6 @@ tests/non-free/memchr.c:641:[value] assertion got status valid.
[12..15] ∈ {1} or UNINITIALIZED
[16..19] ∈ {0; 1} or UNINITIALIZED
[20..99] ∈ UNINITIALIZED
-[value:final-states] Values at end of function memchr_bitfields:
- c ∈ {0}
- s.a ∈ {3}
- .b ∈ {1}
- .[bits 16 to 31] ∈ UNINITIALIZED
- .c ∈ {7}
- .[bits 49 to 63] ∈ UNINITIALIZED
- p ∈ {{ (char *)&s }}
[value:final-states] Values at end of function my_memchr:
s ∈
{{ &t[0] ; &empty_or_non_terminated[0] ; &non_terminated[0] ;
@@ -1405,14 +1407,14 @@ tests/non-free/memchr.c:641:[value] assertion got status valid.
static_str ∈ {{ "Hello World\n" }}
zero_str ∈ {{ "abc\000\000\000abc" }}
__retres ∈ {0}
-[from] Computing for function init_array_nondet
-[from] Computing for function Frama_C_memset <-init_array_nondet
-[from] Done for function Frama_C_memset
-[from] Done for function init_array_nondet
[from] Computing for function memchr_bitfields
-[from] Computing for function Frama_C_memchr <-memchr_bitfields
-[from] Done for function Frama_C_memchr
+[from] Computing for function memchr <-memchr_bitfields
+[from] Done for function memchr
[from] Done for function memchr_bitfields
+[from] Computing for function init_array_nondet
+[from] Computing for function memset <-init_array_nondet
+[from] Done for function memset
+[from] Done for function init_array_nondet
[from] Computing for function my_memchr
[from] Done for function my_memchr
[from] Computing for function memchr_big_array
@@ -1462,8 +1464,8 @@ tests/non-free/memchr.c:641:[value] assertion got status valid.
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
-[from] Function Frama_C_memchr:
- \result FROM c; n; t[0..3]; empty_or_non_terminated[0]; non_terminated[0];
+[from] Function memchr:
+ \result FROM s; c; t[0..3]; empty_or_non_terminated[0]; non_terminated[0];
non_terminated2[2..3]; empty_or_uninitialized[0];
uninitialized[0]; s[0..1]; t[0..3]; s; s; a[3..99]; a[3..99];
s[0..3]; loc_char_array[0..4]; x; unterminated_string[0..11];
@@ -1483,21 +1485,21 @@ tests/non-free/memchr.c:641:[value] assertion got status valid.
"abcde"[bits 0 to 47]; "\000bcdef"[bits 0 to 55];
"bcd\000efg"[bits 0 to 63]; "abc"; "bcd\000eg"[bits 0 to 55];
"abc"; "\000bc"; ""[bits 0 to 7]; "b\000c"
-[from] Function Frama_C_memset:
+[from] Function memchr_bitfields:
+ NO EFFECTS
+[from] Function memset:
a[0..99] FROM c (and SELF)
a[0..99] FROM c (and SELF)
a[0..99] FROM c (and SELF)
a[0..99] FROM c (and SELF)
- \result FROM p
+ \result FROM s
[from] Function init_array_nondet:
a[0..99] FROM val1; val2; nondet (and SELF)
a[0..99] FROM val1; val2; nondet (and SELF)
a[0..99] FROM val1; val2; nondet (and SELF)
a[0..99] FROM val1; val2; nondet (and SELF)
-[from] Function memchr_bitfields:
- NO EFFECTS
[from] Function my_memchr:
- \result FROM p; c; n; t[0..3]; empty_or_non_terminated[0];
+ \result FROM p; offs; c; t[0..3]; empty_or_non_terminated[0];
non_terminated[0]; non_terminated2[2..3];
empty_or_uninitialized[0]; uninitialized[0]; s[0..1];
t[0..3]; s; a[3..99]; a[3..99]; s[0..3]; loc_char_array[0..4];
@@ -1538,21 +1540,7 @@ tests/non-free/memchr.c:641:[value] assertion got status valid.
[from] Function memchr_small_sets:
NO EFFECTS
[from] Function memchr_small_sets_no_assertions:
- res[0..3]
- FROM c; res; ""[bits 0 to 7]; "a"[bits 0 to 15]; "aa"[bits 0 to 23];
- "aaa"; "aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
- "aaaaaa"[bits 0 to 55]; "aaaaaaaaa"[bits 0 to 79];
- "aaaaaaaaaa"[bits 0 to 87]; "aaaaaaaaaaa"[bits 0 to 95];
- "aaaaaaaaaaaa"[bits 0 to 103]; "aaaaaaaaaaaaa"[bits 0 to 111];
- "abc"; "\000bc"; ""[bits 0 to 7]; "b\000c";
- "Hello World\n"[bits 0 to 103]; "abc\000\000\000abc"[bits 0 to 79];
- "Bonjour Monde\n"[bits 0 to 119]; "abc"; "ABCD"[bits 0 to 39];
- "efg"[bits 8 to 31]; "EFGH"[bits 8 to 39];
- "mno\000pqr"[bits 0 to 63]; "MNOP\000QRS"[bits 0 to 71];
- "abcde"[bits 0 to 47]; "\000bcdef"[bits 0 to 55];
- "bcd\000efg"[bits 0 to 63]; "abc"; "bcd\000eg"[bits 0 to 55];
- "abc"; "\000bc"; ""[bits 0 to 7]; "b\000c"
- [4]
+ res{[0..1]; [3..4]}
FROM c; res; nondet; ""[bits 0 to 7]; "a"[bits 0 to 15];
"aa"[bits 0 to 23]; "aaa"; "aaaa"[bits 0 to 39];
"aaaaa"[bits 0 to 47]; "aaaaaa"[bits 0 to 55];
@@ -1567,6 +1555,20 @@ tests/non-free/memchr.c:641:[value] assertion got status valid.
"abcde"[bits 0 to 47]; "\000bcdef"[bits 0 to 55];
"bcd\000efg"[bits 0 to 63]; "abc"; "bcd\000eg"[bits 0 to 55];
"abc"; "\000bc"; ""[bits 0 to 7]; "b\000c"
+ [2]
+ FROM c; res; ""[bits 0 to 7]; "a"[bits 0 to 15]; "aa"[bits 0 to 23];
+ "aaa"; "aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
+ "aaaaaa"[bits 0 to 55]; "aaaaaaaaa"[bits 0 to 79];
+ "aaaaaaaaaa"[bits 0 to 87]; "aaaaaaaaaaa"[bits 0 to 95];
+ "aaaaaaaaaaaa"[bits 0 to 103]; "aaaaaaaaaaaaa"[bits 0 to 111];
+ "abc"; "\000bc"; ""[bits 0 to 7]; "b\000c";
+ "Hello World\n"[bits 0 to 103]; "abc\000\000\000abc"[bits 0 to 79];
+ "Bonjour Monde\n"[bits 0 to 119]; "abc"; "ABCD"[bits 0 to 39];
+ "efg"[bits 8 to 31]; "EFGH"[bits 8 to 39];
+ "mno\000pqr"[bits 0 to 63]; "MNOP\000QRS"[bits 0 to 71];
+ "abcde"[bits 0 to 47]; "\000bcdef"[bits 0 to 55];
+ "bcd\000efg"[bits 0 to 63]; "abc"; "bcd\000eg"[bits 0 to 55];
+ "abc"; "\000bc"; ""[bits 0 to 7]; "b\000c"
\result FROM \nothing
[from] Function memchr_small_sets_chars:
NO EFFECTS
@@ -1575,15 +1577,15 @@ tests/non-free/memchr.c:641:[value] assertion got status valid.
[from] Function memchr_zero_termination:
NO EFFECTS
[from] Function my_memchr2:
- \result FROM base; c; n; loc_char_array[0..4]; x;
+ \result FROM base; offs1; offs2; c; loc_char_array[0..4]; x;
unterminated_string[0..11]; maybe_init[0..1]; s[0..19];
- ""[bits 0 to 7]; "a"[bits 0 to 15]; "aa"[bits 0 to 23];
- "aaa"; "aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
- "aaaaaa"[bits 0 to 55]; "aaaaaaaaa"[bits 0 to 79];
- "aaaaaaaaaa"[bits 0 to 87]; "aaaaaaaaaaa"[bits 0 to 95];
- "aaaaaaaaaaaa"[bits 0 to 103]; "aaaaaaaaaaaaa"[bits 0 to 111];
- "abc"; "\000bc"; ""[bits 0 to 7]; "b\000c";
- "Hello World\n"[bits 0 to 103];
+ nondet; ""[bits 0 to 7]; "a"[bits 0 to 15];
+ "aa"[bits 0 to 23]; "aaa"; "aaaa"[bits 0 to 39];
+ "aaaaa"[bits 0 to 47]; "aaaaaa"[bits 0 to 55];
+ "aaaaaaaaa"[bits 0 to 79]; "aaaaaaaaaa"[bits 0 to 87];
+ "aaaaaaaaaaa"[bits 0 to 95]; "aaaaaaaaaaaa"[bits 0 to 103];
+ "aaaaaaaaaaaaa"[bits 0 to 111]; "abc"; "\000bc";
+ ""[bits 0 to 7]; "b\000c"; "Hello World\n"[bits 0 to 103];
"abc\000\000\000abc"[bits 0 to 79];
"Bonjour Monde\n"[bits 0 to 119]; "abc"; "ABCD"[bits 0 to 39];
"efg"[bits 8 to 31]; "EFGH"[bits 8 to 39];
@@ -1606,15 +1608,15 @@ tests/non-free/memchr.c:641:[value] assertion got status valid.
zero_str FROM \nothing
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function memchr_bitfields:
+ c; s{{.a; .b}; .c}; p
+[inout] Inputs for function memchr_bitfields:
+ nondet
[inout] Out (internal) for function init_array_nondet:
from; to; val1; val2; val; tmp; a[0..99]; a{[0..39]; [50..94]}; a[0..99];
a{[0..9]; [11..19]}
[inout] Inputs for function init_array_nondet:
nondet
-[inout] Out (internal) for function memchr_bitfields:
- c; s{{.a; .b}; .c}; p
-[inout] Inputs for function memchr_bitfields:
- nondet
[inout] Out (internal) for function my_memchr:
s; ss; res
[inout] Inputs for function my_memchr:
diff --git a/tests/non-free/oracle/memcpy.res.oracle b/tests/non-free/oracle/memcpy.res.oracle
index d32b066c629..a97c2781235 100644
--- a/tests/non-free/oracle/memcpy.res.oracle
+++ b/tests/non-free/oracle/memcpy.res.oracle
@@ -4,7 +4,6 @@
[value] Initial state computed
[value:initial-state] Values of globals at initialization
NULL[rbits 800000 to 800015] ∈ [--..--]
- Frama_C_entropy_source ∈ [--..--]
i ∈ [--..--]
src[0..19] ∈ {0}
dst1[0..19] ∈ {0}
@@ -232,7 +231,6 @@ tests/non-free/memcpy.c:210:[value] warning: locals {y} escaping the scope of a
tests/non-free/memcpy.c:212:[value] Frama_C_dump_each:
# Cvalue domain:
NULL[rbits 800000 to 800015] ∈ [--..--]
- Frama_C_entropy_source ∈ [--..--]
i ∈ [--..--]
src[0..19] ∈ {0}
dst1[0..19] ∈ {0}
@@ -273,11 +271,6 @@ tests/non-free/memcpy.c:230:[value] entering loop for the first time
[value] done for function main_all
[scope:rm_asserts] removing 1 assertion(s)
[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function buggy:
- c ∈ {100}
- p ∈ {{ &c ; "abc" }}
-[value:final-states] Values at end of function copy_0:
-
[value:final-states] Values at end of function init:
src[0] ∈ {1}
[1] ∈ {2}
@@ -305,6 +298,11 @@ tests/non-free/memcpy.c:230:[value] entering loop for the first time
dst4[0..19] ∈ {-1}
dst5[0..99] ∈ {-1}
j ∈ {100}
+[value:final-states] Values at end of function buggy:
+ c ∈ {100}
+ p ∈ {{ &c ; "abc" }}
+[value:final-states] Values at end of function copy_0:
+
[value:final-states] Values at end of function main_local:
p ∈ ESCAPINGADDR
q ∈ {0}
@@ -512,42 +510,42 @@ tests/non-free/memcpy.c:230:[value] entering loop for the first time
[value:final-states] Values at end of function main_all:
NON TERMINATING FUNCTION
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:28 (by buggy):
+[from] call to memcpy at tests/non-free/memcpy.c:28 (by buggy):
c FROM "d"[bits 0 to 7]
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:220 (by copy_0):
+[from] call to memcpy at tests/non-free/memcpy.c:220 (by copy_0):
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:221 (by copy_0):
+[from] call to memcpy at tests/non-free/memcpy.c:221 (by copy_0):
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:209 (by main_local):
+[from] call to memcpy at tests/non-free/memcpy.c:209 (by main_local):
p FROM q
\result FROM dest
[from] call to Frama_C_dump_each at tests/non-free/memcpy.c:212 (by main_local):
\result FROM \nothing
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:172 (by main_uninit):
+[from] call to memcpy at tests/non-free/memcpy.c:172 (by main_uninit):
b[0..9] FROM a[0..9]
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:174 (by main_uninit):
+[from] call to memcpy at tests/non-free/memcpy.c:174 (by main_uninit):
b[0..24] FROM a[0..24] (and SELF)
\result FROM dest
[from] call to itv at tests/non-free/memcpy.c:174 (by main_uninit):
\result FROM l; u
[from] call to make_unknown at tests/non-free/memcpy.c:178 (by main_uninit):
a[0..9] FROM maybe
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:179 (by main_uninit):
+[from] call to memcpy at tests/non-free/memcpy.c:179 (by main_uninit):
b[0..9] FROM a[0..9]
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:181 (by main_uninit):
+[from] call to memcpy at tests/non-free/memcpy.c:181 (by main_uninit):
b[0..24] FROM a[0..24] (and SELF)
\result FROM dest
[from] call to itv at tests/non-free/memcpy.c:181 (by main_uninit):
\result FROM l; u
[from] call to make_unknown at tests/non-free/memcpy.c:185 (by main_uninit):
b[0..9] FROM maybe
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:187 (by main_uninit):
+[from] call to memcpy at tests/non-free/memcpy.c:187 (by main_uninit):
b[0..9] FROM a[0..9]
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:190 (by main_uninit):
+[from] call to memcpy at tests/non-free/memcpy.c:190 (by main_uninit):
b[0..24] FROM a[0..24] (and SELF)
\result FROM dest
[from] call to itv at tests/non-free/memcpy.c:190 (by main_uninit):
@@ -556,21 +554,21 @@ tests/non-free/memcpy.c:230:[value] entering loop for the first time
a[0..9] FROM maybe
[from] call to make_unknown at tests/non-free/memcpy.c:197 (by main_uninit):
b[0..9] FROM maybe
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:198 (by main_uninit):
+[from] call to memcpy at tests/non-free/memcpy.c:198 (by main_uninit):
b[0..9] FROM a[0..9]
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:200 (by main_uninit):
+[from] call to memcpy at tests/non-free/memcpy.c:200 (by main_uninit):
b[0..24] FROM a[0..24] (and SELF)
\result FROM dest
[from] call to itv at tests/non-free/memcpy.c:200 (by main_uninit):
\result FROM l; u
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:47 (by many):
+[from] call to memcpy at tests/non-free/memcpy.c:47 (by many):
tm[0..999] FROM s[0..3] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:49 (by many):
+[from] call to memcpy at tests/non-free/memcpy.c:49 (by many):
um{[0..998]; [999][bits 0 to 15]} FROM s[0..1] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:53 (by many):
+[from] call to memcpy at tests/non-free/memcpy.c:53 (by many):
ttyp[0..999] FROM ty (and SELF)
\result FROM dest
[from] call to buggy at tests/non-free/memcpy.c:61 (by main):
@@ -589,70 +587,70 @@ tests/non-free/memcpy.c:230:[value] entering loop for the first time
dst3[0..19] FROM \nothing (and SELF)
dst4[0..19] FROM \nothing (and SELF)
dst5[0..99] FROM \nothing (and SELF)
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:68 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:68 (by main):
dst1[1..5] FROM src[2..6]
[6..15] FROM src[7..16] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:70 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:70 (by main):
dst2[1..10] FROM src[2..11]
[11..19] FROM src[12..19] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:73 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:73 (by main):
dst3[5..9] FROM src[2..6]
[10..18] FROM src[7..15] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:75 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:75 (by main):
dst4[5..14] FROM src[2..11]
[15..19] FROM src[12..19] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:83 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:83 (by main):
v2 FROM v1
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:85 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:85 (by main):
t[2] FROM t[0]
[3] FROM t[1] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:87 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:87 (by main):
v3 FROM t[0..3]
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:89 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:89 (by main):
v4 FROM v1{.x; .y; .p; .padding[0..3]} (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:91 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:91 (by main):
v5 FROM v4{.x; .y; .p; .padding[0..3]} (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:96 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:96 (by main):
x FROM x (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:101 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:101 (by main):
dst5[0..4] FROM src[0..4] (and SELF)
{[5..19]; [25..33]} FROM src[5..13] (and SELF)
[20..24] FROM src[0..13] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:105 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:105 (by main):
dst5[40] FROM src[0] (and SELF)
{[41..69]; [71..88]} FROM src[1..18] (and SELF)
[70] FROM src[0..18] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:114 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:114 (by main):
ptop1[4..799] FROM src[0..3] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:122 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:122 (by main):
ptop2[2..749] FROM src[1..4] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:131 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:131 (by main):
ptop3[2..797] FROM src[2..5] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:140 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:140 (by main):
ptop4[2..798] FROM src[2..6] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:145 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:145 (by main):
garbledsize[10..99] FROM src[0..19] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:151 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:151 (by main):
dstmaybesize1[0..14] FROM src[0..19] (and SELF)
\result FROM dest
-[from] call to Frama_C_memcpy at tests/non-free/memcpy.c:153 (by main):
+[from] call to memcpy at tests/non-free/memcpy.c:153 (by main):
dstmaybesize2[0..5] FROM src[0..5] (and SELF)
\result FROM dest
[from] call to main at tests/non-free/memcpy.c:226 (by main_all):
@@ -700,6 +698,18 @@ tests/non-free/memcpy.c:230:[value] entering loop for the first time
[from] entry point:
NON TERMINATING - NO EFFECTS
[from] ====== END OF CALLWISE DEPENDENCIES ======
+[inout] Out (internal) for function init:
+ src[0..19]; dst1[0..19]; dst2[0..19]; dst3[0..19]; dst4[0..19];
+ dst5[0..99]; j
+[inout] Inputs for function init:
+ \nothing
+[inout] InOut (internal) for function init:
+ Operational inputs:
+ \nothing
+ Operational inputs on termination:
+ \nothing
+ Sure outputs:
+ j
[inout] Out (internal) for function buggy:
c; p; tmp
[inout] Inputs for function buggy:
@@ -722,18 +732,6 @@ tests/non-free/memcpy.c:230:[value] entering loop for the first time
\nothing
Sure outputs:
\nothing
-[inout] Out (internal) for function init:
- src[0..19]; dst1[0..19]; dst2[0..19]; dst3[0..19]; dst4[0..19];
- dst5[0..99]; j
-[inout] Inputs for function init:
- \nothing
-[inout] InOut (internal) for function init:
- Operational inputs:
- \nothing
- Operational inputs on termination:
- \nothing
- Sure outputs:
- j
[inout] Out (internal) for function main_local:
p; q
[inout] Inputs for function main_local:
@@ -803,319 +801,532 @@ tests/non-free/memcpy.c:230:[value] entering loop for the first time
Sure outputs:
ANYTHING(origin:Unknown)
[report] Computing properties status...
-
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_make_unknown'
+--- Global Properties
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 36)
+[ Extern ] Axiom 'memchr_def'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 34)
+[ Extern ] Axiom 'memcmp_strlen_left'
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 34)
+[ Extern ] Axiom 'memcmp_strlen_right'
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 35)
+[ Extern ] Axiom 'memcmp_strlen_shift_left'
Unverifiable but considered Valid.
-[ Valid ] Default behavior
+[ Extern ] Axiom 'memcmp_strlen_shift_right'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'memcmp_zero'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'memset_def'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strchr_def'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strcmp_zero'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strlen_at_null'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strlen_before_null'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strlen_create'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strlen_create_shift'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strlen_neg'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strlen_not_zero'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strlen_pos_or_null'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strlen_shift'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strlen_sup'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strlen_zero'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'strncmp_zero'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcscmp_zero'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcslen_at_null'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcslen_before_null'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcslen_create'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcslen_create_shift'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcslen_neg'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcslen_not_zero'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcslen_pos_or_null'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcslen_shift'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcslen_sup'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcslen_zero'
+ Unverifiable but considered Valid.
+[ Extern ] Axiom 'wcsncmp_zero'
+ Unverifiable but considered Valid.
+[ Valid ] Axiomatic 'MemChr'
+ by Frama-C kernel.
+[ Valid ] Axiomatic 'MemCmp'
+ by Frama-C kernel.
+[ Valid ] Axiomatic 'MemSet'
+ by Frama-C kernel.
+[ Valid ] Axiomatic 'StrChr'
+ by Frama-C kernel.
+[ Valid ] Axiomatic 'StrCmp'
+ by Frama-C kernel.
+[ Valid ] Axiomatic 'StrLen'
+ by Frama-C kernel.
+[ Valid ] Axiomatic 'StrNCmp'
+ by Frama-C kernel.
+[ Valid ] Axiomatic 'WcsCmp'
+ by Frama-C kernel.
+[ Valid ] Axiomatic 'WcsLen'
+ by Frama-C kernel.
+[ Valid ] Axiomatic 'WcsNCmp'
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_nondet'
+--- Properties of Function 'memcmp'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 42)
- Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 40)
+[ Extern ] Post-condition (file share/libc/string.h, line 39)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 40)
+[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 41)
+[ Extern ] Froms (file share/libc/string.h, line 38)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_nondet_ptr'
+--- Properties of Function 'memchr'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 48)
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 47)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 48)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 46)
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 49)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 46)
+[ Extern ] Post-condition for 'not_found' (file share/libc/string.h, line 54)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 47)
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 44)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
+[ Valid ] Behavior 'found'
+ by Frama-C kernel.
+[ Valid ] Behavior 'not_found'
+ by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_interval'
+--- Properties of Function 'memcpy'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 55)
+[ Extern ] Post-condition (file share/libc/string.h, line 65)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition (file share/libc/string.h, line 66)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 53)
+[ Extern ] Assigns (file share/libc/string.h, line 63)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 53)
+[ Extern ] Froms (file share/libc/string.h, line 63)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 54)
+[ Extern ] Froms (file share/libc/string.h, line 64)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_interval_split'
+--- Properties of Function 'memmove'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 62)
+[ Extern ] Post-condition (file share/libc/string.h, line 75)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition (file share/libc/string.h, line 76)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 60)
+[ Extern ] Assigns (file share/libc/string.h, line 73)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 60)
+[ Extern ] Froms (file share/libc/string.h, line 73)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 61)
+[ Extern ] Froms (file share/libc/string.h, line 74)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_unsigned_char_interval'
+--- Properties of Function 'memset'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 69)
+[ Extern ] Post-condition (file share/libc/string.h, line 85)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 67)
+[ Extern ] Post-condition (file share/libc/string.h, line 86)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 67)
+[ Extern ] Assigns (file share/libc/string.h, line 83)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 68)
+[ Extern ] Froms (file share/libc/string.h, line 83)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 84)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_char_interval'
+--- Properties of Function 'strlen'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 77)
- Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 75)
+[ Extern ] Post-condition (file share/libc/string.h, line 94)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 75)
+[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 76)
+[ Extern ] Froms (file share/libc/string.h, line 93)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_unsigned_short_interval'
+--- Properties of Function 'strnlen'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 84)
+[ Extern ] Post-condition (file share/libc/string.h, line 100)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 82)
+[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 82)
+[ Extern ] Froms (file share/libc/string.h, line 99)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 83)
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'strcmp'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition (file share/libc/string.h, line 107)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 106)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_short_interval'
+--- Properties of Function 'strncmp'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 91)
+[ Extern ] Post-condition (file share/libc/string.h, line 114)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 89)
+[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 89)
+[ Extern ] Froms (file share/libc/string.h, line 113)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 90)
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'strcoll'
+--------------------------------------------------------------------------------
+
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 120)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_unsigned_int_interval'
+--- Properties of Function 'strchr'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 99)
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 128)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 129)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 97)
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 130)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 97)
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 131)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 98)
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 132)
Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'not_found' (file share/libc/string.h, line 135)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'default' (file share/libc/string.h, line 137)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 125)
+ Unverifiable but considered Valid.
+[ Valid ] Behavior 'default'
+ by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
+[ Valid ] Behavior 'found'
+ by Frama-C kernel.
+[ Valid ] Behavior 'not_found'
+ by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_int_interval'
+--- Properties of Function 'strrchr'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 106)
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 145)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 104)
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 146)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 104)
+[ Extern ] Post-condition for 'found' (file share/libc/string.h, line 147)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 105)
+[ Extern ] Post-condition for 'not_found' (file share/libc/string.h, line 150)
Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'default' (file share/libc/string.h, line 152)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 142)
+ Unverifiable but considered Valid.
+[ Valid ] Behavior 'default'
+ by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
+[ Valid ] Behavior 'found'
+ by Frama-C kernel.
+[ Valid ] Behavior 'not_found'
+ by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_unsigned_long_interval'
+--- Properties of Function 'strcspn'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 114)
- Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 112)
+[ Extern ] Post-condition (file share/libc/string.h, line 159)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 112)
+[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 113)
+[ Extern ] Froms (file share/libc/string.h, line 158)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_long_interval'
+--- Properties of Function 'strspn'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 122)
+[ Extern ] Post-condition (file share/libc/string.h, line 166)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 120)
+[ Extern ] Froms (file share/libc/string.h, line 165)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 120)
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'strpbrk'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition (file share/libc/string.h, line 173)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 121)
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 172)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_unsigned_long_long_interval'
+--- Properties of Function 'strstr'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 130)
+[ Extern ] Post-condition (file share/libc/string.h, line 181)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 128)
+[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 128)
+[ Extern ] Froms (file share/libc/string.h, line 179)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 129)
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'strtok'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition (file share/libc/string.h, line 201)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 200)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_long_long_interval'
+--- Properties of Function 'strsep'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 138)
+[ Extern ] Assigns (file share/libc/string.h, line 208)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 208)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 209)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 136)
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'strerror'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition (file share/libc/string.h, line 215)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 136)
+[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 137)
+[ Extern ] Froms (file share/libc/string.h, line 214)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_size_t_interval'
+--- Properties of Function 'strcpy'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 145)
+[ Extern ] Post-condition (file share/libc/string.h, line 227)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition (file share/libc/string.h, line 228)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 143)
+[ Extern ] Assigns (file share/libc/string.h, line 225)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 143)
+[ Extern ] Froms (file share/libc/string.h, line 225)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 144)
+[ Extern ] Froms (file share/libc/string.h, line 226)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_float_interval'
+--- Properties of Function 'strncpy'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 153)
+[ Extern ] Post-condition (file share/libc/string.h, line 237)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 151)
+[ Extern ] Post-condition (file share/libc/string.h, line 238)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 151)
+[ Extern ] Post-condition for 'complete' (file share/libc/string.h, line 241)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 152)
+[ Extern ] Post-condition for 'partial' (file share/libc/string.h, line 244)
Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/string.h, line 235)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 235)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 236)
+ Unverifiable but considered Valid.
+[ Valid ] Behavior 'complete'
+ by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
+[ Valid ] Behavior 'partial'
+ by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_double_interval'
+--- Properties of Function 'strcat'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file share/libc/__fc_builtin.h, line 161)
+[ Extern ] Post-condition (file share/libc/string.h, line 269)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 159)
+[ Extern ] Post-condition (file share/libc/string.h, line 271)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 159)
+[ Extern ] Assigns (file share/libc/string.h, line 267)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 160)
+[ Extern ] Froms (file share/libc/string.h, line 267)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 270)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_memcpy'
+--- Properties of Function 'strncat'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 166)
+[ Extern ] Post-condition (file share/libc/string.h, line 280)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'complete' (file share/libc/string.h, line 287)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'partial' (file share/libc/string.h, line 294)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'complete' (file share/libc/string.h, line 284)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/string.h, line 278)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 291)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 166)
+[ Extern ] Froms for 'complete' (file share/libc/string.h, line 284)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 167)
+[ Extern ] Froms for 'complete' (file share/libc/string.h, line 286)
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 278)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 279)
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'partial' (file share/libc/string.h, line 291)
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'partial' (file share/libc/string.h, line 293)
+ Unverifiable but considered Valid.
+[ Valid ] Behavior 'complete'
+ by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
+[ Valid ] Behavior 'partial'
+ by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_memset'
+--- Properties of Function 'strxfrm'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/__fc_builtin.h, line 171)
+[ Extern ] Assigns (file share/libc/string.h, line 300)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 171)
+[ Extern ] Froms (file share/libc/string.h, line 300)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 171)
+[ Extern ] Froms (file share/libc/string.h, line 301)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_abort'
+--- Properties of Function 'strdup'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition (file share/libc/string.h, line 310)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'Frama_C_offset'
+--- Properties of Function 'strndup'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition (file share/libc/string.h, line 316)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/__fc_builtin.h, line 180)
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'bzero'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition (file share/libc/strings.h, line 37)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/strings.h, line 36)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/strings.h, line 36)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1250,9 +1461,9 @@ tests/non-free/memcpy.c:230:[value] entering loop for the first time
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 35 Completely validated
+ 62 Completely validated
1 Locally validated
- 87 Considered valid
+ 152 Considered valid
26 To be validated
- 149 Total
+ 241 Total
--------------------------------------------------------------------------------
diff --git a/tests/non-free/oracle/memcpy2.res.oracle b/tests/non-free/oracle/memcpy2.res.oracle
index 21b8087fab9..b6080423a77 100644
--- a/tests/non-free/oracle/memcpy2.res.oracle
+++ b/tests/non-free/oracle/memcpy2.res.oracle
@@ -48,15 +48,15 @@ tests/non-free/memcpy2.c:18:[value] Call to builtin memcpy(({{ (void *)&t }},{{
[from] Computing for function main
[from] Computing for function Frama_C_interval <-main
[from] Done for function Frama_C_interval
-[from] Computing for function Frama_C_memcpy <-main
-[from] Done for function Frama_C_memcpy
+[from] Computing for function memcpy <-main
+[from] Done for function memcpy
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
-[from] Function Frama_C_memcpy:
+[from] Function memcpy:
t[0..511] FROM s[0..511] (and SELF)
\result FROM dest
[from] Function main:
diff --git a/tests/non-free/oracle/memcpy_invalid.res.oracle b/tests/non-free/oracle/memcpy_invalid.res.oracle
index d84de30ae69..fee106543e8 100644
--- a/tests/non-free/oracle/memcpy_invalid.res.oracle
+++ b/tests/non-free/oracle/memcpy_invalid.res.oracle
@@ -1,36 +1,42 @@
-[kernel] Parsing tests/non-free/memcpy_invalid.i (no preprocessing)
+[kernel] Parsing tests/non-free/memcpy_invalid.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
[value] computing for function test <- main.
- Called from tests/non-free/memcpy_invalid.i:22.
+ Called from tests/non-free/memcpy_invalid.c:22.
[value] computing for function Frama_C_interval <- test <- main.
- Called from tests/non-free/memcpy_invalid.i:16.
+ Called from tests/non-free/memcpy_invalid.c:16.
[value] using specification for function Frama_C_interval
[value] Done for function Frama_C_interval
-tests/non-free/memcpy_invalid.i:17:[value] Call to builtin memcpy(({{ (void *)&dst }},
+tests/non-free/memcpy_invalid.c:17:[value] Call to builtin memcpy(({{ (void *)&dst }},
{{ &src + {0; 2; 4; 6; 8; 10; 12; 14} }},
{1; 4294967283; 4294967285; 4294967287; 4294967289;
4294967291; 4294967293; 4294967295}))
-tests/non-free/memcpy_invalid.i:17:[value] warning: out of bounds read.
+tests/non-free/memcpy_invalid.c:17:[value] warning: out of bounds read.
assert
\valid_read((&src + i) +
- (0 .. (unsigned long)((unsigned long)sizeof(src) - i) - 1));
-tests/non-free/memcpy_invalid.i:17:[value] warning: out of bounds write.
+ (0 ..
+ (unsigned int)((unsigned long)((unsigned long)sizeof(src) -
+ i))
+ - 1));
+tests/non-free/memcpy_invalid.c:17:[value] warning: out of bounds write.
assert
- \valid(&dst + (0 .. (unsigned long)((unsigned long)sizeof(src) - i) - 1));
+ \valid(&dst +
+ (0 ..
+ (unsigned int)((unsigned long)((unsigned long)sizeof(src) - i)) -
+ 1));
[value] Recording results for test
[from] Computing for function test
[from] Done for function test
[value] Done for function test
[value] computing for function test <- main.
- Called from tests/non-free/memcpy_invalid.i:23.
+ Called from tests/non-free/memcpy_invalid.c:23.
[value] computing for function Frama_C_interval <- test <- main.
- Called from tests/non-free/memcpy_invalid.i:16.
+ Called from tests/non-free/memcpy_invalid.c:16.
[value] Done for function Frama_C_interval
-tests/non-free/memcpy_invalid.i:17:[value] Call to builtin memcpy(({{ (void *)&dst }},{{ &src + [0..16],0%2 }},
+tests/non-free/memcpy_invalid.c:17:[value] Call to builtin memcpy(({{ (void *)&dst }},{{ &src + [0..16],0%2 }},
[1..4294967295],1%2))
[value] Recording results for test
[from] Computing for function test
@@ -48,14 +54,14 @@ tests/non-free/memcpy_invalid.i:17:[value] Call to builtin memcpy(({{ (void *)&d
[value:final-states] Values at end of function main:
__retres ∈ {0}
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to Frama_C_interval at tests/non-free/memcpy_invalid.i:16 (by test):
+[from] call to Frama_C_interval at tests/non-free/memcpy_invalid.c:16 (by test):
\result FROM min; max
-[from] call to memcpy at tests/non-free/memcpy_invalid.i:17 (by test):
+[from] call to memcpy at tests/non-free/memcpy_invalid.c:17 (by test):
dst FROM src
- \result FROM dst
-[from] call to test at tests/non-free/memcpy_invalid.i:22 (by main):
+ \result FROM dest
+[from] call to test at tests/non-free/memcpy_invalid.c:22 (by main):
NO EFFECTS
-[from] call to test at tests/non-free/memcpy_invalid.i:23 (by main):
+[from] call to test at tests/non-free/memcpy_invalid.c:23 (by main):
NO EFFECTS
[from] entry point:
\result FROM \nothing
diff --git a/tests/non-free/oracle/memset.res.oracle b/tests/non-free/oracle/memset.res.oracle
index 8a3852f6ed9..ed345e1d479 100644
--- a/tests/non-free/oracle/memset.res.oracle
+++ b/tests/non-free/oracle/memset.res.oracle
@@ -1,5 +1,5 @@
-[kernel] Parsing tests/non-free/memset.i (no preprocessing)
-tests/non-free/memset.i:46:[kernel] warning: A.QUESTION: char * does not match int * (different integer types:
+[kernel] Parsing tests/non-free/memset.c (with preprocessing)
+tests/non-free/memset.c:46:[kernel] warning: A.QUESTION: char * does not match int * (different integer types:
'char' and 'int')
[value] Analyzing a complete application starting at main
[value] Computing initial state
@@ -19,50 +19,50 @@ tests/non-free/memset.i:46:[kernel] warning: A.QUESTION: char * does not match i
t12[0..99] ∈ {0}
ts[0..4] ∈ {0}
vol ∈ [--..--]
-tests/non-free/memset.i:33:[value] Call to builtin memset(({{ (void *)&t1 }},{17},{400}))
-tests/non-free/memset.i:34:[value] Call to builtin memset(({{ garbled mix of &{t2}
- (origin: Arithmetic {tests/non-free/memset.i:34}) }},
+tests/non-free/memset.c:33:[value] Call to builtin memset(({{ (void *)&t1 }},{17},{400}))
+tests/non-free/memset.c:34:[value] Call to builtin memset(({{ garbled mix of &{t2}
+ (origin: Arithmetic {tests/non-free/memset.c:34}) }},
{18},{400}))
-tests/non-free/memset.i:34:[value] warning: out of bounds write.
- assert
- \valid((char *)(&t2[(int)((int *)t2)]) + (0 .. (unsigned long)sizeof(t2) - 1));
-tests/non-free/memset.i:34:[value:imprecision] Call to builtin precise_memset(({{ garbled mix of &{t2}
+tests/non-free/memset.c:34:[value] warning: out of bounds write.
+ assert \valid((char *)(&t2[(int)((int *)t2)]) + (0 .. sizeof(t2) - 1));
+tests/non-free/memset.c:34:[value:imprecision] Call to builtin precise_memset(({{ garbled mix of &{t2}
(origin: Arithmetic
- {tests/non-free/memset.i:34}) }},{18},
+ {tests/non-free/memset.c:34}) }},{18},
{400})) failed; destination is not exact
-tests/non-free/memset.i:35:[value] Call to builtin memset(({{ (void *)&t3[10] }},{17},{{ (unsigned long)&t1 }}))
-tests/non-free/memset.i:35:[value] warning: out of bounds write.
- assert \valid((char *)(&t3[10]) + (0 .. (unsigned long)((int *)t1) - 1));
-tests/non-free/memset.i:35:[value:imprecision] Call to builtin precise_memset(({{ (void *)&t3[10] }},{17},
- {{ (unsigned long)&t1 }})) failed; size is imprecise
-tests/non-free/memset.i:38:[value] Call to builtin memset(({{ (void *)&t4[1] }},{1},{400}))
-tests/non-free/memset.i:38:[value] warning: out of bounds write.
- assert \valid((char *)(&t4[1]) + (0 .. (unsigned long)sizeof(t4) - 1));
-tests/non-free/memset.i:41:[value] Call to builtin memset(({{ (void *)&t5 }},{{ (int)&t1 }},{400}))
-tests/non-free/memset.i:41:[value:imprecision] Call to builtin precise_memset(({{ (void *)&t5 }},{{ (int)&t1 }},{400})) failed; value to write is imprecise
-tests/non-free/memset.i:44:[value] Call to builtin memset(({{ (void *)&t6[10] ; (void *)&t7 }},{34},{16}))
-tests/non-free/memset.i:44:[value:imprecision] Call to builtin precise_memset(({{ (void *)&t6[10] ; (void *)&t7 }},{34},
+tests/non-free/memset.c:35:[value] Call to builtin memset(({{ (void *)&t3[10] }},{17},{{ (unsigned int)&t1 }}))
+tests/non-free/memset.c:35:[value] warning: out of bounds write.
+ assert
+ \valid((char *)(&t3[10]) +
+ (0 .. (unsigned int)((unsigned long)((int *)t1)) - 1));
+tests/non-free/memset.c:35:[value:imprecision] Call to builtin precise_memset(({{ (void *)&t3[10] }},{17},
+ {{ (unsigned int)&t1 }})) failed; size is imprecise
+tests/non-free/memset.c:38:[value] Call to builtin memset(({{ (void *)&t4[1] }},{1},{400}))
+tests/non-free/memset.c:38:[value] warning: out of bounds write. assert \valid((char *)(&t4[1]) + (0 .. sizeof(t4) - 1));
+tests/non-free/memset.c:41:[value] Call to builtin memset(({{ (void *)&t5 }},{{ (int)&t1 }},{400}))
+tests/non-free/memset.c:41:[value:imprecision] Call to builtin precise_memset(({{ (void *)&t5 }},{{ (int)&t1 }},{400})) failed; value to write is imprecise
+tests/non-free/memset.c:44:[value] Call to builtin memset(({{ (void *)&t6[10] ; (void *)&t7 }},{34},{16}))
+tests/non-free/memset.c:44:[value:imprecision] Call to builtin precise_memset(({{ (void *)&t6[10] ; (void *)&t7 }},{34},
{16})) failed; destination is not exact
-tests/non-free/memset.i:47:[value] Call to builtin memset(({{ NULL ; (void *)&t8 }},{34},{16}))
-tests/non-free/memset.i:47:[value] warning: out of bounds write. assert \valid((char *)p + (0 .. (unsigned long)16 - 1));
-tests/non-free/memset.i:47:[value:imprecision] Call to builtin precise_memset(({{ NULL ; (void *)&t8 }},{34},{16})) failed; destination is not exact
-tests/non-free/memset.i:50:[value] entering loop for the first time
-tests/non-free/memset.i:54:[value] Call to builtin memset(({{ &t9 + [80..--],0%4 }},{2302},{4}))
-tests/non-free/memset.i:54:[value] warning: out of bounds write. assert \valid((char *)p + (0 .. (unsigned long)4 - 1));
-tests/non-free/memset.i:54:[value:imprecision] Call to builtin precise_memset(({{ &t9 + [80..--],0%4 }},{2302},{4})) failed; destination is not exact
-tests/non-free/memset.i:58:[value] Call to builtin memset(({{ (void *)&t10[4] }},{136},{12; 36}))
-tests/non-free/memset.i:58:[value:imprecision] Call to builtin precise_memset(({{ (void *)&t10[4] }},{136},{12; 36})) failed; size is imprecise
-tests/non-free/memset.i:65:[value] Call to builtin memset(({{ (void *)&t11{[2], [3]} }},{153},{8; 16}))
-tests/non-free/memset.i:65:[value:imprecision] Call to builtin precise_memset(({{ (void *)&t11{[2], [3]} }},{153},{8; 16})) failed; size is imprecise
-tests/non-free/memset.i:68:[value] Call to builtin memset(({{ (void *)&ts }},{254},{100}))
-tests/non-free/memset.i:71:[value] warning: assertion 'Assume' got status unknown.
-tests/non-free/memset.i:72:[value] Call to builtin memset(({{ &t12 + [0..384],0%32 }},{1},{4}))
-tests/non-free/memset.i:72:[value:imprecision] Call to builtin precise_memset(({{ &t12 + [0..384],0%32 }},{1},{4})) failed; destination is not exact
+tests/non-free/memset.c:47:[value] Call to builtin memset(({{ NULL ; (void *)&t8 }},{34},{16}))
+tests/non-free/memset.c:47:[value] warning: out of bounds write. assert \valid((char *)p + (0 .. (unsigned int)16 - 1));
+tests/non-free/memset.c:47:[value:imprecision] Call to builtin precise_memset(({{ NULL ; (void *)&t8 }},{34},{16})) failed; destination is not exact
+tests/non-free/memset.c:50:[value] entering loop for the first time
+tests/non-free/memset.c:54:[value] Call to builtin memset(({{ &t9 + [80..--],0%4 }},{2302},{4}))
+tests/non-free/memset.c:54:[value] warning: out of bounds write. assert \valid((char *)p + (0 .. (unsigned int)4 - 1));
+tests/non-free/memset.c:54:[value:imprecision] Call to builtin precise_memset(({{ &t9 + [80..--],0%4 }},{2302},{4})) failed; destination is not exact
+tests/non-free/memset.c:58:[value] Call to builtin memset(({{ (void *)&t10[4] }},{136},{12; 36}))
+tests/non-free/memset.c:58:[value:imprecision] Call to builtin precise_memset(({{ (void *)&t10[4] }},{136},{12; 36})) failed; size is imprecise
+tests/non-free/memset.c:65:[value] Call to builtin memset(({{ (void *)&t11{[2], [3]} }},{153},{8; 16}))
+tests/non-free/memset.c:65:[value:imprecision] Call to builtin precise_memset(({{ (void *)&t11{[2], [3]} }},{153},{8; 16})) failed; size is imprecise
+tests/non-free/memset.c:68:[value] Call to builtin memset(({{ (void *)&ts }},{254},{100}))
+tests/non-free/memset.c:71:[value] warning: assertion 'Assume' got status unknown.
+tests/non-free/memset.c:72:[value] Call to builtin memset(({{ &t12 + [0..384],0%32 }},{1},{4}))
+tests/non-free/memset.c:72:[value:imprecision] Call to builtin precise_memset(({{ &t12 + [0..384],0%32 }},{1},{4})) failed; destination is not exact
[value] Recording results for main
[from] Computing for function main
[from] Done for function main
[value] done for function main
-tests/non-free/memset.i:38:[value] assertion 'Value,logic_mem_access' got final status invalid.
+tests/non-free/memset.c:38:[value] assertion 'Value,logic_mem_access' got final status invalid.
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
t1[0..99] ∈ {286331153}
@@ -71,7 +71,7 @@ tests/non-free/memset.i:38:[value] assertion 'Value,logic_mem_access' got final
[10..99]# ∈ {0; 17} repeated %8
t5[0..99] ∈
{{ garbled mix of &{t1}
- (origin: Misaligned {tests/non-free/memset.i:41}) }}
+ (origin: Misaligned {tests/non-free/memset.c:41}) }}
t6[0..9] ∈ {0}
[10..13]# ∈ {0; 34} repeated %8
[14..99] ∈ {0}
@@ -118,44 +118,44 @@ tests/non-free/memset.i:38:[value] assertion 'Value,logic_mem_access' got final
s1 ∈ {8; 16}
k ∈ [0..12]
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to Frama_C_memset at tests/non-free/memset.i:33 (by main):
- t1[0..99] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:34 (by main):
- t2[0..99] FROM v (and SELF)
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:35 (by main):
- t3[10..99] FROM v (and SELF)
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:38 (by main):
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:41 (by main):
- t5[0..99] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:44 (by main):
- t6[10..13] FROM v (and SELF)
- t7[0..3] FROM v (and SELF)
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:47 (by main):
- t8[0..3] FROM v (and SELF)
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:54 (by main):
- t9[20..99] FROM v (and SELF)
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:58 (by main):
- t10[4..6] FROM v
- [7..12] FROM v (and SELF)
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:65 (by main):
- t11{[2]; [4..6]} FROM v (and SELF)
- [3] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:68 (by main):
- ts[0..4] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/memset.i:72 (by main):
- t12[0..96] FROM v (and SELF)
- \result FROM dst
+[from] call to memset at tests/non-free/memset.c:33 (by main):
+ t1[0..99] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:34 (by main):
+ t2[0..99] FROM c (and SELF)
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:35 (by main):
+ t3[10..99] FROM c (and SELF)
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:38 (by main):
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:41 (by main):
+ t5[0..99] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:44 (by main):
+ t6[10..13] FROM c (and SELF)
+ t7[0..3] FROM c (and SELF)
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:47 (by main):
+ t8[0..3] FROM c (and SELF)
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:54 (by main):
+ t9[20..99] FROM c (and SELF)
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:58 (by main):
+ t10[4..6] FROM c
+ [7..12] FROM c (and SELF)
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:65 (by main):
+ t11{[2]; [4..6]} FROM c (and SELF)
+ [3] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:68 (by main):
+ ts[0..4] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/memset.c:72 (by main):
+ t12[0..96] FROM c (and SELF)
+ \result FROM s
[from] entry point:
t1[0..99] FROM \nothing
t2[0..99] FROM \nothing (and SELF)
diff --git a/tests/non-free/oracle/precise_memset.res.oracle b/tests/non-free/oracle/precise_memset.res.oracle
index baa0aa1773d..61e324f6663 100644
--- a/tests/non-free/oracle/precise_memset.res.oracle
+++ b/tests/non-free/oracle/precise_memset.res.oracle
@@ -116,28 +116,28 @@ tests/non-free/precise_memset.c:92:[value] Call to builtin memset(({{ (void *)&t
t_s[0..1023] ∈ {4883}
n ∈ {1; 2; 3; 4; 5; 6; 7; 8}
[from] Computing for function main
-[from] Computing for function Frama_C_memset <-main
-[from] Done for function Frama_C_memset
+[from] Computing for function memset <-main
+[from] Done for function memset
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_memset:
- x FROM v; size (and SELF)
- t[0..49] FROM v; size (and SELF)
- u[0..11] FROM v; size (and SELF)
- f FROM v; size (and SELF)
- fnan FROM v; size (and SELF)
- d FROM v; size (and SELF)
- dnan FROM v; size (and SELF)
- w1[0..3] FROM v; size (and SELF)
- w2[0..3] FROM v; size (and SELF)
- bitf FROM v; size (and SELF)
- tone[0] FROM v; size (and SELF)
- vs FROM v; size (and SELF)
- vv FROM v; size (and SELF)
- t_b[0..1023] FROM v; size (and SELF)
- t_s[0..1023] FROM v; size (and SELF)
- \result FROM dst
+[from] Function memset:
+ x FROM c (and SELF)
+ t[0..49] FROM c (and SELF)
+ u[0..11] FROM c (and SELF)
+ f FROM c (and SELF)
+ fnan FROM c (and SELF)
+ d FROM c (and SELF)
+ dnan FROM c (and SELF)
+ w1[0..3] FROM c (and SELF)
+ w2[0..3] FROM c (and SELF)
+ bitf FROM c (and SELF)
+ tone[0] FROM c (and SELF)
+ vs FROM c (and SELF)
+ vv FROM c (and SELF)
+ t_b[0..1023] FROM c (and SELF)
+ t_s[0..1023] FROM c (and SELF)
+ \result FROM s
[from] Function main:
x FROM v (and SELF)
t[0..49] FROM v (and SELF)
@@ -156,57 +156,57 @@ tests/non-free/precise_memset.c:92:[value] Call to builtin memset(({{ (void *)&t
t_s[0..1023] FROM v (and SELF)
[from] ====== END OF DEPENDENCIES ======
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:72 (by main):
- x FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:73 (by main):
- t[0..49] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:74 (by main):
- u[0..11] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:75 (by main):
- f FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:76 (by main):
- fnan FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:77 (by main):
- d FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:78 (by main):
- dnan FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:79 (by main):
- w1[0..3] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:80 (by main):
- bitf FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:81 (by main):
- tone[0] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:85 (by main):
- w2[0..3] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:87 (by main):
- vs.c2 FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:88 (by main):
- vs.t[0..9] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:89 (by main):
- vv.c3.s FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:90 (by main):
- t[15..34] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:91 (by main):
- t_b[0..1023] FROM v
- \result FROM dst
-[from] call to Frama_C_memset at tests/non-free/precise_memset.c:92 (by main):
- t_s[0..1023] FROM v
- \result FROM dst
+[from] call to memset at tests/non-free/precise_memset.c:72 (by main):
+ x FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:73 (by main):
+ t[0..49] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:74 (by main):
+ u[0..11] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:75 (by main):
+ f FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:76 (by main):
+ fnan FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:77 (by main):
+ d FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:78 (by main):
+ dnan FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:79 (by main):
+ w1[0..3] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:80 (by main):
+ bitf FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:81 (by main):
+ tone[0] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:85 (by main):
+ w2[0..3] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:87 (by main):
+ vs.c2 FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:88 (by main):
+ vs.t[0..9] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:89 (by main):
+ vv.c3.s FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:90 (by main):
+ t[15..34] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:91 (by main):
+ t_b[0..1023] FROM c
+ \result FROM s
+[from] call to memset at tests/non-free/precise_memset.c:92 (by main):
+ t_s[0..1023] FROM c
+ \result FROM s
[from] entry point:
x FROM \nothing
t[0..49] FROM \nothing
diff --git a/tests/non-free/oracle/strchr.res.oracle b/tests/non-free/oracle/strchr.res.oracle
index 667e4d0906d..7c0b278c497 100644
--- a/tests/non-free/oracle/strchr.res.oracle
+++ b/tests/non-free/oracle/strchr.res.oracle
@@ -24,6 +24,8 @@
[value] computing for function my_strchr <- strchr_small_sets <- main.
Called from tests/non-free/strchr.c:79.
tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ "abc" + {0; 1} }},{0}))
+share/libc/string.h:127:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic function strchr
+share/libc/string.h:134:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic function strchr
tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {3}
[value] Recording results for my_strchr
[value] Done for function my_strchr
@@ -605,21 +607,14 @@ tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ "b\000c" +
tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {-1}
[value] Recording results for my_strchr
[value] Done for function my_strchr
-[value] computing for function my_strchr <- strchr_small_sets_no_assertions <-
- strchr_small_sets_chars <- main.
- Called from tests/non-free/strchr.c:447.
-tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ &t[0] }},{97}))
-tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {0; 1}
-[value] Recording results for my_strchr
-[value] Done for function my_strchr
[value] Recording results for strchr_small_sets_no_assertions
[value] Done for function strchr_small_sets_no_assertions
-tests/non-free/strchr.c:457:[value] Frama_C_show_each_res: {-1; 0}, {-1}, {-1}, {-1}, {0; 1}
+tests/non-free/strchr.c:457:[value] Frama_C_show_each_res: {-1; 0}, {-1}, {-1}, {-1}, Bottom
tests/non-free/strchr.c:458:[value] assertion got status valid.
tests/non-free/strchr.c:459:[value] assertion got status valid.
tests/non-free/strchr.c:460:[value] assertion got status valid.
tests/non-free/strchr.c:461:[value] assertion got status valid.
-tests/non-free/strchr.c:462:[value] assertion got status valid.
+tests/non-free/strchr.c:462:[value] warning: assertion got status unknown.
[value] computing for function strchr_small_sets_no_assertions <-
strchr_small_sets_chars <- main.
Called from tests/non-free/strchr.c:465.
@@ -651,21 +646,14 @@ tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ "b\000c" +
tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {-1; 0}
[value] Recording results for my_strchr
[value] Done for function my_strchr
-[value] computing for function my_strchr <- strchr_small_sets_no_assertions <-
- strchr_small_sets_chars <- main.
- Called from tests/non-free/strchr.c:447.
-tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ &t[0] }},{98}))
-tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {0; 1}
-[value] Recording results for my_strchr
-[value] Done for function my_strchr
[value] Recording results for strchr_small_sets_no_assertions
[value] Done for function strchr_small_sets_no_assertions
-tests/non-free/strchr.c:466:[value] Frama_C_show_each_res: {1}, {-1; 1}, {-1}, {-1; 0}, {0; 1}
+tests/non-free/strchr.c:466:[value] Frama_C_show_each_res: {1}, {-1; 1}, {-1}, {-1; 0}, Bottom
tests/non-free/strchr.c:467:[value] assertion got status valid.
tests/non-free/strchr.c:468:[value] assertion got status valid.
tests/non-free/strchr.c:469:[value] assertion got status valid.
tests/non-free/strchr.c:470:[value] assertion got status valid.
-tests/non-free/strchr.c:471:[value] assertion got status valid.
+tests/non-free/strchr.c:471:[value] warning: assertion got status unknown.
tests/non-free/strchr.c:474:[value] Frama_C_show_each_c: {97; 98}
[value] computing for function strchr_small_sets_no_assertions <-
strchr_small_sets_chars <- main.
@@ -698,21 +686,14 @@ tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ "b\000c" +
tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {-1; 0}
[value] Recording results for my_strchr
[value] Done for function my_strchr
-[value] computing for function my_strchr <- strchr_small_sets_no_assertions <-
- strchr_small_sets_chars <- main.
- Called from tests/non-free/strchr.c:447.
-tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ &t[0] }},{97; 98}))
-tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {0; 1}
-[value] Recording results for my_strchr
-[value] Done for function my_strchr
[value] Recording results for strchr_small_sets_no_assertions
[value] Done for function strchr_small_sets_no_assertions
-tests/non-free/strchr.c:476:[value] Frama_C_show_each_res: {-1; 0; 1}, {-1; 1}, {-1}, {-1; 0}, {0; 1}
+tests/non-free/strchr.c:476:[value] Frama_C_show_each_res: {-1; 0; 1}, {-1; 1}, {-1}, {-1; 0}, Bottom
tests/non-free/strchr.c:478:[value] assertion got status valid.
tests/non-free/strchr.c:479:[value] assertion got status valid.
tests/non-free/strchr.c:480:[value] assertion got status valid.
tests/non-free/strchr.c:481:[value] assertion got status valid.
-tests/non-free/strchr.c:482:[value] assertion got status valid.
+tests/non-free/strchr.c:482:[value] warning: assertion got status unknown.
tests/non-free/strchr.c:485:[value] Frama_C_show_each_c: {98; 99}
[value] computing for function strchr_small_sets_no_assertions <-
strchr_small_sets_chars <- main.
@@ -745,22 +726,15 @@ tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ "b\000c" +
tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {-1; 0; 2}
[value] Recording results for my_strchr
[value] Done for function my_strchr
-[value] computing for function my_strchr <- strchr_small_sets_no_assertions <-
- strchr_small_sets_chars <- main.
- Called from tests/non-free/strchr.c:447.
-tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ &t[0] }},{98; 99}))
-tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {0; 1}
-[value] Recording results for my_strchr
-[value] Done for function my_strchr
[value] Recording results for strchr_small_sets_no_assertions
[value] Done for function strchr_small_sets_no_assertions
-tests/non-free/strchr.c:487:[value] Frama_C_show_each_res: {-1; 1; 2}, {-1; 1; 2}, {-1}, {-1; 0; 2}, {0; 1}
+tests/non-free/strchr.c:487:[value] Frama_C_show_each_res: {-1; 1; 2}, {-1; 1; 2}, {-1}, {-1; 0; 2}, Bottom
tests/non-free/strchr.c:488:[value] assertion got status valid.
tests/non-free/strchr.c:489:[value] warning: assertion 'refined' got status unknown.
tests/non-free/strchr.c:490:[value] assertion got status valid.
tests/non-free/strchr.c:491:[value] assertion got status valid.
tests/non-free/strchr.c:492:[value] assertion got status valid.
-tests/non-free/strchr.c:493:[value] assertion got status valid.
+tests/non-free/strchr.c:493:[value] warning: assertion got status unknown.
tests/non-free/strchr.c:496:[value] Frama_C_show_each_c: {0; 98; 99}
[value] computing for function strchr_small_sets_no_assertions <-
strchr_small_sets_chars <- main.
@@ -793,23 +767,16 @@ tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ "b\000c" +
tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {-1; 0; 1; 2; 3}
[value] Recording results for my_strchr
[value] Done for function my_strchr
-[value] computing for function my_strchr <- strchr_small_sets_no_assertions <-
- strchr_small_sets_chars <- main.
- Called from tests/non-free/strchr.c:447.
-tests/non-free/strchr.c:49:[value] Call to builtin Frama_C_strchr(({{ &t[0] }},{0; 98; 99}))
-tests/non-free/strchr.c:56:[value] Frama_C_show_each_mystrchr: {-1; 0; 1}
-[value] Recording results for my_strchr
-[value] Done for function my_strchr
[value] Recording results for strchr_small_sets_no_assertions
[value] Done for function strchr_small_sets_no_assertions
tests/non-free/strchr.c:498:[value] Frama_C_show_each_res:
- {-1; 1; 2; 3}, {-1; 0; 1; 2; 3}, {-1; 0}, {-1; 0; 1; 2; 3}, {-1; 0; 1}
+ {-1; 1; 2; 3}, {-1; 0; 1; 2; 3}, {-1; 0}, {-1; 0; 1; 2; 3}, Bottom
tests/non-free/strchr.c:499:[value] assertion got status valid.
tests/non-free/strchr.c:500:[value] warning: assertion 'refined' got status unknown.
tests/non-free/strchr.c:501:[value] assertion got status valid.
tests/non-free/strchr.c:502:[value] assertion got status valid.
tests/non-free/strchr.c:503:[value] assertion got status valid.
-tests/non-free/strchr.c:504:[value] assertion got status valid.
+tests/non-free/strchr.c:504:[value] warning: assertion got status unknown.
[value] Recording results for strchr_small_sets_chars
[value] Done for function strchr_small_sets_chars
[value] computing for function strchr_unbounded <- main.
@@ -881,6 +848,7 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
[value] Done for function strchr_garbled_mix_in_char
[value] Recording results for main
[value] done for function main
+[scope:rm_asserts] removing 3 assertion(s)
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function init_array_nondet:
from ∈ {-1}
@@ -903,9 +871,9 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
&empty_or_uninitialized[0] ; &s[1] ; &t[3] ; &s + {2} ; &a + [0..99] ;
&a + [0..79] ; &s[0] ; &maybe_init[1] ; &u + [0..799] ;
&r + [0..803] ; &t + [0..3999999] ;
- &s{[10], [14], [15], [16], [17], [18], [19]} ; &t{[0], [1]} ;
- &t + [0..29] ; "" ; "a" + {1} ; "aa" + {2} ; "aaa" + {3} ;
- "aaaa" + {4} ; "aaaaa" + {5} ; "aaaaaa" + {6} ; "aaaaaaaaa" + {9} ;
+ &s{[10], [14], [15], [16], [17], [18], [19]} ; &t + [0..29] ;
+ "" ; "a" + {1} ; "aa" + {2} ; "aaa" + {3} ; "aaaa" + {4} ;
+ "aaaaa" + {5} ; "aaaaaa" + {6} ; "aaaaaaaaa" + {9} ;
"aaaaaaaaaa" + {10} ; "aaaaaaaaaaa" + {11} ; "aaaaaaaaaaaa" + {12} ;
"aaaaaaaaaaaaa" + {13} ; "abc" + {3} ; "\000bc" + {0; 3} ; "" ;
"b\000c" + {1; 3} ; "Hello World\n" + {12} ;
@@ -1070,7 +1038,7 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
res[0..1] ∈ {-1; 0; 1; 2; 3}
[2] ∈ {-1; 0}
[3] ∈ {-1; 0; 1; 2; 3}
- [4] ∈ {-1; 0; 1}
+ [4] ∈ UNINITIALIZED
__retres ∈ {0}
[value:final-states] Values at end of function strchr_small_sets_chars:
c ∈ {0; 98; 99}
@@ -1078,7 +1046,7 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
[1] ∈ {-1; 0; 1; 2; 3}
[2] ∈ {-1; 0}
[3] ∈ {-1; 0; 1; 2; 3}
- [4] ∈ {-1; 0; 1}
+ [4] ∈ UNINITIALIZED
[value:final-states] Values at end of function strchr_unbounded:
c ∈ [--..--]
s ∈ {{ &t[0] ; "ABCDEFGHIJKLMNOPQRSTUVWXYZ" }}
@@ -1103,12 +1071,12 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
zero_str ∈ {{ "abc\000\000\000abc" }}
__retres ∈ {0}
[from] Computing for function init_array_nondet
-[from] Computing for function Frama_C_memset <-init_array_nondet
-[from] Done for function Frama_C_memset
+[from] Computing for function memset <-init_array_nondet
+[from] Done for function memset
[from] Done for function init_array_nondet
[from] Computing for function my_strchr
-[from] Computing for function Frama_C_strchr <-my_strchr
-[from] Done for function Frama_C_strchr
+[from] Computing for function strchr <-my_strchr
+[from] Done for function strchr
[from] Done for function my_strchr
[from] Computing for function my_strchr2
[from] Done for function my_strchr2
@@ -1157,28 +1125,34 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
-[from] Function Frama_C_memset:
+[from] Function memset:
a[0..99] FROM c (and SELF)
a[0..99] FROM c (and SELF)
u[0..199] FROM c (and SELF)
r[0..200] FROM c (and SELF)
t[0..999999] FROM c (and SELF)
t[0..29] FROM c (and SELF)
- \result FROM p
-[from] Function Frama_C_strchr:
- \result FROM c; t[0..3]; empty_or_non_terminated[0]; non_terminated[0];
+ \result FROM s
+[from] Function init_array_nondet:
+ a[0..99] FROM val1; val2; nondet (and SELF)
+ a[0..99] FROM val1; val2; nondet (and SELF)
+ u[0..199] FROM val1; val2; nondet (and SELF)
+ r[0..200] FROM val1; val2; nondet (and SELF)
+ t[0..999999] FROM val1; val2; nondet (and SELF)
+ t[0..29] FROM val1; val2; nondet (and SELF)
+[from] Function strchr:
+ \result FROM s; c; t[0..3]; empty_or_non_terminated[0]; non_terminated[0];
non_terminated2[0..3]; empty_or_uninitialized[0];
uninitialized[0]; s[0..1]; t[0..3]; s; s; a[0..99]; a[0..99];
s[0..3]; loc_char_array[0..4]; x; unterminated_string[0..11];
maybe_init[0..1]; u[0..199]; r[0..200]; t[0..999999];
- s[0..19]; t[0..3]; t[0..29]; s; x; ""[bits 0 to 7];
- "a"[bits 0 to 15]; "aa"[bits 0 to 23]; "aaa";
- "aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
- "aaaaaa"[bits 0 to 55]; "aaaaaaaaa"[bits 0 to 79];
- "aaaaaaaaaa"[bits 0 to 87]; "aaaaaaaaaaa"[bits 0 to 95];
- "aaaaaaaaaaaa"[bits 0 to 103]; "aaaaaaaaaaaaa"[bits 0 to 111];
- "abc"; "\000bc"; ""[bits 0 to 7]; "b\000c";
- "Hello World\n"[bits 0 to 103];
+ s[0..19]; t[0..29]; s; x; ""[bits 0 to 7]; "a"[bits 0 to 15];
+ "aa"[bits 0 to 23]; "aaa"; "aaaa"[bits 0 to 39];
+ "aaaaa"[bits 0 to 47]; "aaaaaa"[bits 0 to 55];
+ "aaaaaaaaa"[bits 0 to 79]; "aaaaaaaaaa"[bits 0 to 87];
+ "aaaaaaaaaaa"[bits 0 to 95]; "aaaaaaaaaaaa"[bits 0 to 103];
+ "aaaaaaaaaaaaa"[bits 0 to 111]; "abc"; "\000bc";
+ ""[bits 0 to 7]; "b\000c"; "Hello World\n"[bits 0 to 103];
"abc\000\000\000abc"[bits 0 to 79];
"Bonjour Monde\n"[bits 0 to 119]; "abc"; "ABCD"[bits 0 to 39];
"efg"; "EFGH"[bits 0 to 39]; "mno\000pqr"[bits 0 to 63];
@@ -1186,22 +1160,15 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
"b\000c"; "abcd"[bits 0 to 39];
"ABCDEFGHIJKLMNOPQRSTUVWXYZ"[bits 0 to 215];
"hello"[bits 0 to 47]
-[from] Function init_array_nondet:
- a[0..99] FROM val1; val2; nondet (and SELF)
- a[0..99] FROM val1; val2; nondet (and SELF)
- u[0..199] FROM val1; val2; nondet (and SELF)
- r[0..200] FROM val1; val2; nondet (and SELF)
- t[0..999999] FROM val1; val2; nondet (and SELF)
- t[0..29] FROM val1; val2; nondet (and SELF)
[from] Function my_strchr:
- \result FROM s; c; t[0..3]; empty_or_non_terminated[0]; non_terminated[0];
- non_terminated2[0..3]; empty_or_uninitialized[0];
- uninitialized[0]; s[0..1]; t[0..3]; s; a[0..99]; a[0..99];
- s[0..3]; loc_char_array[0..4]; x; unterminated_string[0..11];
- maybe_init[0..1]; u[0..199]; r[0..200]; t[0..999999];
- s[0..19]; t[0..3]; t[0..29]; s; ""[bits 0 to 7];
- "a"[bits 0 to 15]; "aa"[bits 0 to 23]; "aaa";
- "aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
+ \result FROM s; offs; c; t[0..3]; empty_or_non_terminated[0];
+ non_terminated[0]; non_terminated2[0..3];
+ empty_or_uninitialized[0]; uninitialized[0]; s[0..1];
+ t[0..3]; s; a[0..99]; a[0..99]; s[0..3]; loc_char_array[0..4];
+ x; unterminated_string[0..11]; maybe_init[0..1]; u[0..199];
+ r[0..200]; t[0..999999]; s[0..19]; t[0..29]; s;
+ ""[bits 0 to 7]; "a"[bits 0 to 15]; "aa"[bits 0 to 23];
+ "aaa"; "aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
"aaaaaa"[bits 0 to 55]; "aaaaaaaaa"[bits 0 to 79];
"aaaaaaaaaa"[bits 0 to 87]; "aaaaaaaaaaa"[bits 0 to 95];
"aaaaaaaaaaaa"[bits 0 to 103]; "aaaaaaaaaaaaa"[bits 0 to 111];
@@ -1215,14 +1182,15 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
"ABCDEFGHIJKLMNOPQRSTUVWXYZ"[bits 0 to 215];
"hello"[bits 0 to 47]
[from] Function my_strchr2:
- \result FROM base; c; loc_char_array[0..4]; x; unterminated_string[0..11];
- maybe_init[0..1]; ""[bits 0 to 7]; "a"[bits 0 to 15];
- "aa"[bits 0 to 23]; "aaa"; "aaaa"[bits 0 to 39];
- "aaaaa"[bits 0 to 47]; "aaaaaa"[bits 0 to 55];
- "aaaaaaaaa"[bits 0 to 79]; "aaaaaaaaaa"[bits 0 to 87];
- "aaaaaaaaaaa"[bits 0 to 95]; "aaaaaaaaaaaa"[bits 0 to 103];
- "aaaaaaaaaaaaa"[bits 0 to 111]; "abc"; "\000bc";
- ""[bits 0 to 7]; "b\000c"; "Hello World\n"[bits 0 to 103];
+ \result FROM base; offs1; offs2; c; loc_char_array[0..4]; x;
+ unterminated_string[0..11]; maybe_init[0..1]; nondet;
+ ""[bits 0 to 7]; "a"[bits 0 to 15]; "aa"[bits 0 to 23];
+ "aaa"; "aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
+ "aaaaaa"[bits 0 to 55]; "aaaaaaaaa"[bits 0 to 79];
+ "aaaaaaaaaa"[bits 0 to 87]; "aaaaaaaaaaa"[bits 0 to 95];
+ "aaaaaaaaaaaa"[bits 0 to 103]; "aaaaaaaaaaaaa"[bits 0 to 111];
+ "abc"; "\000bc"; ""[bits 0 to 7]; "b\000c";
+ "Hello World\n"[bits 0 to 103];
"abc\000\000\000abc"[bits 0 to 79];
"Bonjour Monde\n"[bits 0 to 119]; "abc"; "ABCD"[bits 0 to 39];
"efg"; "EFGH"[bits 0 to 39]; "mno\000pqr"[bits 0 to 63];
@@ -1260,20 +1228,7 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
[from] Function strchr_small_sets:
NO EFFECTS
[from] Function strchr_small_sets_no_assertions:
- res[0..3]
- FROM c; res; ""[bits 0 to 7]; "a"[bits 0 to 15]; "aa"[bits 0 to 23];
- "aaa"; "aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
- "aaaaaa"[bits 0 to 55]; "aaaaaaaaa"[bits 0 to 79];
- "aaaaaaaaaa"[bits 0 to 87]; "aaaaaaaaaaa"[bits 0 to 95];
- "aaaaaaaaaaaa"[bits 0 to 103]; "aaaaaaaaaaaaa"[bits 0 to 111];
- "abc"; "\000bc"; ""[bits 0 to 7]; "b\000c";
- "Hello World\n"[bits 0 to 103]; "abc\000\000\000abc"[bits 0 to 79];
- "Bonjour Monde\n"[bits 0 to 119]; "abc"; "ABCD"[bits 0 to 39];
- "efg"; "EFGH"[bits 0 to 39]; "mno\000pqr"[bits 0 to 63];
- "MNOP\000QRS"[bits 0 to 71]; "abc"; "\000bc"; ""[bits 0 to 7];
- "b\000c"; "abcd"[bits 0 to 39];
- "ABCDEFGHIJKLMNOPQRSTUVWXYZ"[bits 0 to 215]; "hello"[bits 0 to 47]
- [4]
+ res{[0..1]; [3]}
FROM c; res; nondet; ""[bits 0 to 7]; "a"[bits 0 to 15];
"aa"[bits 0 to 23]; "aaa"; "aaaa"[bits 0 to 39];
"aaaaa"[bits 0 to 47]; "aaaaaa"[bits 0 to 55];
@@ -1287,6 +1242,19 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
"MNOP\000QRS"[bits 0 to 71]; "abc"; "\000bc"; ""[bits 0 to 7];
"b\000c"; "abcd"[bits 0 to 39];
"ABCDEFGHIJKLMNOPQRSTUVWXYZ"[bits 0 to 215]; "hello"[bits 0 to 47]
+ [2]
+ FROM c; res; ""[bits 0 to 7]; "a"[bits 0 to 15]; "aa"[bits 0 to 23];
+ "aaa"; "aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
+ "aaaaaa"[bits 0 to 55]; "aaaaaaaaa"[bits 0 to 79];
+ "aaaaaaaaaa"[bits 0 to 87]; "aaaaaaaaaaa"[bits 0 to 95];
+ "aaaaaaaaaaaa"[bits 0 to 103]; "aaaaaaaaaaaaa"[bits 0 to 111];
+ "abc"; "\000bc"; ""[bits 0 to 7]; "b\000c";
+ "Hello World\n"[bits 0 to 103]; "abc\000\000\000abc"[bits 0 to 79];
+ "Bonjour Monde\n"[bits 0 to 119]; "abc"; "ABCD"[bits 0 to 39];
+ "efg"; "EFGH"[bits 0 to 39]; "mno\000pqr"[bits 0 to 63];
+ "MNOP\000QRS"[bits 0 to 71]; "abc"; "\000bc"; ""[bits 0 to 7];
+ "b\000c"; "abcd"[bits 0 to 39];
+ "ABCDEFGHIJKLMNOPQRSTUVWXYZ"[bits 0 to 215]; "hello"[bits 0 to 47]
\result FROM \nothing
[from] Function strchr_small_sets_chars:
NO EFFECTS
@@ -1312,9 +1280,9 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
non_terminated2[0..3]; empty_or_uninitialized[0]; uninitialized[0];
s[0..1]; t[0..3]; s; a[0..99]; a[0..99]; s[0..3]; loc_char_array[0..4];
unterminated_string[0..11]; maybe_init[0..1]; u[0..199]; r[0..200];
- t[0..999999]; s[0..19]; t[0..3]; t[0..29]; s; ""[bits 0 to 7];
- "a"[bits 0 to 15]; "aa"[bits 0 to 23]; "aaa"; "aaaa"[bits 0 to 39];
- "aaaaa"[bits 0 to 47]; "aaaaaa"[bits 0 to 55]; "aaaaaaaaa"[bits 0 to 79];
+ t[0..999999]; s[0..19]; t[0..29]; s; ""[bits 0 to 7]; "a"[bits 0 to 15];
+ "aa"[bits 0 to 23]; "aaa"; "aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
+ "aaaaaa"[bits 0 to 55]; "aaaaaaaaa"[bits 0 to 79];
"aaaaaaaaaa"[bits 0 to 87]; "aaaaaaaaaaa"[bits 0 to 95];
"aaaaaaaaaaaa"[bits 0 to 103]; "aaaaaaaaaaaaa"[bits 0 to 111]; "abc";
"\000bc"; ""[bits 0 to 7]; "b\000c"; "Hello World\n"[bits 0 to 103];
@@ -1495,7 +1463,7 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
"abcd"[bits 0 to 39]; "ABCDEFGHIJKLMNOPQRSTUVWXYZ"[bits 0 to 215];
"hello"[bits 0 to 47]
[inout] Out (internal) for function strchr_small_sets_no_assertions:
- s; o; tmp; t[0..3]; res[0..4]; __retres
+ s; o; tmp; t[0..3]; res[0..3]; __retres
[inout] Inputs for function strchr_small_sets_no_assertions:
nondet; ""[bits 0 to 7]; "a"[bits 0 to 15]; "aa"[bits 0 to 23]; "aaa";
"aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47]; "aaaaaa"[bits 0 to 55];
@@ -1508,7 +1476,7 @@ tests/non-free/strchr.c:534:[value] warning: builtin Frama_C_strchr:
"abcd"[bits 0 to 39]; "ABCDEFGHIJKLMNOPQRSTUVWXYZ"[bits 0 to 215];
"hello"[bits 0 to 47]
[inout] Out (internal) for function strchr_small_sets_chars:
- c; res[0..4]
+ c; res[0..3]
[inout] Inputs for function strchr_small_sets_chars:
nondet; ""[bits 0 to 7]; "a"[bits 0 to 15]; "aa"[bits 0 to 23]; "aaa";
"aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47]; "aaaaaa"[bits 0 to 55];
diff --git a/tests/non-free/oracle/strlen.res.oracle b/tests/non-free/oracle/strlen.res.oracle
index 0f928fa9724..6e33e443e91 100644
--- a/tests/non-free/oracle/strlen.res.oracle
+++ b/tests/non-free/oracle/strlen.res.oracle
@@ -341,6 +341,17 @@ tests/non-free/strlen.c:329:[value] warning: builtin Frama_C_strlen:
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
+[value:final-states] Values at end of function init_array_nondet:
+ from ∈ {-1}
+ to ∈ {-1}
+ val1 ∈ {-1}
+ val2 ∈ {-1}
+ val ∈ {0; 1; 2; 3; 4}
+ a[0..99] ∈ {0; 1; 2}
+ a[0..39] ∈ {1; 2}
+ [40..49] ∈ UNINITIALIZED
+ [50..94] ∈ {3; 4} or UNINITIALIZED
+ [95..99] ∈ UNINITIALIZED
[value:final-states] Values at end of function big_array:
t[0..999999] ∈ {270729319} or UNINITIALIZED
u[0..199] ∈ {270729319} or UNINITIALIZED
@@ -368,17 +379,6 @@ tests/non-free/strlen.c:329:[value] warning: builtin Frama_C_strlen:
[1..3] ∈ ESCAPINGADDR
z1 ∈ {0}
z2 ∈ {0}
-[value:final-states] Values at end of function init_array_nondet:
- from ∈ {-1}
- to ∈ {-1}
- val1 ∈ {-1}
- val2 ∈ {-1}
- val ∈ {0; 1; 2; 3; 4}
- a[0..99] ∈ {0; 1; 2}
- a[0..39] ∈ {1; 2}
- [40..49] ∈ UNINITIALIZED
- [50..94] ∈ {3; 4} or UNINITIALIZED
- [95..99] ∈ UNINITIALIZED
[value:final-states] Values at end of function misc:
Frama_C_entropy_source ∈ [--..--]
loc_str ∈ {{ "Bonjour Monde\n" }}
@@ -478,9 +478,13 @@ tests/non-free/strlen.c:329:[value] warning: builtin Frama_C_strlen:
[value:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
__retres ∈ {0}
+[from] Computing for function init_array_nondet
+[from] Computing for function memset <-init_array_nondet
+[from] Done for function memset
+[from] Done for function init_array_nondet
[from] Computing for function big_array
-[from] Computing for function Frama_C_strlen <-big_array
-[from] Done for function Frama_C_strlen
+[from] Computing for function strlen <-big_array
+[from] Done for function strlen
[from] Done for function big_array
[from] Computing for function bitfields
[from] Done for function bitfields
@@ -488,10 +492,6 @@ tests/non-free/strlen.c:329:[value] warning: builtin Frama_C_strlen:
[from] Done for function bitfields2
[from] Computing for function escaping
[from] Done for function escaping
-[from] Computing for function init_array_nondet
-[from] Computing for function Frama_C_memset <-init_array_nondet
-[from] Done for function Frama_C_memset
-[from] Done for function init_array_nondet
[from] Computing for function misc
[from] Computing for function Frama_C_interval <-misc
[from] Done for function Frama_C_interval
@@ -517,11 +517,14 @@ tests/non-free/strlen.c:329:[value] warning: builtin Frama_C_strlen:
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
-[from] Function Frama_C_memset:
+[from] Function memset:
a[0..99] FROM c (and SELF)
a[0..99] FROM c (and SELF)
- \result FROM p
-[from] Function Frama_C_strlen:
+ \result FROM s
+[from] Function init_array_nondet:
+ a[0..99] FROM val1; val2; nondet (and SELF)
+ a[0..99] FROM val1; val2; nondet (and SELF)
+[from] Function strlen:
\result FROM unterminated_string[0..11]; t[0..3];
empty_or_non_terminated[0]; non_terminated[0];
non_terminated2[2..3]; empty_or_uninitialized[0];
@@ -547,9 +550,6 @@ tests/non-free/strlen.c:329:[value] warning: builtin Frama_C_strlen:
NO EFFECTS
[from] Function escaping:
NO EFFECTS
-[from] Function init_array_nondet:
- a[0..99] FROM val1; val2; nondet (and SELF)
- a[0..99] FROM val1; val2; nondet (and SELF)
[from] Function misc:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function my_strlen:
@@ -582,6 +582,10 @@ tests/non-free/strlen.c:329:[value] warning: builtin Frama_C_strlen:
Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function init_array_nondet:
+ from; to; val1; val2; val; tmp; a[0..99]; a{[0..39]; [50..94]}
+[inout] Inputs for function init_array_nondet:
+ nondet
[inout] Out (internal) for function big_array:
t[0..999999]; u[0..199]; r[0..200]; p; len_u; len_r; len_t
[inout] Inputs for function big_array:
@@ -598,10 +602,6 @@ tests/non-free/strlen.c:329:[value] warning: builtin Frama_C_strlen:
s[0..3]; z1; tmp; z2; tmp_0
[inout] Inputs for function escaping:
nondet
-[inout] Out (internal) for function init_array_nondet:
- from; to; val1; val2; val; tmp; a[0..99]; a{[0..39]; [50..94]}
-[inout] Inputs for function init_array_nondet:
- nondet
[inout] Out (internal) for function misc:
Frama_C_entropy_source; loc_str; loc_char_array[3]; sz1; sz2; sz3;
sz4; sz5; sz6; sz7; sz8; x; z; i; str; s1; tmp; s2; tmp_0; j;
diff --git a/tests/non-free/oracle/strnlen2.res.oracle b/tests/non-free/oracle/strnlen2.res.oracle
index fc31214ef8d..3c9db5c6d08 100644
--- a/tests/non-free/oracle/strnlen2.res.oracle
+++ b/tests/non-free/oracle/strnlen2.res.oracle
@@ -603,25 +603,6 @@ tests/non-free/strnlen2.c:508:[value] warning: builtin Frama_C_strnlen:
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function bitfields:
- s.a ∈ {3}
- .b ∈ {1}
- .[bits 16 to 31] ∈ UNINITIALIZED
- .c ∈ {7}
- .[bits 49 to 63] ∈ UNINITIALIZED
- p ∈ {{ (char *)&s }}
-[value:final-states] Values at end of function bitfields2:
- s.a ∈ {3}
- .b ∈ {1}
- .c ∈ {7}
- .[bits 25 to 31] ∈ UNINITIALIZED
- p ∈ {{ (char *)&s }}
- z1 ∈ {2}
-[value:final-states] Values at end of function escaping:
- s[0] ∈ {0}
- [1..3] ∈ ESCAPINGADDR
- z1 ∈ {0}
- z2 ∈ {0}
[value:final-states] Values at end of function init_array_nondet:
from ∈ {-1}
to ∈ {-1}
@@ -651,6 +632,25 @@ tests/non-free/strnlen2.c:508:[value] warning: builtin Frama_C_strnlen:
len_u ∈ [0..799]
len_r ∈ [0..803]
len_t ∈ [0..3999999]
+[value:final-states] Values at end of function bitfields:
+ s.a ∈ {3}
+ .b ∈ {1}
+ .[bits 16 to 31] ∈ UNINITIALIZED
+ .c ∈ {7}
+ .[bits 49 to 63] ∈ UNINITIALIZED
+ p ∈ {{ (char *)&s }}
+[value:final-states] Values at end of function bitfields2:
+ s.a ∈ {3}
+ .b ∈ {1}
+ .c ∈ {7}
+ .[bits 25 to 31] ∈ UNINITIALIZED
+ p ∈ {{ (char *)&s }}
+ z1 ∈ {2}
+[value:final-states] Values at end of function escaping:
+ s[0] ∈ {0}
+ [1..3] ∈ ESCAPINGADDR
+ z1 ∈ {0}
+ z2 ∈ {0}
[value:final-states] Values at end of function initialization:
empty_or_uninitialized[0] ∈ {0} or UNINITIALIZED
z1 ∈ {0}
@@ -809,20 +809,20 @@ tests/non-free/strnlen2.c:508:[value] warning: builtin Frama_C_strnlen:
[value:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
__retres ∈ {0}
+[from] Computing for function init_array_nondet
+[from] Computing for function memset <-init_array_nondet
+[from] Done for function memset
+[from] Done for function init_array_nondet
+[from] Computing for function big_array
+[from] Computing for function strnlen <-big_array
+[from] Done for function strnlen
+[from] Done for function big_array
[from] Computing for function bitfields
-[from] Computing for function Frama_C_strnlen <-bitfields
-[from] Done for function Frama_C_strnlen
[from] Done for function bitfields
[from] Computing for function bitfields2
[from] Done for function bitfields2
[from] Computing for function escaping
[from] Done for function escaping
-[from] Computing for function init_array_nondet
-[from] Computing for function Frama_C_memset <-init_array_nondet
-[from] Done for function Frama_C_memset
-[from] Done for function init_array_nondet
-[from] Computing for function big_array
-[from] Done for function big_array
[from] Computing for function initialization
[from] Done for function initialization
[from] Computing for function intervals
@@ -856,7 +856,7 @@ tests/non-free/strnlen2.c:508:[value] warning: builtin Frama_C_strnlen:
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
-[from] Function Frama_C_memset:
+[from] Function memset:
a[0..99] FROM c (and SELF)
a[0..99] FROM c (and SELF)
u[0..199] FROM c (and SELF)
@@ -864,8 +864,16 @@ tests/non-free/strnlen2.c:508:[value] warning: builtin Frama_C_strnlen:
t[0..999999] FROM c (and SELF)
a[0..99] FROM c (and SELF)
a[0..99] FROM c (and SELF)
- \result FROM p
-[from] Function Frama_C_strnlen:
+ \result FROM s
+[from] Function init_array_nondet:
+ a[0..99] FROM val1; val2; nondet (and SELF)
+ a[0..99] FROM val1; val2; nondet (and SELF)
+ u[0..199] FROM val1; val2; nondet (and SELF)
+ r[0..200] FROM val1; val2; nondet (and SELF)
+ t[0..999999] FROM val1; val2; nondet (and SELF)
+ a[0..99] FROM val1; val2; nondet (and SELF)
+ a[0..99] FROM val1; val2; nondet (and SELF)
+[from] Function strnlen:
\result FROM unterminated_string[0..11]; t[0..3];
empty_or_non_terminated[0]; non_terminated[0];
non_terminated2[2..3]; empty_or_uninitialized[0];
@@ -885,22 +893,14 @@ tests/non-free/strnlen2.c:508:[value] warning: builtin Frama_C_strnlen:
"mno\000pqr"[bits 0 to 63]; "MNOP\000QRS"[bits 0 to 71];
"abcde"[bits 0 to 47]; "\000bcdef"[bits 0 to 55];
"bcd\000efg"[bits 0 to 63]; "abc"; "bcd\000eg"[bits 0 to 55]
+[from] Function big_array:
+ NO EFFECTS
[from] Function bitfields:
NO EFFECTS
[from] Function bitfields2:
NO EFFECTS
[from] Function escaping:
NO EFFECTS
-[from] Function init_array_nondet:
- a[0..99] FROM val1; val2; nondet (and SELF)
- a[0..99] FROM val1; val2; nondet (and SELF)
- u[0..199] FROM val1; val2; nondet (and SELF)
- r[0..200] FROM val1; val2; nondet (and SELF)
- t[0..999999] FROM val1; val2; nondet (and SELF)
- a[0..99] FROM val1; val2; nondet (and SELF)
- a[0..99] FROM val1; val2; nondet (and SELF)
-[from] Function big_array:
- NO EFFECTS
[from] Function initialization:
NO EFFECTS
[from] Function intervals:
@@ -929,6 +929,15 @@ tests/non-free/strnlen2.c:508:[value] warning: builtin Frama_C_strnlen:
Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function init_array_nondet:
+ from; to; val1; val2; val; tmp; a[0..99]; a{[0..39]; [50..94]}; u[0..199];
+ r[0..200]; t[0..999999]; a[0..99]; a{[0..9]; [11..19]}
+[inout] Inputs for function init_array_nondet:
+ nondet
+[inout] Out (internal) for function big_array:
+ u[0..199]; r[0..200]; t[0..999999]; p; len_u; len_r; len_t
+[inout] Inputs for function big_array:
+ nondet
[inout] Out (internal) for function bitfields:
s{{.a; .b}; .c}; p
[inout] Inputs for function bitfields:
@@ -941,15 +950,6 @@ tests/non-free/strnlen2.c:508:[value] warning: builtin Frama_C_strnlen:
s[0..3]; z1; tmp; z2; tmp_0
[inout] Inputs for function escaping:
nondet
-[inout] Out (internal) for function init_array_nondet:
- from; to; val1; val2; val; tmp; a[0..99]; a{[0..39]; [50..94]}; u[0..199];
- r[0..200]; t[0..999999]; a[0..99]; a{[0..9]; [11..19]}
-[inout] Inputs for function init_array_nondet:
- nondet
-[inout] Out (internal) for function big_array:
- u[0..199]; r[0..200]; t[0..999999]; p; len_u; len_r; len_t
-[inout] Inputs for function big_array:
- nondet
[inout] Out (internal) for function initialization:
empty_or_uninitialized[0]; z1; tmp; s[0..1]; z2; tmp_0; t[0..3]; z3; tmp_1
[inout] Inputs for function initialization:
diff --git a/tests/non-free/oracle/wcslen.res.oracle b/tests/non-free/oracle/wcslen.res.oracle
index 170b40de1c4..39040a33d3d 100644
--- a/tests/non-free/oracle/wcslen.res.oracle
+++ b/tests/non-free/oracle/wcslen.res.oracle
@@ -348,6 +348,17 @@ tests/non-free/wcslen.c:333:[value] warning: builtin Frama_C_wcslen:
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
+[value:final-states] Values at end of function init_array_nondet:
+ from ∈ {-1}
+ to ∈ {-1}
+ val1 ∈ {-1}
+ val2 ∈ {-1}
+ val ∈ {0; 1; 2; 3; 4}
+ a[0..99] ∈ {0; 16843009; 33686018}
+ a[0..39] ∈ {16843009; 33686018}
+ [40..49] ∈ UNINITIALIZED
+ [50..94] ∈ {50529027; 67372036} or UNINITIALIZED
+ [95..99] ∈ UNINITIALIZED
[value:final-states] Values at end of function big_array:
t[0..999999] ∈ {1162886966899900416} or UNINITIALIZED
u[0..199] ∈ {1162886966899900416} or UNINITIALIZED
@@ -374,17 +385,6 @@ tests/non-free/wcslen.c:333:[value] warning: builtin Frama_C_wcslen:
[1..3] ∈ ESCAPINGADDR
z1 ∈ {0}
z2 ∈ {0}
-[value:final-states] Values at end of function init_array_nondet:
- from ∈ {-1}
- to ∈ {-1}
- val1 ∈ {-1}
- val2 ∈ {-1}
- val ∈ {0; 1; 2; 3; 4}
- a[0..99] ∈ {0; 16843009; 33686018}
- a[0..39] ∈ {16843009; 33686018}
- [40..49] ∈ UNINITIALIZED
- [50..94] ∈ {50529027; 67372036} or UNINITIALIZED
- [95..99] ∈ UNINITIALIZED
[value:final-states] Values at end of function misc:
Frama_C_entropy_source ∈ [--..--]
loc_str ∈ {{ L"Bonjour Monde\n" }}
@@ -492,9 +492,13 @@ tests/non-free/wcslen.c:333:[value] warning: builtin Frama_C_wcslen:
[value:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
__retres ∈ {0}
+[from] Computing for function init_array_nondet
+[from] Computing for function memset <-init_array_nondet
+[from] Done for function memset
+[from] Done for function init_array_nondet
[from] Computing for function big_array
-[from] Computing for function Frama_C_wcslen <-big_array
-[from] Done for function Frama_C_wcslen
+[from] Computing for function wcslen <-big_array
+[from] Done for function wcslen
[from] Done for function big_array
[from] Computing for function bitfields
[from] Done for function bitfields
@@ -502,10 +506,6 @@ tests/non-free/wcslen.c:333:[value] warning: builtin Frama_C_wcslen:
[from] Done for function bitfields2
[from] Computing for function escaping
[from] Done for function escaping
-[from] Computing for function init_array_nondet
-[from] Computing for function Frama_C_memset <-init_array_nondet
-[from] Done for function Frama_C_memset
-[from] Done for function init_array_nondet
[from] Computing for function misc
[from] Computing for function Frama_C_interval <-misc
[from] Done for function Frama_C_interval
@@ -531,11 +531,14 @@ tests/non-free/wcslen.c:333:[value] warning: builtin Frama_C_wcslen:
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
-[from] Function Frama_C_memset:
+[from] Function memset:
a[0..99] FROM c (and SELF)
a[0..99] FROM c (and SELF)
- \result FROM p
-[from] Function Frama_C_wcslen:
+ \result FROM s
+[from] Function init_array_nondet:
+ a[0..99] FROM val1; val2; nondet (and SELF)
+ a[0..99] FROM val1; val2; nondet (and SELF)
+[from] Function wcslen:
\result FROM unterminated_string[0..11]; t[0..3];
empty_or_non_terminated[0]; non_terminated[0];
non_terminated2[2..3]; empty_or_uninitialized[0];
@@ -563,9 +566,6 @@ tests/non-free/wcslen.c:333:[value] warning: builtin Frama_C_wcslen:
NO EFFECTS
[from] Function escaping:
NO EFFECTS
-[from] Function init_array_nondet:
- a[0..99] FROM val1; val2; nondet (and SELF)
- a[0..99] FROM val1; val2; nondet (and SELF)
[from] Function misc:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function my_wcslen:
@@ -600,6 +600,10 @@ tests/non-free/wcslen.c:333:[value] warning: builtin Frama_C_wcslen:
Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function init_array_nondet:
+ from; to; val1; val2; val; tmp; a[0..99]; a{[0..39]; [50..94]}
+[inout] Inputs for function init_array_nondet:
+ nondet
[inout] Out (internal) for function big_array:
t[0..999999]; u[0..199]; r[0..200]; p; len_u; len_r; len_t
[inout] Inputs for function big_array:
@@ -616,10 +620,6 @@ tests/non-free/wcslen.c:333:[value] warning: builtin Frama_C_wcslen:
s[0..3]; z1; tmp; z2; tmp_0
[inout] Inputs for function escaping:
nondet
-[inout] Out (internal) for function init_array_nondet:
- from; to; val1; val2; val; tmp; a[0..99]; a{[0..39]; [50..94]}
-[inout] Inputs for function init_array_nondet:
- nondet
[inout] Out (internal) for function misc:
Frama_C_entropy_source; loc_str; loc_char_array[3]; sz1; sz2; sz3;
sz4; sz5; sz6; sz7; sz8; x[0..3]; z[0..3]; i; str; s1; tmp; s2; tmp_0;
diff --git a/tests/non-free/precise_memset.c b/tests/non-free/precise_memset.c
index 56878692da1..1fac6f5db6d 100644
--- a/tests/non-free/precise_memset.c
+++ b/tests/non-free/precise_memset.c
@@ -2,8 +2,8 @@
STDOPT: #" -val -calldeps "
*/
-//@ assigns ((char*)dst)[0..] \from v, size; assigns \result \from dst;
-void * Frama_C_memset(void * dst, int v, unsigned long size);
+#include "string.h"
+
volatile v;
@@ -69,25 +69,25 @@ char t_b[SIZE];
short t_s[SIZE];
void main() {
- Frama_C_memset (&x, 0x2, sizeof(x));
- Frama_C_memset (&t, 0x3, sizeof(t));
- Frama_C_memset (&u, 154, sizeof(u));
- Frama_C_memset (&f, 0x2, sizeof(float));
- Frama_C_memset (&fnan, 0xFF, sizeof(float));
- Frama_C_memset (&d, 0x2, sizeof(double));
- Frama_C_memset (&dnan, 0xFF, sizeof(double));
- Frama_C_memset (&w1, 0x2, sizeof(w1));
- Frama_C_memset (&bitf, 126, sizeof(bitf));
- Frama_C_memset (&tone, 0x6, sizeof(tone));
+ memset (&x, 0x2, sizeof(x));
+ memset (&t, 0x3, sizeof(t));
+ memset (&u, 154, sizeof(u));
+ memset (&f, 0x2, sizeof(float));
+ memset (&fnan, 0xFF, sizeof(float));
+ memset (&d, 0x2, sizeof(double));
+ memset (&dnan, 0xFF, sizeof(double));
+ memset (&w1, 0x2, sizeof(w1));
+ memset (&bitf, 126, sizeof(bitf));
+ memset (&tone, 0x6, sizeof(tone));
int n = v;
//@ assert 1 <= n <= 8;
- Frama_C_memset (&w2, n, sizeof(w2));
-
- Frama_C_memset(&vs, 0x04, sizeof(short));
- Frama_C_memset(vs.t, 0x02, sizeof(vs.t));
- Frama_C_memset(&vv, 0x06, sizeof(short));
- Frama_C_memset(&t[15], 0x07, 20*sizeof(short));
- Frama_C_memset(t_b, 0x05, sizeof(t_b));
- Frama_C_memset(t_s, 0x13, sizeof(t_s));
+ memset (&w2, n, sizeof(w2));
+
+ memset(&vs, 0x04, sizeof(short));
+ memset(vs.t, 0x02, sizeof(vs.t));
+ memset(&vv, 0x06, sizeof(short));
+ memset(&t[15], 0x07, 20*sizeof(short));
+ memset(t_b, 0x05, sizeof(t_b));
+ memset(t_s, 0x13, sizeof(t_s));
}
diff --git a/tests/non-free/realloc.c b/tests/non-free/realloc.c
index 0bf087610fe..5351982c752 100644
--- a/tests/non-free/realloc.c
+++ b/tests/non-free/realloc.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-slevel 10 -val-builtin malloc:Frama_C_malloc_fresh,free:Frama_C_free,realloc:Frama_C_realloc -val-malloc-functions malloc,realloc -val-warn-copy-indeterminate @all"
+ STDOPT: +"-slevel 10 -val-builtin malloc:Frama_C_malloc_fresh -val-malloc-functions malloc,realloc -val-warn-copy-indeterminate @all"
*/
#include <stdlib.h>
diff --git a/tests/non-free/realloc_multiple.c b/tests/non-free/realloc_multiple.c
index 9b97fde2a3c..14fad8f1fd8 100644
--- a/tests/non-free/realloc_multiple.c
+++ b/tests/non-free/realloc_multiple.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-slevel 10 -val-builtin malloc:Frama_C_malloc_fresh,free:Frama_C_free,realloc:Frama_C_realloc_multiple -val-malloc-functions malloc,realloc"
+ STDOPT: +"-slevel 10 -val-builtin malloc:Frama_C_malloc_fresh,realloc:Frama_C_realloc_multiple -val-malloc-functions malloc,realloc"
*/
#include <stdlib.h>
diff --git a/tests/non-free/strchr.c b/tests/non-free/strchr.c
index e065f100f03..3464a03ff39 100644
--- a/tests/non-free/strchr.c
+++ b/tests/non-free/strchr.c
@@ -1,4 +1,5 @@
#include "__fc_builtin.h"
+#include "string.h"
// NOTE: all unnamed assertions should be valid.
// Imprecise results should be defined using named
@@ -11,9 +12,8 @@
static volatile int nondet;
#define assert_bottom(exp,id) if (nondet) { exp; Frama_C_show_each_unreachable_ ## id(); }
-#define strchr Frama_C_strchr
-//@ assigns \result \from ((char*)s)[0..], c;
-char *Frama_C_strchr(const char *s, int c);
+
+
// Definitions for C++ oracle checking
typedef int Ival;
@@ -154,7 +154,7 @@ void strchr_bitfields() {
s.c = 7;
CHAR_PTR(p);
p = &s;
- assert_bottom(Frama_C_strchr(p, c),bitfields);
+ assert_bottom(strchr(p, c),bitfields);
}
typedef struct {
@@ -177,7 +177,7 @@ void strchr_bitfields2() {
void init_array_nondet(void *a, int from, int to, int val1, int val2) {
int val = NONDET(val1, val2);
- Frama_C_memset(((char*)a) + from, val, to-from+1);
+ memset(((char*)a) + from, val, to-from+1);
from = to = val1 = val2 = -1; // reset to minimize oracle changes
}
@@ -444,7 +444,7 @@ int strchr_small_sets_no_assertions(CHAR c, RES *res) {
CHAR_ARRAY(t, 4);
t[0] = t[1] = NONDET(c, 1);
t[2] = t[3] = 1;
- res[4] = my_strchr(t, 0, c);
+ /* res[4] = my_strchr(t, 0, c); Invalid: t is not a string */
return 0;
}
diff --git a/tests/non-free/strlen.c b/tests/non-free/strlen.c
index f1e34b98345..3b0e9a7916d 100644
--- a/tests/non-free/strlen.c
+++ b/tests/non-free/strlen.c
@@ -1,4 +1,5 @@
#include "__fc_builtin.h"
+#include "string.h"
// NOTE: all unnamed assertions should be valid.
// Imprecise results should be defined using named
@@ -11,9 +12,8 @@
static volatile int nondet;
#define assert_bottom(exp,id) if (nondet) { exp; Frama_C_show_each_unreachable_ ## id(); }
-#define strlen Frama_C_strlen
-//@ assigns \result \from p[0..];
-size_t Frama_C_strlen(const char *p);
+
+
// Definitions for C++ oracle checking
typedef int Ival;
@@ -78,7 +78,7 @@ void small_sets() {
char t[4];
t[0] = t[1] = nondet ? 0 : 1;
t[2] = t[3] = 1;
- int z5 = Frama_C_strlen(t); // warning
+ int z5 = strlen(t); // warning
//@ assert z5 == 0 || z5 == 1;
}
@@ -137,7 +137,7 @@ void bitfields() {
s.b = 1;
s.c = 7;
char *p = &s;
- assert_bottom(Frama_C_strlen(p), p);
+ assert_bottom(strlen(p), p);
}
typedef struct {
@@ -152,13 +152,13 @@ void bitfields2() {
s.b = 1;
s.c = 7;
char *p = &s;
- int z1 = Frama_C_strlen(p);
+ int z1 = strlen(p);
//@assert (z1 == 2);
}
void init_array_nondet(char *a, int from, int to, int val1, int val2) {
int val = NONDET(val1, val2);
- Frama_C_memset(a + from, val, to-from+1);
+ memset(a + from, val, to-from+1);
from = to = val1 = val2 = -1; // reset to minimize oracle changes
}
@@ -238,43 +238,43 @@ void misc() {
int i;
char *str;
- assert_bottom(Frama_C_strlen(unterminated_string), unterminated_string);
+ assert_bottom(strlen(unterminated_string), unterminated_string);
str = nondet ? static_str : loc_str;
- sz1 = Frama_C_strlen(str);
+ sz1 = strlen(str);
//@ assert(sz1 == 12) || (sz1 == 14);
str = &x;
str = nondet ? str : str + 3;
- sz2 = Frama_C_strlen(str);
+ sz2 = strlen(str);
//@ assert(sz2 == 0) ; // no, could also do an RTE
i = Frama_C_interval(0,TSZ-1);
str = tab_str[i];
- sz3 = Frama_C_strlen(str);
+ sz3 = strlen(str);
//@ assert (sz3 >= 0) && (sz3 <= 13);
loc_char_array[3] = '\0';
- assert_bottom(Frama_C_strlen(loc_char_array), loc_char_array);
- sz4 = Frama_C_strlen(zero_str);
+ assert_bottom(strlen(loc_char_array), loc_char_array);
+ sz4 = strlen(zero_str);
//@ assert(sz4 == 3);
char *s1 = nondet ? "abc" : "ABCD";
char *s2 = nondet ? s1 : s1+1;
- sz5 = Frama_C_strlen(s2);
+ sz5 = strlen(s2);
//@ assert(sz5 >= 2 && sz5 <= 4);
s1 = nondet ? "efg" : "EFGH";
s2 = nondet ? s1+1 : s1+2;
- sz6 = Frama_C_strlen(s2);
+ sz6 = strlen(s2);
//@ assert(sz6 >= 1 && sz6 <= 3);
s1 = nondet ? "mno\0pqr" : "MNOP\0QRS";
for (int j = 0; j < 8; j++) {
- sz7 = Frama_C_strlen(s1 + j);
+ sz7 = strlen(s1 + j);
//@ assert(sz7 >= 0 && sz7 <= 4);
}
char maybe_init[2];
maybe_init[1] = '\0';
if (nondet) maybe_init[0] = 'A';
- sz8 = Frama_C_strlen(maybe_init);
+ sz8 = strlen(maybe_init);
//@ assert(sz8 == 1);
}
diff --git a/tests/non-free/strlen_align.c b/tests/non-free/strlen_align.c
index 03dde522621..d3c0ef33934 100644
--- a/tests/non-free/strlen_align.c
+++ b/tests/non-free/strlen_align.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-val-builtin strlen:Frama_C_strlen"
+ STDOPT: #""
*/
#include <string.h>
diff --git a/tests/non-free/strnlen2.c b/tests/non-free/strnlen2.c
index 7a1a31b9b09..6f3fe740a58 100644
--- a/tests/non-free/strnlen2.c
+++ b/tests/non-free/strnlen2.c
@@ -1,10 +1,10 @@
#include "__fc_builtin.h"
+#include "string.h"
static volatile int nondet;
#define assert_bottom(exp,id) if (nondet) { exp; Frama_C_show_each_unreachable_ ## id(); }
-#define strnlen Frama_C_strnlen
-//@ assigns \result \from p[0..];
-size_t Frama_C_strnlen(const char *p, size_t maxlen);
+
+
const char* static_str = "Hello World\n";
const char* zero_str = "abc\0\0\0abc";
#define TSZ 12
@@ -114,7 +114,7 @@ void bitfields() {
s.b = 1;
s.c = 7;
char *p = &s;
- assert_bottom(Frama_C_strnlen(p, 3),bitfields);
+ assert_bottom(strnlen(p, 3),bitfields);
}
typedef struct {
@@ -129,13 +129,13 @@ void bitfields2() {
s.b = 1;
s.c = 7;
char *p = &s;
- RES z1 = Frama_C_strnlen(p, 3);
+ RES z1 = strnlen(p, 3);
//@assert (z1 == 2);
}
void init_array_nondet(void *a, int from, int to, int val1, int val2) {
int val = nondet ? val1 : val2;
- Frama_C_memset(((char*)a) + from, val, to-from+1);
+ memset(((char*)a) + from, val, to-from+1);
from = to = val1 = val2 = -1; // reset to minimize oracle changes
}
@@ -212,43 +212,43 @@ void misc() {
int i;
char *str;
- assert_bottom(Frama_C_strnlen(unterminated_string, 13),unterminated_string);
+ assert_bottom(strnlen(unterminated_string, 13),unterminated_string);
str = nondet ? static_str : loc_str;
- sz1 = Frama_C_strnlen(str, 14);
+ sz1 = strnlen(str, 14);
//@ assert(sz1 == 12) || (sz1 == 14);
str = &x;
str = nondet ? str : str + 3;
- sz2 = Frama_C_strnlen(str, 12);
+ sz2 = strnlen(str, 12);
//@ assert(sz2 == 0) ; // no, could also do an RTE
i = Frama_C_interval(0,TSZ-1);
str = tab_str[i];
- sz3 = Frama_C_strnlen(str, 13);
+ sz3 = strnlen(str, 13);
//@ assert (sz3 >= 0) && (sz3 <= 13);
loc_char_array[3] = '\0';
- assert_bottom(Frama_C_strnlen(loc_char_array, 5),loc_char_array);
- sz4 = Frama_C_strnlen(zero_str, 9);
+ assert_bottom(strnlen(loc_char_array, 5),loc_char_array);
+ sz4 = strnlen(zero_str, 9);
//@ assert(sz4 == 3);
char *s1 = nondet ? "abc" : "ABCD";
char *s2 = nondet ? s1 : s1+1;
- sz5 = Frama_C_strnlen(s2, 5);
+ sz5 = strnlen(s2, 5);
//@ assert(sz5 >= 2 && sz5 <= 4);
s1 = nondet ? "efg" : "EFGH";
s2 = nondet ? s1+1 : s1+2;
- sz6 = Frama_C_strnlen(s2, 5);
+ sz6 = strnlen(s2, 5);
//@ assert(sz6 >= 1 && sz6 <= 3);
s1 = nondet ? "mno\0pqr" : "MNOP\0QRS";
for (int j = 0; j < 8; j++) {
- sz7 = Frama_C_strnlen(s1 + j, 10);
+ sz7 = strnlen(s1 + j, 10);
//@ assert(sz7 >= 0 && sz7 <= 4);
}
char maybe_init[2];
maybe_init[1] = '\0';
IF_NONDET(maybe_init[0], 'A');
- sz8 = Frama_C_strnlen(maybe_init, 2);
+ sz8 = strnlen(maybe_init, 2);
//@ assert(sz8 == 1);
}
diff --git a/tests/non-free/wcslen.c b/tests/non-free/wcslen.c
index 634278f96ee..f3bf937c717 100644
--- a/tests/non-free/wcslen.c
+++ b/tests/non-free/wcslen.c
@@ -1,4 +1,5 @@
#include "__fc_builtin.h"
+#include "string.h"
#include <wchar.h>
// NOTE: all unnamed assertions should be valid.
// Imprecise results should be defined using named
@@ -11,9 +12,8 @@
static volatile int nondet;
#define assert_bottom(exp,id) if (nondet) { exp; Frama_C_show_each_unreachable_ ## id(); }
-#define wcslen Frama_C_wcslen
-//@ assigns \result \from p[0..];
-size_t Frama_C_wcslen(const wchar_t *p);
+
+
// Definitions for C++ oracle checking
typedef int Ival;
@@ -78,7 +78,7 @@ void small_sets() {
wchar_t t[4];
t[0] = t[1] = nondet ? 0 : 1;
t[2] = t[3] = 1;
- int z5 = Frama_C_wcslen(t); // warning
+ int z5 = wcslen(t); // warning
//@ assert z5 == 0 || z5 == 1;
}
@@ -137,7 +137,7 @@ void bitfields() {
s.b = 1;
s.c = 7;
wchar_t *p = &s;
- assert_bottom(Frama_C_wcslen(p), p);
+ assert_bottom(wcslen(p), p);
}
typedef struct {
@@ -152,13 +152,13 @@ void bitfields2() {
s.b = 1;
s.c = 0x70000;
wchar_t *p = &s;
- int z1 = Frama_C_wcslen(p);
+ int z1 = wcslen(p);
//@assert (z1 == 2);
}
void init_array_nondet(wchar_t *a, int from, int to, int val1, int val2) {
int val = NONDET(val1, val2);
- Frama_C_memset(a + from, val, sizeof(wchar_t)*(to-from+1));
+ memset(a + from, val, sizeof(wchar_t)*(to-from+1));
from = to = val1 = val2 = -1; // reset to minimize oracle changes
}
@@ -238,43 +238,43 @@ void misc() {
int i;
wchar_t *str;
- assert_bottom(Frama_C_wcslen(unterminated_string), unterminated_string);
+ assert_bottom(wcslen(unterminated_string), unterminated_string);
str = nondet ? static_str : loc_str;
- sz1 = Frama_C_wcslen(str);
+ sz1 = wcslen(str);
//@ assert(sz1 == 12) || (sz1 == 14);
str = x;
str = nondet ? str : str + 3;
- sz2 = Frama_C_wcslen(str);
+ sz2 = wcslen(str);
//@ assert(sz2 == 0) ; // no, could also do an RTE
i = Frama_C_interval(0,TSZ-1);
str = tab_str[i];
- sz3 = Frama_C_wcslen(str);
+ sz3 = wcslen(str);
//@ assert (sz3 >= 0) && (sz3 <= 13);
loc_char_array[3] = L'\0';
- assert_bottom(Frama_C_wcslen(loc_char_array), loc_char_array);
- sz4 = Frama_C_wcslen(zero_str);
+ assert_bottom(wcslen(loc_char_array), loc_char_array);
+ sz4 = wcslen(zero_str);
//@ assert(sz4 == 3);
wchar_t *s1 = nondet ? L"abc" : L"ABCD";
wchar_t *s2 = nondet ? s1 : s1+1;
- sz5 = Frama_C_wcslen(s2);
+ sz5 = wcslen(s2);
//@ assert(sz5 >= 2 && sz5 <= 4);
s1 = nondet ? L"efg" : L"EFGH";
s2 = nondet ? s1+1 : s1+2;
- sz6 = Frama_C_wcslen(s2);
+ sz6 = wcslen(s2);
//@ assert(sz6 >= 1 && sz6 <= 3);
s1 = nondet ? L"mno\0pqr" : L"MNOP\0QRS";
for (int j = 0; j < 8; j++) {
- sz7 = Frama_C_wcslen(s1 + j);
+ sz7 = wcslen(s1 + j);
//@ assert(sz7 >= 0 && sz7 <= 4);
}
wchar_t maybe_init[2];
maybe_init[1] = L'\0';
if (nondet) maybe_init[0] = L'A';
- sz8 = Frama_C_wcslen(maybe_init);
+ sz8 = wcslen(maybe_init);
//@ assert(sz8 == 1);
}
--
GitLab