[libc] add some C11, C23 and glibc headers/definitions

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"},

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)

share/libc/__fc_define_mbstate_t.h

+/**************************************************************************/
+/*                                                                        */
+/*  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

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"

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"

share/libc/error.c

+/**************************************************************************/
+/*                                                                        */
+/*  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

share/libc/error.h

+/**************************************************************************/
+/*                                                                        */
+/*  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

share/libc/uchar.h

+/**************************************************************************/
+/*                                                                        */
+/*  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

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

src/plugins/variadic/tests/known/oracle/printf.res.oracle

-[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.

src/plugins/variadic/tests/known/oracle/swprintf.res.oracle

-[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: 

src/plugins/variadic/tests/known/oracle/wchar.res.oracle

-[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.

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"

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"

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)

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

tests/libc/oracle/uchar_h.res.oracle

+[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}

tests/libc/uchar_h.c

+#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;
+}