diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index f2b7746849a3a64caa2dc813c843b392d3a6c0cb..081be10cddc9316980317342a9e9121ece630708 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -190,6 +190,7 @@ share/libc/__fc_define_ino_t.h: CEA_LGPL
share/libc/__fc_define_intptr_t.h: CEA_LGPL
share/libc/__fc_define_iovec.h: CEA_LGPL
share/libc/__fc_define_key_t.h: CEA_LGPL
+share/libc/__fc_define_locale_t.h: CEA_LGPL
share/libc/__fc_define_max_open_files.h: CEA_LGPL
share/libc/__fc_define_mode_t.h: CEA_LGPL
share/libc/__fc_define_nlink_t.h: CEA_LGPL
@@ -254,6 +255,7 @@ share/libc/ifaddrs.h: CEA_LGPL
share/libc/inttypes.c: CEA_LGPL
share/libc/inttypes.h: CEA_LGPL
share/libc/iso646.h: CEA_LGPL
+share/libc/langinfo.h: CEA_LGPL
share/libc/libgen.h: CEA_LGPL
share/libc/limits.h: CEA_LGPL
share/libc/locale.c: CEA_LGPL
diff --git a/share/libc/__fc_define_locale_t.h b/share/libc/__fc_define_locale_t.h
new file mode 100644
index 0000000000000000000000000000000000000000..68e4db7e6d583669e556700dc00748434bfa9b44
--- /dev/null
+++ b/share/libc/__fc_define_locale_t.h
@@ -0,0 +1,36 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#ifndef __FC_DEFINE_LOCALE_T
+#define __FC_DEFINE_LOCALE_T
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+struct __fc_locale_struct
+{
+ const char *names[13];
+};
+
+typedef struct __fc_locale_struct *locale_t;
+__END_DECLS
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
index 310a2148445201ee81609116a1a60c4c84d617b0..3e710e9cec5c3dbe81bb7decbd30c1840597785e 100644
--- a/share/libc/__fc_libc.h
+++ b/share/libc/__fc_libc.h
@@ -51,6 +51,7 @@
#include "ifaddrs.h"
#include "inttypes.h"
#include "iso646.h"
+#include "langinfo.h"
#include "libgen.h"
#include "limits.h"
#include "locale.h"
diff --git a/share/libc/fcntl.h b/share/libc/fcntl.h
index 2fb91da8e750e37edddf13263dd6e283dc221be7..7ef658186f97dd26eb9503d0337d8af367f6e357 100644
--- a/share/libc/fcntl.h
+++ b/share/libc/fcntl.h
@@ -63,6 +63,9 @@ __PUSH_FC_STDLIB
#define O_TRUNC 0x200
//#define O_TTY_INIT
+// Non-POSIX
+#define O_DIRECT 0x4000
+
#define O_APPEND 0x400
#define O_DSYNC 0x1000
#define O_NONBLOCK 0x800
diff --git a/share/libc/langinfo.h b/share/libc/langinfo.h
new file mode 100644
index 0000000000000000000000000000000000000000..02ba80f8dd4e0db7938da86282f9079fac468324
--- /dev/null
+++ b/share/libc/langinfo.h
@@ -0,0 +1,163 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#ifndef __FC_LANGINFO_H
+#define __FC_LANGINFO_H
+#include "features.h"
+__PUSH_FC_STDLIB
+#include "__fc_define_locale_t.h"
+#include "nl_types.h"
+#include "locale.h" // for LC_CTYPE and other constants
+__BEGIN_DECLS
+
+
+#define _NL_ITEM(category, index) (((category) << 16) | (index))
+
+/* Extract the category and item index from a constructed `nl_item' value. */
+#define _NL_ITEM_CATEGORY(item) ((int) (item) >> 16)
+#define _NL_ITEM_INDEX(item) ((int) (item) & 0xffff)
+
+enum
+{
+ CODESET = (LC_CTYPE) << 16,
+#define CODESET CODESET
+ ABDAY_1 = (LC_TIME) << 16,
+#define ABDAY_1 ABDAY_1
+ ABDAY_2,
+#define ABDAY_2 ABDAY_2
+ ABDAY_3,
+#define ABDAY_3 ABDAY_3
+ ABDAY_4,
+#define ABDAY_4 ABDAY_4
+ ABDAY_5,
+#define ABDAY_5 ABDAY_5
+ ABDAY_6,
+#define ABDAY_6 ABDAY_6
+ ABDAY_7,
+#define ABDAY_7 ABDAY_7
+ DAY_1,
+#define DAY_1 DAY_1
+ DAY_2,
+#define DAY_2 DAY_2
+ DAY_3,
+#define DAY_3 DAY_3
+ DAY_4,
+#define DAY_4 DAY_4
+ DAY_5,
+#define DAY_5 DAY_5
+ DAY_6,
+#define DAY_6 DAY_6
+ DAY_7,
+#define DAY_7 DAY_7
+ ABMON_1,
+#define ABMON_1 ABMON_1
+ ABMON_2,
+#define ABMON_2 ABMON_2
+ ABMON_3,
+#define ABMON_3 ABMON_3
+ ABMON_4,
+#define ABMON_4 ABMON_4
+ ABMON_5,
+#define ABMON_5 ABMON_5
+ ABMON_6,
+#define ABMON_6 ABMON_6
+ ABMON_7,
+#define ABMON_7 ABMON_7
+ ABMON_8,
+#define ABMON_8 ABMON_8
+ ABMON_9,
+#define ABMON_9 ABMON_9
+ ABMON_10,
+#define ABMON_10 ABMON_10
+ ABMON_11,
+#define ABMON_11 ABMON_11
+ ABMON_12,
+#define ABMON_12 ABMON_12
+ MON_1,
+#define MON_1 MON_1
+ MON_2,
+#define MON_2 MON_2
+ MON_3,
+#define MON_3 MON_3
+ MON_4,
+#define MON_4 MON_4
+ MON_5,
+#define MON_5 MON_5
+ MON_6,
+#define MON_6 MON_6
+ MON_7,
+#define MON_7 MON_7
+ MON_8,
+#define MON_8 MON_8
+ MON_9,
+#define MON_9 MON_9
+ MON_10,
+#define MON_10 MON_10
+ MON_11,
+#define MON_11 MON_11
+ MON_12,
+#define MON_12 MON_12
+ AM_STR,
+#define AM_STR AM_STR
+ PM_STR,
+#define PM_STR PM_STR
+ D_T_FMT,
+#define D_T_FMT D_T_FMT
+ D_FMT,
+#define D_FMT D_FMT
+ T_FMT,
+#define T_FMT T_FMT
+ T_FMT_AMPM,
+#define T_FMT_AMPM T_FMT_AMPM
+ ERA,
+#define ERA ERA
+ ERA_YEAR, // Non-POSIX; GNU
+#define ERA_YEAR ERA_YEAR
+ ERA_D_FMT,
+#define ERA_D_FMT ERA_D_FMT
+ ALT_DIGITS,
+#define ALT_DIGITS ALT_DIGITS
+ ERA_D_T_FMT,
+#define ERA_D_T_FMT ERA_D_T_FMT
+ ERA_T_FMT,
+#define ERA_T_FMT ERA_T_FMT
+ DECIMAL_POINT = (LC_NUMERIC) << 16, // Non-POSIX; GNU
+#define DECIMAL_POINT DECIMAL_POINT
+ RADIXCHAR,
+#define RADIXCHAR RADIXCHAR
+ THOUSEP,
+#define THOUSEP THOUSEP
+ YESEXPR = (LC_MESSAGES) << 16,
+#define YESEXPR YESEXPR
+ NOEXPR,
+#define NOEXPR NOEXPR
+ CRNCYSTR = (LC_MONETARY) << 16,
+#define CRNCYSTR CRNCYSTR
+};
+
+extern char *nl_langinfo(nl_item item);
+extern char *nl_langinfo_l(nl_item item, locale_t locale);
+
+__END_DECLS
+
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/locale.h b/share/libc/locale.h
index ca23603228d31d79d2a1b3d2f2870df595cb9eb6..04b0e75495cd42e1db3f8f966a56a97f22afbede 100644
--- a/share/libc/locale.h
+++ b/share/libc/locale.h
@@ -24,7 +24,7 @@
#define __FC_LOCALE
#include "features.h"
__PUSH_FC_STDLIB
-
+#include "__fc_define_locale_t.h"
__BEGIN_DECLS
/* Structure giving information about numeric and monetary notation. */
@@ -149,6 +149,11 @@ extern char *setlocale(int category, const char *locale);
*/
extern struct lconv *localeconv(void);
+extern locale_t duplocale(locale_t);
+extern void freelocale(locale_t);
+extern locale_t newlocale(int, const char *, locale_t);
+extern locale_t uselocale(locale_t);
+
__END_DECLS
__POP_FC_STDLIB
diff --git a/share/libc/regex.h b/share/libc/regex.h
index c2bdf2b425113a938daa1de1d651b9641e966483..a08abdb485d329cf89f52d46e97939d2565e1e74 100644
--- a/share/libc/regex.h
+++ b/share/libc/regex.h
@@ -25,10 +25,16 @@
#include "features.h"
__PUSH_FC_STDLIB
#include "__fc_define_size_t.h"
-
+#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;
@@ -64,7 +70,15 @@ typedef enum __fc_reg_errcode_t
REG_ERPAREN
} reg_errcode_t;
-typedef int regoff_t;
+typedef ssize_t regoff_t;
+
+// Non-POSIX
+struct re_registers
+{
+ size_t num_regs;
+ regoff_t *start;
+ regoff_t *end;
+};
typedef struct __fc_regmatch_t
{
diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index e473fe89afb026b9a81774ef8121ac3ef6f43d3d..1596d1b195cb31ca7ad38fe24776998ea7c1034b 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 688c2885483ab84cac47bdaae2a7ad9d8582bb08..dcb1f4084932962daf4d28cf490db418ce640fa7 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 190c944be8249e58ea6a2fd5d15f9e330fc04f0c..b2deabaa9cae10a03be9003e0c3fb8aff4c61f48 100644
--- a/share/libc/sys/stat.h
+++ b/share/libc/sys/stat.h
@@ -104,6 +104,21 @@ extern mode_t umask(mode_t cmask);
#define S_TYPEISSHM(buf) ((buf)->st_mode - (buf)->st_mode)
#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)
+
+// Non-POSIX
+#define S_IFDOOR 0
+#define S_ISDOOR(m) 0
+
+// Non-POSIX
+#define UTIME_NOW ((1L << 30) - 1L)
+#define UTIME_OMIT ((1L << 30) - 2L)
+
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/sys/types.h b/share/libc/sys/types.h
index d540a3b9df7a7469f367a4bc69585a872a7546ab..929f09a019cc2393b6dd29a6ea34f1c27f2c80d1 100644
--- a/share/libc/sys/types.h
+++ b/share/libc/sys/types.h
@@ -50,10 +50,12 @@ typedef unsigned int u_int;
typedef unsigned short u_short;
typedef unsigned char u_char;
-// Note: makedev (non-POSIX) is usually a macro; in case of problems,
-// consider redefining this.
-/*@ assigns \result \from maj, min; */
-extern dev_t makedev(int maj, int min);
+// The macros below are non-POSIX; the definitions below should allow
+// parsing coreutils.
+# define major(dev) (((dev) >> 8) & 0xff)
+# define minor(dev) ((dev) & 0xff)
+# define makedev(maj, min) (((maj) << 8) | (min))
+
#define __u_char_defined
#endif
diff --git a/share/libc/sys/wait.h b/share/libc/sys/wait.h
index df14c934bc7579ada01667cb475a3f86acc24111..37ea46dc9ec1e4dbafeeded333052ba499c3677b 100644
--- a/share/libc/sys/wait.h
+++ b/share/libc/sys/wait.h
@@ -45,6 +45,9 @@ __BEGIN_DECLS
#define WNOWAIT 0x01000000
#define WSTOPPED 2
+// Non-POSIX
+#define WCOREDUMP(status) ((status) & 0x80)
+
#include "../__fc_define_id_t.h"
#include "../__fc_define_pid_t.h"
#include "../__fc_define_uid_and_gid.h"
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index 1c95f09bf73480d5684cfa49940cc34453c8cdbc..4cf7ead5fe4c5ea399386f19cd2578b3b1ce6a88 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -728,7 +728,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -755,7 +755,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -788,7 +788,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 34c9f132beba3a64708f52e4705daee7fb7a92a4..bf3ae7909b3b68131387e61208dc5f328ecf0e20 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -268,7 +268,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -295,7 +295,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -328,7 +328,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 18295663672294403e180049e24654af482ebd96..9bbf428995a5ecd80f66ec3e83d1ab883a221022 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -702,7 +702,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -729,7 +729,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -762,7 +762,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index 3a832d675a1e42a186e5034d6a7d03154b7cb5bb..765767f1d025073d70e44ddaac3d731d8506157a 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -242,7 +242,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -269,7 +269,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -302,7 +302,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
index 19dbb447c775cdf3cef0296249455486845756dc..c63be9146f50355689141c67e84aa8a5bd3673b7 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
@@ -11,10 +11,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index a8284618e550daae25f90434b93e89e3e99786e9..c9c93a0901d6ad3ed35316884eb6cf6090c5896f 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -44,10 +44,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 247fe7037ee8d8b4c19af56b986307549d5473f8..930d48cf15e4b7bbcf80d4af2564e9c99fc34e86 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -39,10 +39,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index 96325fbbbf3c10a63062b0076067e5fd1e6d8547..ace2bc58bc26deed40f0c82d6d2bf54e4365d4ea 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -42,10 +42,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index a33c96cfed628a46547dc226fafaf172a6a45d8a..87d5a40951cbea3902b5532c1fa6ecea3ab9206f 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -17,10 +17,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index d13ce9530e4af785dd7394dccfb56688d927f257..2326ab5b6bddfe11b47c128f6bb1b5e5b5061306 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -182,7 +182,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -209,7 +209,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -242,7 +242,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index d9a1a7302c53451bf506f1e44ee56fdcf09c9f9f..1e978e6e597763458d73bfa271c2fbcdc23c7fff 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -1071,7 +1071,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -1098,7 +1098,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -1131,7 +1131,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 57529e5daacfc80a51d916f693f84e7d15fdef13..7cffddb92f552e1957e8f4cf02fe661fd5b77ad3 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -80,10 +80,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index fb21a5a91f6cdbf509522b13d394901cedb616e4..317ebbe66ee547e29767c6eb6080210fb6a40396 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/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
index 9d0262aed46f6d6b2869db34f08acdd4d116a738..79b0b40397ed7b28352584ca5ec8a13ee719d0a6 100644
--- a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:118:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
Declaration of variadic function openat.
[variadic] fcntl.c:8:
Translating call to the specialized version fcntl(int, int).
diff --git a/src/plugins/variadic/tests/known/oracle/open.res.oracle b/src/plugins/variadic/tests/known/oracle/open.res.oracle
index 5702001954cb309a157ee842d7cde3c102424758..ff7c52d67ccbab097e52ec13f8fedcfe72369ff6 100644
--- a/src/plugins/variadic/tests/known/oracle/open.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:118:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
Declaration of variadic function openat.
[variadic] open.c:7:
Translating call to the specialized version open(char const *, int, mode_t).
diff --git a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
index ea5a7b2c33209a57f5432a405582b78bf96e56e4..45d5466519d6cf030ab1d1db40fa0f6daa0a3950 100644
--- a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:118:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
Declaration of variadic function openat.
[variadic] open_wrong.c:13: Warning:
No matching prototype found for this call to open.
diff --git a/src/plugins/variadic/tests/known/oracle/openat.res.oracle b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
index 2c5a0f9da014e84b2edeeb181838a7a7970e6925..9df27b194b91e66c4de695ee4451cdc078c7fde4 100644
--- a/src/plugins/variadic/tests/known/oracle/openat.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:118:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
Declaration of variadic function openat.
[variadic] openat.c:8:
Translating call to the specialized version openat(int, char const *, int, mode_t).
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index e6143dde67e0b9a42e104d3b0b83931442bc25b5..a129b3b58e801edd9676cad89e9d9020598cc59e 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -170,7 +170,6 @@
#include "stdlib.h"
#include "string.h"
#include "strings.h"
-#include "sys/types.h"
#include "time.h"
#include "wchar.h"
/*@ requires valid_read_string(format);
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index c966edbc370fcfa9931b8543bdcca3d12deccf87..813cf4c15be5ee6856815cd37365c99e63426633 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -47,7 +47,6 @@
#include "stdio.c"
#include "stdio.h"
#include "stdlib.h"
-#include "sys/types.h"
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 23ce1d6fe4b7b3497c76fcdd552788e964daeae5..89e599df66ea928defbcdf7a77f9ce637626df0e 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -53,6 +53,7 @@
#include "__fc_define_intptr_t.h"
#include "__fc_define_iovec.h"
#include "__fc_define_key_t.h"
+#include "__fc_define_locale_t.h"
#include "__fc_define_max_open_files.h"
#include "__fc_define_mode_t.h"
#include "__fc_define_nlink_t.h"
@@ -97,6 +98,7 @@
#include "ifaddrs.h"
#include "inttypes.h"
#include "iso646.h"
+#include "langinfo.h"
#include "libgen.h"
#include "limits.h"
#include "locale.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index eaeeebc57c865f7366b0125fa9ecd8769abf7639..3e6a3b4a237eaa671cc9ff9c55b502ba39483e65 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,16 +4,16 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] fc_libc.c:167: assertion got status valid.
-[eva] fc_libc.c:168: assertion got status valid.
[eva] fc_libc.c:169: assertion got status valid.
[eva] fc_libc.c:170: assertion got status valid.
+[eva] fc_libc.c:171: assertion got status valid.
+[eva] fc_libc.c:172: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[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);
@@ -64,7 +64,7 @@
wcslen (3 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (1 call);
wmemset (0 call);
- Specified-only functions (428)
+ Specified-only functions (427)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -141,17 +141,16 @@
log (0 call); log10 (0 call); log10f (0 call); log10l (0 call);
log2 (0 call); log2f (0 call); log2l (0 call); logf (0 call); logl (0 call);
longjmp (0 call); lrand48 (0 call); lseek (0 call); lstat (0 call);
- makedev (0 call); malloc (13 calls); mblen (0 call); mbstowcs (0 call);
- mbtowc (0 call); mkdir (0 call); mkfifo (0 call); mknod (0 call);
- mkstemp (0 call); mktime (0 call); mrand48 (0 call); nan (0 call);
- nanf (0 call); nanl (0 call); nanosleep (0 call); nrand48 (0 call);
- ntohl (0 call); ntohs (0 call); open (0 call); openat (0 call);
- opendir (0 call); openlog (0 call); pathconf (0 call); pclose (0 call);
- perror (0 call); pipe (0 call); poll (0 call); popen (0 call); pow (0 call);
- powf (0 call); pthread_cond_broadcast (0 call);
- pthread_cond_destroy (0 call); pthread_cond_init (0 call);
- pthread_cond_wait (0 call); pthread_create (0 call);
- pthread_getname_np (0 call); pthread_join (0 call);
+ malloc (13 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+ mkdir (0 call); mkfifo (0 call); mknod (0 call); mkstemp (0 call);
+ mktime (0 call); mrand48 (0 call); nan (0 call); nanf (0 call);
+ nanl (0 call); nanosleep (0 call); nrand48 (0 call); ntohl (0 call);
+ ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
+ openlog (0 call); pathconf (0 call); pclose (0 call); perror (0 call);
+ pipe (0 call); poll (0 call); popen (0 call); pow (0 call); powf (0 call);
+ pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
+ pthread_cond_init (0 call); pthread_cond_wait (0 call);
+ pthread_create (0 call); pthread_getname_np (0 call); pthread_join (0 call);
pthread_mutex_destroy (0 call); pthread_mutex_init (0 call);
pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call);
pthread_mutexattr_destroy (0 call); pthread_mutexattr_init (0 call);
@@ -214,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
+ Assignment = 718
+ Exit point = 129
Function = 557
- Function call = 165
+ 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 c4986b27502f39b78667dc392d8fcf35ccac5af0..880d36bf6a6a100cec73e2e8253496fb152a4d5d 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);
@@ -6698,10 +6700,6 @@ ssize_t getline(char **lineptr, size_t *n, FILE *stream);
int asprintf(char **strp, char const *fmt, void * const *__va_params);
-/*@ assigns \result;
- assigns \result \from maj, min; */
-extern dev_t makedev(int maj, int min);
-
FILE __fc_initial_stdout =
{.__fc_FILE_id = (unsigned int)1, .__fc_FILE_data = 0U};
FILE *__fc_stdout = & __fc_initial_stdout;
@@ -7222,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/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 58fab9624e5211f9e3545690c86120ab90421e36..19a092a2d83bdbd6279b2825c8cd7ef4370fd5f7 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -15,6 +15,7 @@
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_intptr_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_iovec.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_key_t.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_locale_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_max_open_files.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_mode_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_nlink_t.h (with preprocessing)
@@ -70,6 +71,7 @@ skipping FRAMAC_SHARE/libc/complex.h
[kernel] Parsing FRAMAC_SHARE/libc/ifaddrs.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/inttypes.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/iso646.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/langinfo.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/libgen.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/limits.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/locale.h (with preprocessing)
diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle
index 455e3224fdcdbca6d7a56e1c485c104266d6804e..de5dc645871557d472e178e5336116a5d5d47305 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 6591da2a4ba55bff3530364588638f54f4dae4d4..989193e4adde5c3bcb87e206fa2249a041be1f47 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 01861ff92b210e6a56013802b3f39aa96076880d..38d0c05207233c440dcf4b0908f70da89082c1b1 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/oracle/sys_types.res.oracle b/tests/libc/oracle/sys_types.res.oracle
index bd50338df61de05aec784e2b28936ef4509bacce..43690a9dd32cb238190785c2661e9ff6248824c1 100644
--- a/tests/libc/oracle/sys_types.res.oracle
+++ b/tests/libc/oracle/sys_types.res.oracle
@@ -4,13 +4,9 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] computing for function makedev <- main.
- Called from sys_types.c:4.
-[eva] using specification for function makedev
-[eva] Done for function makedev
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- dev ∈ [--..--]
+ dev ∈ {298}
__retres ∈ {0}
diff --git a/tests/libc/stdlib_c.c b/tests/libc/stdlib_c.c
index 33dc8110214a11851008f465801601bf39f23e1b..065ed34d5cfc5f024dd837451311dc1bae16123c 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;
}