Merge branch 'feature/andre/libc-sys-param' into 'master'

[Libc] add stub for non-POSIX sys/param.h

See merge request frama-c/frama-c!2630

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

share/libc/sys/param.h

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

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

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"

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"

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:

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)

tests/libc/oracle/sys_utsname_h.res.oracle

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

tests/libc/sys_utsname_h.c

+#include <time.h>
+#include <sys/utsname.h>
+
+int main() {
+  struct utsname n;
+  int r = uname(&n);
+  //@ assert \initialized(&n);
+  return 0;
+}