diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index e2199735c8ffdce984900513525cf71b58689c82..17b5c4e5a21d9618db173fd6d1d3ec67baac7365 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -317,6 +317,7 @@ share/libc/time.h: CEA_LGPL
share/libc/unistd.c: CEA_LGPL
share/libc/unistd.h: CEA_LGPL
share/libc/utime.h: CEA_LGPL
+share/libc/utmp.h: CEA_LGPL
share/libc/utmpx.h: CEA_LGPL
share/libc/wchar.c: CEA_LGPL
share/libc/wchar.h: CEA_LGPL
diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
index f9677ee2920415c3d8636d49de0dcd153fac5844..f48c2a451635a25714abca51a28b18f3442e7d2b 100644
--- a/share/libc/__fc_libc.h
+++ b/share/libc/__fc_libc.h
@@ -104,6 +104,7 @@
#include "time.h"
#include "unistd.h"
#include "utime.h"
+#include "utmp.h"
#include "utmpx.h"
#include "wchar.h"
#include "wctype.h"
diff --git a/share/libc/utmp.h b/share/libc/utmp.h
new file mode 100644
index 0000000000000000000000000000000000000000..6c7577b3e28a5a20a11e6edcd6305bb1f0848b0c
--- /dev/null
+++ b/share/libc/utmp.h
@@ -0,0 +1,111 @@
+/**************************************************************************/
+/* */
+/* 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). */
+/* */
+/**************************************************************************/
+
+// Note: this file is non-POSIX, but used by some coreutils.
+
+#ifndef __FC_UTMP
+#define __FC_UTMP
+#include "features.h"
+__PUSH_FC_STDLIB
+
+#include "__fc_define_pid_t.h"
+#include "sys/time.h"
+#include "stdint.h"
+
+__BEGIN_DECLS
+
+#define _PATH_UTMP "/var/run/utmp"
+#define UTMP_FILE _PATH_UTMP
+#define UTMP_FILENAME _PATH_UTMP
+#define _PATH_WTMP "/var/log/wtmp"
+#define WTMP_FILE _PATH_WTMP
+#define WTMP_FILENAME _PATH_WTMP
+
+#define UT_LINESIZE 32
+#define UT_NAMESIZE 32
+#define UT_HOSTSIZE 256
+
+struct lastlog
+{
+ time_t ll_time;
+ char ll_line[UT_LINESIZE];
+ char ll_host[UT_HOSTSIZE];
+};
+
+struct exit_status
+{
+ short int e_termination;
+ short int e_exit;
+};
+
+struct utmp
+{
+ short int ut_type;
+ pid_t ut_pid;
+ char ut_line[UT_LINESIZE];
+ char ut_id[4];
+ char ut_user[UT_NAMESIZE];
+ char ut_host[UT_HOSTSIZE];
+ struct exit_status ut_exit;
+ long int ut_session;
+ struct timeval ut_tv;
+ int32_t ut_addr_v6[4];
+ char __glibc_reserved[20]; // used by who.c
+};
+
+#define ut_name ut_user
+#define ut_time ut_tv.tv_sec
+
+extern int login_tty (int fd);
+extern void login (const struct utmp *entry);
+extern int logout (const char *ut_line);
+extern void logwtmp (const char *ut_line, const char *ut_name,
+ const char *ut_host);
+
+extern void updwtmp (const char *wtmp_file, const struct utmp *utmp);
+
+extern int utmpname (const char *file);
+
+extern struct utmp *getutent (void);
+
+extern void setutent (void);
+
+extern void endutent (void);
+
+extern struct utmp *getutid (const struct utmp *id);
+
+extern struct utmp *getutline (const struct utmp *line);
+
+extern struct utmp *pututline (const struct utmp *utmp_ptr);
+
+extern int getutent_r (struct utmp *buffer, struct utmp **result);
+
+extern int getutid_r (const struct utmp *id, struct utmp *buffer,
+ struct utmp **result);
+
+extern int getutline_r (const struct utmp *line,
+ struct utmp *buffer, struct utmp **result);
+
+
+__END_DECLS
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/utmpx.h b/share/libc/utmpx.h
index 17aefa94f035c2221b1ccc52a4094028a4ffc0d2..62df76cf503673f27f62e70055afc5af722e746e 100644
--- a/share/libc/utmpx.h
+++ b/share/libc/utmpx.h
@@ -26,6 +26,7 @@
__PUSH_FC_STDLIB
#include "__fc_define_pid_t.h"
+#include "stdint.h"
#include "sys/time.h"
__BEGIN_DECLS
@@ -41,6 +42,8 @@ struct utmpx {
pid_t ut_pid;
short ut_type;
struct timeval ut_tv;
+ int32_t ut_addr_v6[4]; // not POSIX, but allowed by it
+ char __glibc_reserved[20]; // not POSIX, but allowed by it
};
#define EMPTY 0
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 7b1e11d5a7fca2ade7f3553ea51e6200046fbac5..a4bf6fc2786257dcf7d1e638573ac0698478a1a6 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -148,6 +148,7 @@
#include "time.h"
#include "unistd.h"
#include "utime.h"
+#include "utmp.h"
#include "utmpx.h"
#include "wchar.h"
#include "wctype.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 7955573b0c8101d35d2a7b324dcc54e1a9266e80..27d51d73125d488deb50c9b03993abb5f11e6c64 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -7,10 +7,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/libc/fc_libc.c:158: assertion got status valid.
[eva] tests/libc/fc_libc.c:159: assertion got status valid.
[eva] tests/libc/fc_libc.c:160: assertion got status valid.
[eva] tests/libc/fc_libc.c:161: assertion got status valid.
+[eva] tests/libc/fc_libc.c:162: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 3061c00a62693b3c162c1ee0902ec050b76d8b3a..79d97d4b4490d23eca6cadbd4f2f69b36a6c26ec 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -124,6 +124,7 @@ skipping share/libc/tgmath.h
[kernel] Parsing share/libc/time.h (with preprocessing)
[kernel] Parsing share/libc/unistd.h (with preprocessing)
[kernel] Parsing share/libc/utime.h (with preprocessing)
+[kernel] Parsing share/libc/utmp.h (with preprocessing)
[kernel] Parsing share/libc/utmpx.h (with preprocessing)
[kernel] Parsing share/libc/wchar.h (with preprocessing)
[kernel] Parsing share/libc/wctype.h (with preprocessing)