diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 593ff2ec4babcbe9806706009b5cb7f2621e32a4..90def1eb36789bcf7ad67f2739707038715a56ba 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -279,6 +279,7 @@ share/libc/sys/file.h: CEA_LGPL
share/libc/sys/ioctl.h: CEA_LGPL
share/libc/sys/ipc.h: CEA_LGPL
share/libc/sys/mman.h: CEA_LGPL
+share/libc/sys/param.h: CEA_LGPL
share/libc/sys/random.h: CEA_LGPL
share/libc/sys/resource.h: CEA_LGPL
share/libc/sys/select.h: CEA_LGPL
diff --git a/share/libc/sys/param.h b/share/libc/sys/param.h
new file mode 100644
index 0000000000000000000000000000000000000000..a8206b81cd6a78791ee12d0ae7b8438eeba5d638
--- /dev/null
+++ b/share/libc/sys/param.h
@@ -0,0 +1,36 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2020 */
+/* 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_SYS_PARAM_H__
+#define __FC_SYS_PARAM_H__
+#include "../features.h"
+__PUSH_FC_STDLIB
+
+// Note: sys/param.h is not a POSIX file. This is provided as a best-effort
+// basis to support projects using constants such as PATH_MAX, which should
+// be defined in "limits.h" according to POSIX. For instance, in Linux,
+// PATH_MAX is defined in the non-POSIX file linux/limits.h.
+
+#include "../limits.h"
+
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/sys/utsname.h b/share/libc/sys/utsname.h
index 54f908fa310c14c7c106f352a913ac5ea98fa552..e60cacea8b185e8452c44e948a147ce6348c5556 100644
--- a/share/libc/sys/utsname.h
+++ b/share/libc/sys/utsname.h
@@ -38,6 +38,12 @@ struct utsname
char machine[_FC_UTSNAME_LENGTH];
};
+/*@ // missing: assigns *name, \result \from "system information"
+ requires valid_name: \valid(name);
+ assigns *name, \result \from \nothing;
+ ensures result_ok_or_error: -1 <= \result;
+ ensures initialization:name:\initialized(name);
+*/
extern int uname (struct utsname *name);
__POP_FC_STDLIB
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index fc52ca5ff0ad17a4190b6bb394a20cd090e22d0f..db68bcf3adf8d06663093e725347cb4f8ae7de7f 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -123,6 +123,7 @@
#include "sys/ipc.h"
#include "syslog.h"
#include "sys/mman.h"
+#include "sys/param.h"
#include "sys/random.h"
#include "sys/resource.h"
#include "sys/select.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index fefd9fce133ac0e463ea535e54a79caec09fc2af..d0a318762b25eed2f4bbcf4f604f864e49adb936 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/libc/fc_libc.c:153: assertion got status valid.
[eva] tests/libc/fc_libc.c:154: assertion got status valid.
[eva] tests/libc/fc_libc.c:155: assertion got status valid.
[eva] tests/libc/fc_libc.c:156: assertion got status valid.
+[eva] tests/libc/fc_libc.c:157: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -40,7 +40,7 @@
unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
- Undefined functions (406)
+ Undefined functions (407)
=========================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -154,14 +154,15 @@
syslog (0 call); system (0 call); tcflush (0 call); tcgetattr (0 call);
tcsetattr (0 call); time (0 call); times (0 call); tmpfile (0 call);
tmpnam (0 call); trunc (0 call); truncf (0 call); truncl (0 call);
- ttyname (0 call); tzset (0 call); umask (0 call); ungetc (0 call);
- unlink (0 call); usleep (0 call); utimes (0 call); vfprintf (0 call);
- vfscanf (0 call); vprintf (0 call); vscanf (0 call); vsnprintf (0 call);
- vsprintf (0 call); vsyslog (0 call); wait (0 call); waitpid (0 call);
- wcschr (0 call); wcscmp (0 call); wcscspn (0 call); wcslcat (0 call);
- wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call);
- wcsspn (0 call); wcsstr (0 call); wcstombs (0 call); wctomb (0 call);
- wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call); write (0 call);
+ ttyname (0 call); tzset (0 call); umask (0 call); uname (0 call);
+ ungetc (0 call); unlink (0 call); usleep (0 call); utimes (0 call);
+ vfprintf (0 call); vfscanf (0 call); vprintf (0 call); vscanf (0 call);
+ vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call); wait (0 call);
+ waitpid (0 call); wcschr (0 call); wcscmp (0 call); wcscspn (0 call);
+ wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call);
+ wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call); wcstombs (0 call);
+ wctomb (0 call); wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call);
+ write (0 call);
'Extern' global variables (16)
==============================
@@ -184,7 +185,7 @@
Goto = 89
Assignment = 438
Exit point = 82
- Function = 488
+ Function = 489
Function call = 89
Pointer dereferencing = 158
Cyclomatic complexity = 286
@@ -244,6 +245,7 @@
#include "sys/times.h"
#include "sys/types.h"
#include "sys/uio.h"
+#include "sys/utsname.h"
#include "sys/wait.h"
#include "syslog.h"
#include "termios.h"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index f940ecca0a0a3bd89df54454c6c97cbe5cbfa77a..6e164aa81579b0f8146b9ca5e60b583632cce8f7 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -363,6 +363,13 @@ struct tms {
clock_t tms_cutime ;
clock_t tms_cstime ;
};
+struct utsname {
+ char sysname[65] ;
+ char nodename[65] ;
+ char release[65] ;
+ char version[65] ;
+ char machine[65] ;
+};
typedef unsigned int tcflag_t;
typedef unsigned char cc_t;
typedef unsigned int speed_t;
@@ -8024,6 +8031,15 @@ extern int setrlimit(int resource, struct rlimit const *rlp);
*/
extern clock_t times(struct tms *buffer);
+/*@ requires valid_name: \valid(name);
+ ensures result_ok_or_error: -1 ≤ \result;
+ ensures initialization: name: \initialized(\old(name));
+ assigns *name, \result;
+ assigns *name \from \nothing;
+ assigns \result \from \nothing;
+ */
+extern int uname(struct utsname *name);
+
/*@ ensures result_ok_or_error: \result ≡ -1 ∨ \result ≥ 0;
ensures
initialization: stat_loc_init_on_success:
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index e85ef1cf9e12a1987c8e2da16cd1ca85923d016b..4b7f321bdaefa863bb3a434a0f0479af8319120d 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -97,6 +97,7 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/sys/ioctl.h (with preprocessing)
[kernel] Parsing share/libc/sys/ipc.h (with preprocessing)
[kernel] Parsing share/libc/sys/mman.h (with preprocessing)
+[kernel] Parsing share/libc/sys/param.h (with preprocessing)
[kernel] Parsing share/libc/sys/random.h (with preprocessing)
[kernel] Parsing share/libc/sys/resource.h (with preprocessing)
[kernel] Parsing share/libc/sys/select.h (with preprocessing)
diff --git a/tests/libc/oracle/sys_utsname_h.res.oracle b/tests/libc/oracle/sys_utsname_h.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..62c536e7987b104dc03b6025d29085c77c3d7419
--- /dev/null
+++ b/tests/libc/oracle/sys_utsname_h.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing tests/libc/sys_utsname_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 uname <- main.
+ Called from tests/libc/sys_utsname_h.c:6.
+[eva] using specification for function uname
+[eva] tests/libc/sys_utsname_h.c:6:
+ function uname: precondition 'valid_name' got status valid.
+[eva] Done for function uname
+[eva] tests/libc/sys_utsname_h.c:7: assertion got status valid.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ n ∈ [--..--]
+ r ∈ [-1..2147483647]
+ __retres ∈ {0}
diff --git a/tests/libc/sys_utsname_h.c b/tests/libc/sys_utsname_h.c
new file mode 100644
index 0000000000000000000000000000000000000000..3e606cf36d1eac4487355aaf7f2870b62544c7dc
--- /dev/null
+++ b/tests/libc/sys_utsname_h.c
@@ -0,0 +1,9 @@
+#include <time.h>
+#include <sys/utsname.h>
+
+int main() {
+ struct utsname n;
+ int r = uname(&n);
+ //@ assert \initialized(&n);
+ return 0;
+}