From 81e54f9867d41a3b1f5dee38546c2926ea2c4ebd Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 28 Sep 2021 22:25:05 +0200
Subject: [PATCH] [Libc] add non-POSIX definitions and stubs to help parse
coreutils
---
share/libc/regex.h | 8 ++-
share/libc/stdlib.c | 5 ++
share/libc/stdlib.h | 9 +++
share/libc/sys/stat.h | 10 +--
src/plugins/value/utils/library_functions.ml | 18 ++---
tests/libc/oracle/fc_libc.0.res.oracle | 36 +++++-----
tests/libc/oracle/fc_libc.1.res.oracle | 9 +++
tests/libc/oracle/stdlib_c.0.res.oracle | 70 +++++++++++++++++++-
tests/libc/oracle/stdlib_c.1.res.oracle | 70 +++++++++++++++++++-
tests/libc/oracle/stdlib_c.2.res.oracle | 43 +++++++++++-
tests/libc/stdlib_c.c | 3 +
11 files changed, 240 insertions(+), 41 deletions(-)
diff --git a/share/libc/regex.h b/share/libc/regex.h
index ac0bb089414..a08abdb485d 100644
--- a/share/libc/regex.h
+++ b/share/libc/regex.h
@@ -28,7 +28,13 @@ __PUSH_FC_STDLIB
#include "__fc_define_ssize_t.h"
__BEGIN_DECLS
-struct re_pattern_buffer { size_t re_nsub; };
+struct re_pattern_buffer {
+ struct re_dfa_t *buffer; // Non-POSIX
+ size_t allocated; // Non-POSIX
+ char *fastmap; // Non-POSIX
+ unsigned char *translate; // Non-POSIX
+ size_t re_nsub;
+};
typedef struct re_pattern_buffer regex_t;
diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index e473fe89afb..1596d1b195c 100644
--- a/share/libc/stdlib.c
+++ b/share/libc/stdlib.c
@@ -232,4 +232,9 @@ char *realpath(const char *restrict file_name, char *restrict resolved_name)
return resolved_name;
}
+char *canonicalize_file_name(const char *path) {
+ return realpath(path, NULL);
+}
+
+
__POP_FC_STDLIB
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 688c2885483..dcb1f408493 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -699,9 +699,18 @@ extern int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
extern int mkstemp(char *templat);
+// This function may allocate memory for the result, which is not supported by
+// some plugins such as Eva. In such cases, it is preferable to use the stub
+// provided in stdlib.c.
extern char *realpath(const char *restrict file_name,
char *restrict resolved_name);
+// Non-POSIX; GNU extension
+// This function may allocate memory for the result, which is not supported by
+// some plugins such as Eva. In such cases, it is preferable to use the stub
+// provided in stdlib.c.
+extern char *canonicalize_file_name(const char *path);
+
__END_DECLS
__POP_FC_STDLIB
diff --git a/share/libc/sys/stat.h b/share/libc/sys/stat.h
index af9b9e59d2d..b2deabaa9ca 100644
--- a/share/libc/sys/stat.h
+++ b/share/libc/sys/stat.h
@@ -105,11 +105,11 @@ extern mode_t umask(mode_t cmask);
#define S_TYPEISTMO(buf) (0)
// Non-POSIX; Linux-specific
-#define S_IRWXUGO (S_IRWXU|S_IRWXG|S_IRWXO)
-#define S_IALLUGO (S_ISUID|S_ISGID|S_ISVTX|S_IRWXUGO)
-#define S_IRUGO (S_IRUSR|S_IRGRP|S_IROTH)
-#define S_IWUGO (S_IWUSR|S_IWGRP|S_IWOTH)
-#define S_IXUGO (S_IXUSR|S_IXGRP|S_IXOTH)
+#define S_IRWXUGO (S_IRWXU|S_IRWXG|S_IRWXO)
+#define S_IALLUGO (S_ISUID|S_ISGID|S_ISVTX|S_IRWXUGO)
+#define S_IRUGO (S_IRUSR|S_IRGRP|S_IROTH)
+#define S_IWUGO (S_IWUSR|S_IWGRP|S_IWOTH)
+#define S_IXUGO (S_IXUSR|S_IXGRP|S_IXOTH)
// Non-POSIX
#define S_IFDOOR 0
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index fb21a5a91f6..317ebbe66ee 100644
--- a/src/plugins/value/utils/library_functions.ml
+++ b/src/plugins/value/utils/library_functions.ml
@@ -71,20 +71,22 @@ let returned_value kf =
let unsupported_specifications =
- [ "asprintf", "stdio.c";
- "glob", "glob.c";
- "globfree", "glob.c";
+ [
+ "asprintf", "stdio.c";
+ "canonicalize_path_name", "stdlib.c";
"getaddrinfo", "netdb.c";
- "getline", "stdio.c";
- "strerror", "string.c";
- "strdup", "string.c";
- "strndup", "string.c";
"getenv", "stdlib.c";
+ "getline", "stdio.c";
+ "glob", "glob.c";
+ "globfree", "glob.c";
"posix_memalign", "stdlib.c";
"putenv", "stdlib.c";
+ "realpath", "stdlib.c";
"setenv", "stdlib.c";
+ "strdup", "string.c";
+ "strerror", "string.c";
+ "strndup", "string.c";
"unsetenv", "stdlib.c";
- "realpath", "stdlib.c"
]
let unsupported_specs_tbl =
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 70cedee0a6e..3e6a3b4a237 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -13,7 +13,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
-[metrics] Defined functions (128)
+[metrics] Defined functions (129)
=======================
Frama_C_abort (1 call); Frama_C_char_interval (1 call);
Frama_C_double_interval (0 call); Frama_C_float_interval (0 call);
@@ -43,17 +43,17 @@
atomic_flag_clear_explicit (0 call); atomic_flag_test_and_set (0 call);
atomic_flag_test_and_set_explicit (0 call); atomic_signal_fence (0 call);
atomic_thread_fence (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);
- getaddrinfo (0 call); getenv (0 call); gethostbyname (0 call);
- getline (0 call); glob (0 call); globfree (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); memchr (0 call);
- memcmp (1 call); memcpy (7 calls); memmove (3 calls); memoverlap (1 call);
- mempcpy (1 call); memrchr (0 call); memset (1 call);
- posix_memalign (0 call); putenv (0 call); realpath (0 call);
+ canonicalize_file_name (0 call); char_equal_ignore_case (1 call);
+ fabs (0 call); fabsf (0 call); feholdexcept (0 call); fesetenv (0 call);
+ fetestexcept (0 call); getaddrinfo (0 call); getenv (0 call);
+ gethostbyname (0 call); getline (0 call); glob (0 call); globfree (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);
+ memchr (0 call); memcmp (1 call); memcpy (7 calls); memmove (3 calls);
+ memoverlap (1 call); mempcpy (1 call); memrchr (0 call); memset (1 call);
+ posix_memalign (0 call); putenv (0 call); realpath (1 call);
res_search (1 call); setenv (0 call); setlocale (0 call); stpcpy (1 call);
str_append (3 calls); strcasecmp (0 call); strcat (0 call);
strchr (4 calls); strcmp (0 call); strcpy (1 call); strdup (0 call);
@@ -213,18 +213,18 @@
Global metrics
==============
- Sloc = 1647
+ Sloc = 1649
Decision point = 307
Global variables = 86
If = 292
Loop = 55
Goto = 118
- Assignment = 717
- Exit point = 128
- Function = 556
- Function call = 165
+ Assignment = 718
+ Exit point = 129
+ Function = 557
+ Function call = 166
Pointer dereferencing = 350
- Cyclomatic complexity = 435
+ Cyclomatic complexity = 436
[kernel] FRAMAC_SHARE/libc/sys/socket.h:451: Warning:
clause with '\initialized' must contain name 'initialization'
/* Generated by Frama-C */
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 1fe50ce6e10..880d36bf6a6 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1630,6 +1630,8 @@ extern int mkstemp(char *templat);
char *realpath(char const * restrict file_name, char * restrict resolved_name);
+char *canonicalize_file_name(char const *path);
+
/*@
predicate non_escaping{L}(void *s, ℤ n) =
∀ ℤ i; 0 ≤ i < n ⇒ ¬\dangling((char *)s + i);
@@ -7218,6 +7220,13 @@ char *realpath(char const * restrict file_name, char * restrict resolved_name)
return_label: return __retres;
}
+char *canonicalize_file_name(char const *path)
+{
+ char *tmp;
+ tmp = realpath(path,(char *)0);
+ return tmp;
+}
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle
index 455e3224fdc..de5dc645871 100644
--- a/tests/libc/oracle/stdlib_c.0.res.oracle
+++ b/tests/libc/oracle/stdlib_c.0.res.oracle
@@ -191,6 +191,58 @@
[eva] Done for function Frama_C_make_unknown
[eva] Recording results for realpath
[eva] Done for function realpath
+[eva] computing for function canonicalize_file_name <- main.
+ Called from stdlib_c.c:56.
+[eva] computing for function realpath <- canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:236.
+[eva] computing for function Frama_C_interval <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] FRAMAC_SHARE/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] FRAMAC_SHARE/libc/stdlib.c:224:
+ allocating variable __malloc_realpath_l224_0
+[eva] computing for function Frama_C_make_unknown <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] Recording results for canonicalize_file_name
+[eva] Done for function canonicalize_file_name
+[eva] computing for function canonicalize_file_name <- main.
+ Called from stdlib_c.c:56.
+[eva] computing for function realpath <- canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:236.
+[eva] computing for function Frama_C_interval <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] FRAMAC_SHARE/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] computing for function Frama_C_make_unknown <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] Recording results for canonicalize_file_name
+[eva] Done for function canonicalize_file_name
+[eva] computing for function free <- main.
+ Called from stdlib_c.c:57.
+[eva] stdlib_c.c:57: Warning: ignoring unsupported \allocates clause
+[eva] stdlib_c.c:57: function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] computing for function free <- main.
+ Called from stdlib_c.c:57.
+[eva] Done for function free
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -204,14 +256,23 @@
Frama_C_entropy_source ∈ [--..--]
__fc_errno ∈ [--..--]
resolved_name ∈
- {{ NULL ; &__malloc_main_l44[0] ;
- &__malloc_realpath_l224[0] }}
+ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
+ &__malloc_realpath_l224_0[0] }}
realpath_len ∈ [1..256]
__retres ∈
- {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] }}
+ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
+ &__malloc_realpath_l224_0[0] }}
__malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224[0] ∈ [--..--]
[1..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224_0[0] ∈ [--..--]
+ [1..255] ∈ [--..--] or UNINITIALIZED
+[eva:final-states] Values at end of function canonicalize_file_name:
+ __fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
+ __fc_errno ∈ [--..--]
+ __malloc_realpath_l224_0[0] ∈ [--..--]
+ [1..255] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
@@ -227,8 +288,11 @@
p_memal_res2 ∈ {0; 12}
resolved_name ∈ {{ NULL ; &__malloc_main_l44[0] }}
realpath_res ∈ {{ NULL ; &__malloc_realpath_l224[0] }}
+ canon ∈ {{ NULL ; &__malloc_realpath_l224_0[0] }}
__retres ∈ {0; 1}
__calloc_w_main_l33[0..1073741823] ∈ {0; 42}
__malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224[0] ∈ [--..--]
[1..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224_0[0] ∈ [--..--]
+ [1..255] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/stdlib_c.1.res.oracle b/tests/libc/oracle/stdlib_c.1.res.oracle
index 6591da2a4ba..989193e4add 100644
--- a/tests/libc/oracle/stdlib_c.1.res.oracle
+++ b/tests/libc/oracle/stdlib_c.1.res.oracle
@@ -207,6 +207,58 @@
[eva] Done for function Frama_C_make_unknown
[eva] Recording results for realpath
[eva] Done for function realpath
+[eva] computing for function canonicalize_file_name <- main.
+ Called from stdlib_c.c:56.
+[eva] computing for function realpath <- canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:236.
+[eva] computing for function Frama_C_interval <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] FRAMAC_SHARE/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] FRAMAC_SHARE/libc/stdlib.c:224:
+ allocating variable __malloc_realpath_l224_0
+[eva] computing for function Frama_C_make_unknown <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] Recording results for canonicalize_file_name
+[eva] Done for function canonicalize_file_name
+[eva] computing for function canonicalize_file_name <- main.
+ Called from stdlib_c.c:56.
+[eva] computing for function realpath <- canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:236.
+[eva] computing for function Frama_C_interval <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] FRAMAC_SHARE/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] computing for function Frama_C_make_unknown <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] Recording results for canonicalize_file_name
+[eva] Done for function canonicalize_file_name
+[eva] computing for function free <- main.
+ Called from stdlib_c.c:57.
+[eva] stdlib_c.c:57: Warning: ignoring unsupported \allocates clause
+[eva] stdlib_c.c:57: function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] computing for function free <- main.
+ Called from stdlib_c.c:57.
+[eva] Done for function free
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -220,14 +272,23 @@
Frama_C_entropy_source ∈ [--..--]
__fc_errno ∈ [--..--]
resolved_name ∈
- {{ NULL ; &__malloc_main_l44[0] ;
- &__malloc_realpath_l224[0] }}
+ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
+ &__malloc_realpath_l224_0[0] }}
realpath_len ∈ [1..256]
__retres ∈
- {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] }}
+ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
+ &__malloc_realpath_l224_0[0] }}
__malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224[0] ∈ [--..--]
[1..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224_0[0] ∈ [--..--]
+ [1..255] ∈ [--..--] or UNINITIALIZED
+[eva:final-states] Values at end of function canonicalize_file_name:
+ __fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
+ __fc_errno ∈ [--..--]
+ __malloc_realpath_l224_0[0] ∈ [--..--]
+ [1..255] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
@@ -243,8 +304,11 @@
p_memal_res2 ∈ {0}
resolved_name ∈ {{ &__malloc_main_l44[0] }}
realpath_res ∈ {{ NULL ; &__malloc_realpath_l224[0] }}
+ canon ∈ {{ NULL ; &__malloc_realpath_l224_0[0] }}
__retres ∈ {0}
__calloc_w_main_l33[0..1073741823] ∈ {0; 42}
__malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224[0] ∈ [--..--]
[1..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224_0[0] ∈ [--..--]
+ [1..255] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle
index 01861ff92b2..38d0c052072 100644
--- a/tests/libc/oracle/stdlib_c.2.res.oracle
+++ b/tests/libc/oracle/stdlib_c.2.res.oracle
@@ -172,6 +172,34 @@
[eva] Done for function Frama_C_make_unknown
[eva] Recording results for realpath
[eva] Done for function realpath
+[eva] computing for function canonicalize_file_name <- main.
+ Called from stdlib_c.c:56.
+[eva] computing for function realpath <- canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:236.
+[eva] computing for function Frama_C_interval <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] FRAMAC_SHARE/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] FRAMAC_SHARE/libc/stdlib.c:224:
+ allocating variable __malloc_realpath_l224_0
+[eva] computing for function Frama_C_make_unknown <- realpath <-
+ canonicalize_file_name <- main.
+ Called from FRAMAC_SHARE/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] Recording results for canonicalize_file_name
+[eva] Done for function canonicalize_file_name
+[eva] computing for function free <- main.
+ Called from stdlib_c.c:57.
+[eva] stdlib_c.c:57: Warning: ignoring unsupported \allocates clause
+[eva] stdlib_c.c:57: function free: precondition 'freeable' got status valid.
+[eva] Done for function free
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -198,13 +226,20 @@
Frama_C_entropy_source ∈ [--..--]
__fc_errno ∈ [--..--]
resolved_name ∈
- {{ NULL ; &__malloc_main_l44[0] ;
- &__malloc_realpath_l224[0] }}
+ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
+ &__malloc_realpath_l224_0[0] }}
realpath_len ∈ [1..256]
__retres ∈
- {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] }}
+ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
+ &__malloc_realpath_l224_0[0] }}
__malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224_0[0..255] ∈ [--..--] or UNINITIALIZED
+[eva:final-states] Values at end of function canonicalize_file_name:
+ __fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
+ __fc_errno ∈ [--..--]
+ __malloc_realpath_l224_0[0..255] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
@@ -220,9 +255,11 @@
p_memal_res2 ∈ {0; 12}
resolved_name ∈ {{ NULL ; &__malloc_main_l44[0] }}
realpath_res ∈ {{ NULL ; &__malloc_realpath_l224[0] }}
+ canon ∈ {{ NULL ; &__malloc_realpath_l224_0[0] }}
__retres ∈ {0; 1}
__malloc_calloc_l72[0..3] ∈ [--..--] or UNINITIALIZED
__malloc_calloc_l72_0[0..4294967291] ∈ [--..--] or UNINITIALIZED
__malloc_w_calloc_l72_1[0..4294967291] ∈ [--..--] or UNINITIALIZED
__malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224_0[0..255] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/stdlib_c.c b/tests/libc/stdlib_c.c
index 33dc8110214..065ed34d5cf 100644
--- a/tests/libc/stdlib_c.c
+++ b/tests/libc/stdlib_c.c
@@ -53,5 +53,8 @@ int main() {
free(resolved_name);
realpath_res = realpath("/bin/ls", NULL);
+ char *canon = canonicalize_file_name("/bin/../etc");
+ free(canon);
+
return 0;
}
--
GitLab