From 38e15162e3d5390c5fee1a93bf81a1311a17a117 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 16 Jul 2024 10:45:00 +0200
Subject: [PATCH] [libc] add some C11, C23 and glibc headers/definitions
---
share/compliance/nonstandard_identifiers.json | 4 +
share/dune | 4 +
share/libc/__fc_define_mbstate_t.h | 35 ++++
share/libc/__fc_libc.h | 2 +
share/libc/__fc_runtime.c | 1 +
share/libc/error.c | 29 ++++
share/libc/error.h | 53 +++++++
share/libc/uchar.h | 126 +++++++++++++++
share/libc/wchar.h | 6 +-
.../tests/known/oracle/printf.res.oracle | 12 +-
.../tests/known/oracle/swprintf.res.oracle | 14 +-
.../tests/known/oracle/wchar.res.oracle | 12 +-
tests/libc/fc_libc.c | 3 +
tests/libc/oracle/fc_libc.0.res.oracle | 9 +-
tests/libc/oracle/fc_libc.2.res.oracle | 3 +
tests/libc/oracle/fc_libc.4.res.oracle | 2 +
tests/libc/oracle/uchar_h.res.oracle | 150 ++++++++++++++++++
tests/libc/uchar_h.c | 39 +++++
18 files changed, 477 insertions(+), 27 deletions(-)
create mode 100644 share/libc/__fc_define_mbstate_t.h
create mode 100644 share/libc/error.c
create mode 100644 share/libc/error.h
create mode 100644 share/libc/uchar.h
create mode 100644 tests/libc/oracle/uchar_h.res.oracle
create mode 100644 tests/libc/uchar_h.c
diff --git a/share/compliance/nonstandard_identifiers.json b/share/compliance/nonstandard_identifiers.json
index 5ad01f743fb..86e2fa0eb0e 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 e7ab88d2f41..95125fc8c20 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 00000000000..5fe1ddb1136
--- /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 8157b6347b9..781e13c54f0 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 dfc6cf363c9..71a948e1e90 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 00000000000..95697210d2c
--- /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 00000000000..3542df03333
--- /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 00000000000..c24d5ebc42d
--- /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 89bbba4df2e..8a9b4d12248 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 00a916d66f0..898a29b5191 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 dc5aa4bc442..2fadf3268d0 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 e845bbf02f0..d0f176337a2 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 37e879fb7c4..4d4ec0cf07d 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 9753e12ffeb..4c4b48b4a96 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 f4b1572e418..09cc0099892 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 3f2a38d68be..862bb1b108e 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 00000000000..82a0ae39173
--- /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 00000000000..eb567dbd25f
--- /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;
+}
--
GitLab