diff --git a/share/compliance/nonstandard_identifiers.json b/share/compliance/nonstandard_identifiers.json
index 5ad01f743fb6656c7998c00cd85e74c4ebc1b8ba..86e2fa0eb0e2e8a23c8a81fac8a57a6a7f1ddc44 100644
--- a/share/compliance/nonstandard_identifiers.json
+++ b/share/compliance/nonstandard_identifiers.json
@@ -3,6 +3,10 @@
"source":"Manpages, mostly Linux and BSD",
"data":{
"arc4random_buf": {"header":"stdlib.h"},
+ "error": {"header":"error.h"},
+ "error_at_line": {"header":"error.h"},
+ "error_message_count": {"header":"error.h"},
+ "error_one_per_line": {"header":"error.h"},
"facilitynames": {"header":"syslog.h"},
"getresgid": {"header":"unistd.h"},
"getresuid": {"header":"unistd.h"},
diff --git a/share/dune b/share/dune
index e7ab88d2f418b70fb4584b78a7bd9c3847aa6271..95125fc8c20bb374433ef4026abe51a2fd2e93f7 100644
--- a/share/dune
+++ b/share/dune
@@ -107,6 +107,7 @@
(libc/__fc_define_key_t.h as libc/__fc_define_key_t.h)
(libc/__fc_define_locale_t.h as libc/__fc_define_locale_t.h)
(libc/__fc_define_max_open_files.h as libc/__fc_define_max_open_files.h)
+(libc/__fc_define_mbstate_t.h as libc/__fc_define_mbstate_t.h)
(libc/__fc_define_mode_t.h as libc/__fc_define_mode_t.h)
(libc/__fc_define_nlink_t.h as libc/__fc_define_nlink_t.h)
(libc/__fc_define_null.h as libc/__fc_define_null.h)
@@ -154,6 +155,8 @@
(libc/err.h as libc/err.h)
(libc/errno.c as libc/errno.c)
(libc/errno.h as libc/errno.h)
+(libc/error.c as libc/error.c)
+(libc/error.h as libc/error.h)
(libc/fcntl.h as libc/fcntl.h)
(libc/features.h as libc/features.h)
(libc/fenv.c as libc/fenv.c)
@@ -254,6 +257,7 @@
(libc/time.c as libc/time.c)
(libc/time.h as libc/time.h)
(libc/trace.h as libc/trace.h)
+(libc/uchar.h as libc/uchar.h)
(libc/ulimit.h as libc/ulimit.h)
(libc/unistd.c as libc/unistd.c)
(libc/unistd.h as libc/unistd.h)
diff --git a/share/libc/__fc_define_mbstate_t.h b/share/libc/__fc_define_mbstate_t.h
new file mode 100644
index 0000000000000000000000000000000000000000..5fe1ddb1136990ffc2c68a1c9a9f413995b86757
--- /dev/null
+++ b/share/libc/__fc_define_mbstate_t.h
@@ -0,0 +1,35 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2024 */
+/* 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_MBSTATE_T
+#define __FC_DEFINE_MBSTATE_T
+#include "features.h"
+__PUSH_FC_STDLIB
+#include "__fc_machdep.h"
+__BEGIN_DECLS
+#ifndef __mbstate_t_defined
+typedef struct __fc_mbstate_t { int __count; char __value[4]; } mbstate_t;
+#define __mbstate_t_defined
+#endif
+__END_DECLS
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
index 8157b6347b9d8499ae41e55132d1363b6b7b480f..781e13c54f09f69022ec5be07ef58aa105d96d45 100644
--- a/share/libc/__fc_libc.h
+++ b/share/libc/__fc_libc.h
@@ -41,6 +41,7 @@
#include "endian.h"
#include "err.h"
#include "errno.h"
+#include "error.h"
#include "fcntl.h"
#include "features.h"
#include "fenv.h"
@@ -126,6 +127,7 @@
//#include "tgmath.h"
#include "time.h"
#include "trace.h"
+#include "uchar.h"
#include "ulimit.h"
#include "unistd.h"
#include "utime.h"
diff --git a/share/libc/__fc_runtime.c b/share/libc/__fc_runtime.c
index dfc6cf363c96f8fff21774df9946a30896e881c5..71a948e1e90f7a829ca2bb1fac7d68095c19d35f 100644
--- a/share/libc/__fc_runtime.c
+++ b/share/libc/__fc_runtime.c
@@ -25,6 +25,7 @@
#include "assert.c"
#include "ctype.c"
#include "errno.c"
+#include "error.c"
#include "fenv.c"
#include "glob.c"
#include "inttypes.c"
diff --git a/share/libc/error.c b/share/libc/error.c
new file mode 100644
index 0000000000000000000000000000000000000000..95697210d2c74312fd1706c50cd94ec9b4a0b551
--- /dev/null
+++ b/share/libc/error.c
@@ -0,0 +1,29 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2024 */
+/* 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). */
+/* */
+/**************************************************************************/
+
+#include "error.h"
+__PUSH_FC_STDLIB
+
+unsigned int error_message_count = 0;
+int error_one_per_line = 0;
+
+__POP_FC_STDLIB
diff --git a/share/libc/error.h b/share/libc/error.h
new file mode 100644
index 0000000000000000000000000000000000000000..3542df0333395d3ac91a231bdba59709bfbb8808
--- /dev/null
+++ b/share/libc/error.h
@@ -0,0 +1,53 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2024 */
+/* 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). */
+/* */
+/**************************************************************************/
+
+/* Non-POSIX; glibc definitions */
+
+#ifndef __FC_ERROR_H
+#define __FC_ERROR_H
+#include "features.h"
+__PUSH_FC_STDLIB
+#include "__fc_machdep.h"
+
+__BEGIN_DECLS
+
+extern unsigned int error_message_count;
+
+extern int error_one_per_line;
+
+/*@
+ assigns error_message_count \from error_message_count;
+*/
+extern void error(int __status, int __errnum, const char *__format, ...);
+
+/*@
+ assigns error_message_count \from error_message_count;
+*/
+extern void error_at_line(int __status, int __errnum, const char *__fname,
+ unsigned int __lineno, const char *__format, ...);
+
+extern void (*error_print_progname)(void);
+
+__END_DECLS
+
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/uchar.h b/share/libc/uchar.h
new file mode 100644
index 0000000000000000000000000000000000000000..c24d5ebc42d4aaf981f9b17dd2e09df4877efd05
--- /dev/null
+++ b/share/libc/uchar.h
@@ -0,0 +1,126 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2024 */
+/* 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). */
+/* */
+/**************************************************************************/
+
+/* C11 */
+#ifndef __FC_UCHAR_H
+#define __FC_UCHAR_H
+
+#include "features.h"
+__PUSH_FC_STDLIB
+#include "__fc_define_mbstate_t.h"
+#include "__fc_define_size_t.h"
+#include "errno.h"
+
+__BEGIN_DECLS
+
+#define __STDC_VERSION_UCHAR_H__ 202311L
+
+#ifndef __cpp_char8_t
+typedef unsigned char char8_t;
+#endif
+
+#ifndef __USE_ISOCXX11
+typedef __UINT_LEAST16_T char16_t;
+typedef __UINT_LEAST16_T char32_t;
+#endif
+
+/* C23 7.30.1 "...If ps is a null pointer, each function uses its own
+ internal mbstate_t object..."
+*/
+mbstate_t __fc_mbrtoc8_internal_mbstate;
+mbstate_t __fc_c8rtomb_internal_mbstate;
+mbstate_t __fc_mbrtoc16_internal_mbstate;
+mbstate_t __fc_c16rtomb_internal_mbstate;
+mbstate_t __fc_mbrtoc32_internal_mbstate;
+mbstate_t __fc_c32rtomb_internal_mbstate;
+
+/* C23 7.30.1.2 / 7.30.1.4 / 7.30.1.6 : If s is a null pointer, the c8rtomb,
+ c16rtomb and c32rtomb function are using an internal buffer instead.
+*/
+char __fc_c8rtomb_internal_buf[__FC_MB_CUR_MAX];
+char __fc_c16rtomb_internal_buf[__FC_MB_CUR_MAX];
+char __fc_c32rtomb_internal_buf[__FC_MB_CUR_MAX];
+
+/*@
+ assigns pc8[0], *ps, __fc_mbrtoc8_internal_mbstate
+ \from indirect:pc8, s[0 .. n-1], indirect:n, indirect:ps, *ps,
+ __fc_mbrtoc8_internal_mbstate;
+ assigns \result, errno \from indirect:s[0 .. n-1], indirect:n, indirect:ps,
+ indirect:*ps, indirect:__fc_mbrtoc8_internal_mbstate;
+*/
+extern size_t mbrtoc8(char8_t *restrict pc8, const char *restrict s, size_t n,
+ mbstate_t *restrict ps);
+
+/*@
+ assigns s[0 .. __FC_MB_CUR_MAX-1], *ps, __fc_c8rtomb_internal_mbstate,
+ __fc_c8rtomb_internal_buf[0 .. __FC_MB_CUR_MAX-1]
+ \from indirect:s, c8, indirect:ps, *ps, __fc_c8rtomb_internal_mbstate,
+ __fc_c8rtomb_internal_buf[0 .. __FC_MB_CUR_MAX-1];
+ assigns \result, errno \from indirect:c8, indirect:ps,
+ indirect:*ps, indirect:__fc_c8rtomb_internal_mbstate;
+*/
+extern size_t c8rtomb(char *restrict s, char8_t c8, mbstate_t *restrict ps);
+
+/*@
+ assigns pc16[0], *ps, __fc_mbrtoc16_internal_mbstate
+ \from indirect:pc16, s[0 .. n-1], indirect:n, indirect:ps, *ps,
+ __fc_mbrtoc16_internal_mbstate;
+ assigns \result, errno \from indirect:s[0 .. n-1], indirect:n, indirect:ps,
+ indirect:*ps, indirect:__fc_mbrtoc16_internal_mbstate;
+*/
+extern size_t mbrtoc16(char16_t *restrict pc16, const char *restrict s,
+ size_t n, mbstate_t *restrict ps);
+
+/*@
+ assigns s[0 .. __FC_MB_CUR_MAX-1], *ps, __fc_c16rtomb_internal_mbstate,
+ __fc_c16rtomb_internal_buf[0 .. __FC_MB_CUR_MAX-1]
+ \from indirect:s, c16, indirect:ps, *ps, __fc_c16rtomb_internal_mbstate,
+ __fc_c16rtomb_internal_buf[0 .. __FC_MB_CUR_MAX-1];
+ assigns \result, errno \from indirect:c16, indirect:ps,
+ indirect:*ps, indirect:__fc_c16rtomb_internal_mbstate;
+*/
+extern size_t c16rtomb(char *restrict s, char16_t c16, mbstate_t *restrict ps);
+
+
+/*@
+ assigns pc32[0], *ps, __fc_mbrtoc32_internal_mbstate
+ \from indirect:pc32, s[0 .. n-1], indirect:n, indirect:ps, *ps,
+ __fc_mbrtoc32_internal_mbstate;
+ assigns \result, errno \from indirect:s[0 .. n-1], indirect:n, indirect:ps,
+ indirect:*ps, indirect:__fc_mbrtoc32_internal_mbstate;
+*/
+extern size_t mbrtoc32(char32_t *restrict pc32, const char *restrict s,
+ size_t n, mbstate_t *restrict ps);
+/*@
+ assigns s[0 .. __FC_MB_CUR_MAX-1], *ps, __fc_c32rtomb_internal_mbstate,
+ __fc_c32rtomb_internal_buf[0 .. __FC_MB_CUR_MAX-1]
+ \from indirect:s, c32, indirect:ps, *ps, __fc_c32rtomb_internal_mbstate,
+ __fc_c32rtomb_internal_buf[0 .. __FC_MB_CUR_MAX-1];
+ assigns \result, errno \from indirect:c32, indirect:ps,
+ indirect:*ps, indirect:__fc_c32rtomb_internal_mbstate;
+*/
+extern size_t c32rtomb(char *restrict s, char32_t c32, mbstate_t *restrict ps);
+
+__END_DECLS
+
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/wchar.h b/share/libc/wchar.h
index 89bbba4df2e0a158c99d07b13b969683f51a48ba..8a9b4d122488c6dc87674e33330024a64523d6e0 100644
--- a/share/libc/wchar.h
+++ b/share/libc/wchar.h
@@ -26,6 +26,7 @@
#include "features.h"
__PUSH_FC_STDLIB
+#include "__fc_define_mbstate_t.h"
#include "__fc_define_wchar_t.h"
#include "__fc_define_wint_t.h"
#include "__fc_define_size_t.h"
@@ -304,11 +305,6 @@ extern int fwscanf(FILE * stream, const wchar_t * format, ...);
extern int swscanf(const wchar_t * str, const wchar_t * format, ...);
-#ifndef __mbstate_t_defined
-typedef struct __fc_mbstate_t { int __count; char __value[4]; } mbstate_t;
-#define __mbstate_t_defined
-#endif
-
__END_DECLS
__POP_FC_STDLIB
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 00a916d66f04b9e80fda0b2e932f9c9f0f0f693a..898a29b51911c3b5427d6035edd1ddecef844211 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:294:
+[variadic] FRAMAC_SHARE/libc/wchar.h:295:
Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:296:
+[variadic] FRAMAC_SHARE/libc/wchar.h:297:
Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:298:
+[variadic] FRAMAC_SHARE/libc/wchar.h:299:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:301:
+[variadic] FRAMAC_SHARE/libc/wchar.h:302:
Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:303:
+[variadic] FRAMAC_SHARE/libc/wchar.h:304:
Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:305:
+[variadic] FRAMAC_SHARE/libc/wchar.h:306:
Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index dc5aa4bc442e933bfd48886bf346e8db86cd04ff..2fadf3268d0e688c8bd91dc92068b40283de472d 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:294:
+[variadic] FRAMAC_SHARE/libc/wchar.h:295:
Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:296:
+[variadic] FRAMAC_SHARE/libc/wchar.h:297:
Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:298:
+[variadic] FRAMAC_SHARE/libc/wchar.h:299:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:301:
+[variadic] FRAMAC_SHARE/libc/wchar.h:302:
Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:303:
+[variadic] FRAMAC_SHARE/libc/wchar.h:304:
Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:305:
+[variadic] FRAMAC_SHARE/libc/wchar.h:306:
Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
@@ -35,7 +35,7 @@
[eva] Analyzing a complete application starting at main
[eva] using specification for function wmemset
[eva] using specification for function swprintf_va_1
-[eva] FRAMAC_SHARE/libc/wchar.h:296:
+[eva] FRAMAC_SHARE/libc/wchar.h:297:
Cannot evaluate range bound wformat_length(format) - 1
(unsupported ACSL construct: logic function wformat_length). Approximating
[eva:alarm] swprintf.c:12: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index e845bbf02f0ea226aabc42339cdb937ebb3eadc2..d0f176337a2ca9f69d21f3fb705bed9e90ce5c98 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:294:
+[variadic] FRAMAC_SHARE/libc/wchar.h:295:
Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:296:
+[variadic] FRAMAC_SHARE/libc/wchar.h:297:
Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:298:
+[variadic] FRAMAC_SHARE/libc/wchar.h:299:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:301:
+[variadic] FRAMAC_SHARE/libc/wchar.h:302:
Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:303:
+[variadic] FRAMAC_SHARE/libc/wchar.h:304:
Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:305:
+[variadic] FRAMAC_SHARE/libc/wchar.h:306:
Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 37e879fb7c48f7045b3d0783e4a079384fd0c5f6..4d4ec0cf07d92c0344595dcdd9293b208b31905e 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -45,6 +45,7 @@
#include "endian.h"
#include "err.h"
#include "errno.h"
+#include "error.h"
#include "__fc_alloc_axiomatic.h"
#include "__fc_builtin.h"
#include "__fc_define_blkcnt_t.h"
@@ -64,6 +65,7 @@
#include "__fc_define_key_t.h"
#include "__fc_define_locale_t.h"
#include "__fc_define_max_open_files.h"
+#include "__fc_define_mbstate_t.h"
#include "__fc_define_mode_t.h"
#include "__fc_define_nlink_t.h"
#include "__fc_define_null.h"
@@ -179,6 +181,7 @@
#include "tgmath.h"
#include "time.h"
#include "trace.h"
+#include "uchar.h"
#include "ulimit.h"
#include "unistd.h"
#include "utime.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 9753e12ffebb6769813519d2da15a91fd2e5520c..4c4b48b4a96e7f0109a58850892b12cab68aed18 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -5,10 +5,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] fc_libc.c:206: assertion got status valid.
-[eva] fc_libc.c:207: assertion got status valid.
-[eva] fc_libc.c:208: assertion got status valid.
[eva] fc_libc.c:209: assertion got status valid.
+[eva] fc_libc.c:210: assertion got status valid.
+[eva] fc_libc.c:211: assertion got status valid.
+[eva] fc_libc.c:212: assertion got status valid.
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -32,6 +32,8 @@
#include "err.h"
#include "errno.c"
#include "errno.h"
+#include "error.c"
+#include "error.h"
#include "fcntl.h"
#include "fenv.c"
#include "fenv.h"
@@ -85,6 +87,7 @@
#include "syslog.h"
#include "termios.h"
#include "time.h"
+#include "uchar.h"
#include "unistd.c"
#include "unistd.h"
#include "wchar.c"
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index f4b1572e418b5308dc78d9bdcfb09af9413e108a..09cc0099892aaa99ba920608a4d093ec6c57584b 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -18,6 +18,7 @@
[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_mbstate_t.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)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_null.h (with preprocessing)
@@ -60,6 +61,7 @@ skipping FRAMAC_SHARE/libc/complex.h
[kernel] Parsing FRAMAC_SHARE/libc/endian.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/err.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/errno.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/error.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/fcntl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/features.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/fenv.h (with preprocessing)
@@ -145,6 +147,7 @@ skipping FRAMAC_SHARE/libc/complex.h
skipping FRAMAC_SHARE/libc/tgmath.h
[kernel] Parsing FRAMAC_SHARE/libc/time.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/trace.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/uchar.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/ulimit.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/unistd.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/utime.h (with preprocessing)
diff --git a/tests/libc/oracle/fc_libc.4.res.oracle b/tests/libc/oracle/fc_libc.4.res.oracle
index 3f2a38d68becdef4bd703f7a9746a195706af948..862bb1b108efc0888a12d7e72e38f0f481f10bc5 100644
--- a/tests/libc/oracle/fc_libc.4.res.oracle
+++ b/tests/libc/oracle/fc_libc.4.res.oracle
@@ -4,3 +4,5 @@
[kernel] Parsing glibc_functions.json
[kernel] Parsing posix_identifiers.json
[kernel] Parsing nonstandard_identifiers.json
+[kernel] Warning: <uchar.h>:c8rtomb : unknown identifier
+[kernel] Warning: <uchar.h>:mbrtoc8 : unknown identifier
diff --git a/tests/libc/oracle/uchar_h.res.oracle b/tests/libc/oracle/uchar_h.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..82a0ae391735acd03045073e97a1f0bf7b214cc4
--- /dev/null
+++ b/tests/libc/oracle/uchar_h.res.oracle
@@ -0,0 +1,150 @@
+[kernel] Parsing uchar_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function mbrtoc8 <- main.
+ Called from uchar_h.c:10.
+[eva] using specification for function mbrtoc8
+[eva:invalid-assigns] uchar_h.c:10:
+ Completely invalid destination for assigns clause *ps. Ignoring.
+[eva] Done for function mbrtoc8
+[eva] computing for function mbrtoc8 <- main.
+ Called from uchar_h.c:11.
+[eva] Done for function mbrtoc8
+[eva] computing for function mbrtoc8 <- main.
+ Called from uchar_h.c:12.
+[eva:invalid-assigns] uchar_h.c:12:
+ Completely invalid destination for assigns clause *(pc8 + 0). Ignoring.
+[eva] Done for function mbrtoc8
+[eva] computing for function mbrtoc8 <- main.
+ Called from uchar_h.c:13.
+[eva:invalid-assigns] uchar_h.c:13:
+ Completely invalid destination for assigns clause *(pc8 + 0). Ignoring.
+[eva:invalid-assigns] uchar_h.c:13:
+ Completely invalid destination for assigns clause *ps. Ignoring.
+[eva] Done for function mbrtoc8
+[eva] computing for function c8rtomb <- main.
+ Called from uchar_h.c:14.
+[eva] using specification for function c8rtomb
+[eva] Done for function c8rtomb
+[eva] computing for function c8rtomb <- main.
+ Called from uchar_h.c:15.
+[eva:invalid-assigns] uchar_h.c:15:
+ Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
+ Ignoring.
+[eva] Done for function c8rtomb
+[eva] computing for function c8rtomb <- main.
+ Called from uchar_h.c:16.
+[eva:invalid-assigns] uchar_h.c:16:
+ Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
+ Ignoring.
+[eva:invalid-assigns] uchar_h.c:16:
+ Completely invalid destination for assigns clause *ps. Ignoring.
+[eva] Done for function c8rtomb
+[eva] computing for function mbrtoc16 <- main.
+ Called from uchar_h.c:20.
+[eva] using specification for function mbrtoc16
+[eva:invalid-assigns] uchar_h.c:20:
+ Completely invalid destination for assigns clause *ps. Ignoring.
+[eva] Done for function mbrtoc16
+[eva] computing for function mbrtoc16 <- main.
+ Called from uchar_h.c:21.
+[eva] Done for function mbrtoc16
+[eva] computing for function mbrtoc16 <- main.
+ Called from uchar_h.c:22.
+[eva:invalid-assigns] uchar_h.c:22:
+ Completely invalid destination for assigns clause *(pc16 + 0). Ignoring.
+[eva] Done for function mbrtoc16
+[eva] computing for function mbrtoc16 <- main.
+ Called from uchar_h.c:23.
+[eva:invalid-assigns] uchar_h.c:23:
+ Completely invalid destination for assigns clause *(pc16 + 0). Ignoring.
+[eva:invalid-assigns] uchar_h.c:23:
+ Completely invalid destination for assigns clause *ps. Ignoring.
+[eva] Done for function mbrtoc16
+[eva] computing for function c16rtomb <- main.
+ Called from uchar_h.c:24.
+[eva] using specification for function c16rtomb
+[eva] Done for function c16rtomb
+[eva] computing for function c16rtomb <- main.
+ Called from uchar_h.c:25.
+[eva:invalid-assigns] uchar_h.c:25:
+ Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
+ Ignoring.
+[eva] Done for function c16rtomb
+[eva] computing for function c16rtomb <- main.
+ Called from uchar_h.c:26.
+[eva:invalid-assigns] uchar_h.c:26:
+ Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
+ Ignoring.
+[eva:invalid-assigns] uchar_h.c:26:
+ Completely invalid destination for assigns clause *ps. Ignoring.
+[eva] Done for function c16rtomb
+[eva] computing for function mbrtoc32 <- main.
+ Called from uchar_h.c:30.
+[eva] using specification for function mbrtoc32
+[eva:invalid-assigns] uchar_h.c:30:
+ Completely invalid destination for assigns clause *ps. Ignoring.
+[eva] Done for function mbrtoc32
+[eva] computing for function mbrtoc32 <- main.
+ Called from uchar_h.c:31.
+[eva] Done for function mbrtoc32
+[eva] computing for function mbrtoc32 <- main.
+ Called from uchar_h.c:32.
+[eva:invalid-assigns] uchar_h.c:32:
+ Completely invalid destination for assigns clause *(pc32 + 0). Ignoring.
+[eva] Done for function mbrtoc32
+[eva] computing for function mbrtoc32 <- main.
+ Called from uchar_h.c:33.
+[eva:invalid-assigns] uchar_h.c:33:
+ Completely invalid destination for assigns clause *(pc32 + 0). Ignoring.
+[eva:invalid-assigns] uchar_h.c:33:
+ Completely invalid destination for assigns clause *ps. Ignoring.
+[eva] Done for function mbrtoc32
+[eva] computing for function c32rtomb <- main.
+ Called from uchar_h.c:34.
+[eva] using specification for function c32rtomb
+[eva] Done for function c32rtomb
+[eva] computing for function c32rtomb <- main.
+ Called from uchar_h.c:35.
+[eva:invalid-assigns] uchar_h.c:35:
+ Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
+ Ignoring.
+[eva] Done for function c32rtomb
+[eva] computing for function c32rtomb <- main.
+ Called from uchar_h.c:36.
+[eva:invalid-assigns] uchar_h.c:36:
+ Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
+ Ignoring.
+[eva:invalid-assigns] uchar_h.c:36:
+ Completely invalid destination for assigns clause *ps. Ignoring.
+[eva] Done for function c32rtomb
+[eva] Recording results for main
+[eva] Done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __fc_errno ∈ [--..--]
+ __fc_mbrtoc8_internal_mbstate ∈ [--..--]
+ __fc_c8rtomb_internal_mbstate ∈ [--..--]
+ __fc_mbrtoc16_internal_mbstate ∈ [--..--]
+ __fc_c16rtomb_internal_mbstate ∈ [--..--]
+ __fc_mbrtoc32_internal_mbstate ∈ [--..--]
+ __fc_c32rtomb_internal_mbstate ∈ [--..--]
+ __fc_c8rtomb_internal_buf[0..15] ∈ [--..--]
+ __fc_c16rtomb_internal_buf[0..15] ∈ [--..--]
+ __fc_c32rtomb_internal_buf[0..15] ∈ [--..--]
+ st ∈ [--..--]
+ r ∈ [--..--]
+ buf[0..9] ∈ [--..--] or UNINITIALIZED
+ pc8[0] ∈ [--..--] or UNINITIALIZED
+ [1..9] ∈ UNINITIALIZED
+ c8 ∈ {0}
+ pc16[0] ∈ [--..--] or UNINITIALIZED
+ [1..9] ∈ UNINITIALIZED
+ c16 ∈ {0}
+ pc32[0] ∈ [--..--] or UNINITIALIZED
+ [1..9] ∈ UNINITIALIZED
+ c32 ∈ {0}
+ __retres ∈ {0}
diff --git a/tests/libc/uchar_h.c b/tests/libc/uchar_h.c
new file mode 100644
index 0000000000000000000000000000000000000000..eb567dbd25f93882f19fb58f0e9bdc5c68bf6c4f
--- /dev/null
+++ b/tests/libc/uchar_h.c
@@ -0,0 +1,39 @@
+#include <uchar.h>
+
+int main() {
+ mbstate_t st = {0};
+ size_t r;
+ char buf[10];
+
+ char8_t pc8[10];
+ char8_t c8 = {0};
+ r = mbrtoc8(pc8, "bla", 3, 0);
+ r = mbrtoc8(pc8, "bla", 3, &st);
+ r = mbrtoc8(0, 0, 3, &st);
+ r = mbrtoc8(0, "", 1, 0);
+ r = c8rtomb(buf, c8, &st);
+ r = c8rtomb(0, c8, &st);
+ r = c8rtomb(0, c8, 0);
+
+ char16_t pc16[10];
+ char16_t c16 = {0};
+ r = mbrtoc16(pc16, "bla", 3, 0);
+ r = mbrtoc16(pc16, "bla", 3, &st);
+ r = mbrtoc16(0, 0, 3, &st);
+ r = mbrtoc16(0, "", 1, 0);
+ r = c16rtomb(buf, c16, &st);
+ r = c16rtomb(0, c16, &st);
+ r = c16rtomb(0, c16, 0);
+
+ char32_t pc32[10];
+ char32_t c32 = {0};
+ r = mbrtoc32(pc32, "bla", 3, 0);
+ r = mbrtoc32(pc32, "bla", 3, &st);
+ r = mbrtoc32(0, 0, 3, &st);
+ r = mbrtoc32(0, "", 1, 0);
+ r = c32rtomb(buf, c32, &st);
+ r = c32rtomb(0, c32, &st);
+ r = c32rtomb(0, c32, 0);
+
+ return 0;
+}