Merge branch 'feature/andre/libc-stat' into 'master'

[Libc] add a few specs for sys/stat.h

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

share/compliance/nonstandard_identifiers.json

@@ -5,6 +5,7 @@
         {"ident":"facilitynames", "header":"syslog.h"},
         {"ident":"getresgid", "header":"unistd.h"},
         {"ident":"getresuid", "header":"unistd.h"},
+        {"ident":"makedev", "header":"sys/types.h"},
         {"ident":"option", "header":"getopt.h"},
         {"ident":"prioritynames", "header":"syslog.h"},
         {"ident":"setresgid", "header":"unistd.h"},

share/libc/sys/stat.h

@@ -32,25 +32,58 @@ __BEGIN_DECLS
 extern int    chmod(const char *, mode_t);
 extern int    fchmod(int, mode_t);
 extern int    fstat(int, struct stat *);
-extern int    lstat(const char *, struct stat *);
+
+/*@ // missing: may assign to errno: EACCES, ELOOP, ENAMETOOLONG,
+    //                               ENOENT, ENOMEM, ENOTDIR, EOVERFLOW,
+    //                               EINVAL
+    // missing: assigns \result, *buf \from 'filesystem'
+  requires valid_path: valid_read_string(path);
+  requires valid_buf: \valid(buf);
+  assigns \result, *buf \from indirect:path, indirect:path[0..strlen(path)];
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int    lstat(const char *path, struct stat *buf);
 
 /*@ // missing: may assign to errno: EACCES, EEXIST, ELOOP, EMLINK,
     //                               ENAMETOOLONG, ENOENT, ENOSPC,
     //                               ENOTDIR, EROFS
     // missing: assigns \result \from 'filesystem'
-  requires valid_string_path: valid_read_string(path);
-  assigns \result \from indirect:path, indirect:path[0..], indirect:mode;
+  requires valid_path: valid_read_string(path);
+  assigns \result \from indirect:path, indirect:path[0..strlen(path)],
+                        indirect:mode;
   ensures result_ok_or_error: \result == 0 || \result == -1;
 */
 extern int    mkdir(const char *path, mode_t mode);
 
-extern int    mkfifo(const char *, mode_t);
-extern int    mknod(const char *, mode_t, dev_t);
+/*@ // missing: may assign to errno: EACCES, EEXIST, ELOOP, ENAMETOOLONG,
+    //                               ENOENT, ENOTDIR, ENOSPC, EROFS
+    // missing: assigns \result \from 'filesystem'
+    // missing: assigns 'filesystem' \from indirect:path,
+    //                                     indirect:path[0..strlen(path)], mode;
+  requires valid_path: valid_read_string(path);
+  assigns \result \from indirect:path, indirect:path[0..strlen(path)],
+                        indirect:mode;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int    mkfifo(const char *path, mode_t mode);
+
+/*@ // missing: may assign to errno: EACCES, EEXIST, EINVAL, EIO, ELOOP,
+    //                               ENAMETOOLONG, ENOENT, ENOTDIR, ENOSPC,
+    //                               EPERM, EROFS
+    // missing: assigns \result \from 'filesystem'
+    // missing: assigns 'filesystem' \from indirect:path,
+    //          indirect:path[0..strlen(path)], mode, dev;
+  requires valid_path: valid_read_string(path);
+  assigns \result \from indirect:path, indirect:path[0..strlen(path)],
+                        indirect:mode, indirect:dev;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int    mknod(const char *path, mode_t mode, dev_t dev);
 
 /*@ //missing: assigns \from 'filesystem'
   requires valid_pathname: valid_read_string(pathname);
   requires valid_buf: \valid(buf);
-  assigns \result, *buf \from pathname[0..];
+  assigns \result, *buf \from pathname[0..strlen(pathname)];
   ensures result_ok_or_error: \result == 0 || \result == -1;
   ensures init_on_success:initialization:buf:
     \result == 0 ==> \initialized(buf);

share/libc/sys/types.h

@@ -49,6 +49,10 @@ typedef unsigned long u_long;
 typedef unsigned int u_int;
 typedef unsigned short u_short;
 typedef unsigned char u_char;
+
+// Note: makedev (non-POSIX) is usually a macro; in case of problems,
+// consider redefining this.
+/*@ assigns \result \from maj, min; */
 extern dev_t makedev(int maj, int min);
 #define __u_char_defined
 #endif

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

@@ -164,6 +164,7 @@
 #include "stdlib.h"
 #include "string.h"
 #include "strings.h"
+#include "sys/types.h"
 #include "time.h"
 #include "wchar.h"
 /*@ requires valid_read_string(format);

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

@@ -44,6 +44,7 @@
 #include "stdio.c"
 #include "stdio.h"
 #include "stdlib.h"
+#include "sys/types.h"
 /*@ requires valid_read_string(format);
     assigns \result, __fc_stdout->__fc_FILE_data;
     assigns \result

tests/libc/oracle/fc_libc.0.res.oracle

@@ -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 (390)
+  Undefined functions (394)
   =========================
    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);
@@ -111,8 +111,9 @@
    localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
    log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
    logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
-   lseek (0 call); malloc (7 calls); mblen (0 call); mbstowcs (0 call);
-   mbtowc (0 call); mkdir (0 call); mkstemp (0 call); mktime (0 call);
+   lseek (0 call); lstat (0 call); makedev (0 call); malloc (7 calls);
+   mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call);
+   mkfifo (0 call); mknod (0 call); mkstemp (0 call); mktime (0 call);
    mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
    nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
    open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
@@ -180,7 +181,7 @@
   Goto = 89
   Assignment = 438
   Exit point = 82
-  Function = 472
+  Function = 476
   Function call = 89
   Pointer dereferencing = 158
   Cyclomatic complexity = 286

tests/libc/oracle/fc_libc.1.res.oracle

@@ -4954,6 +4954,10 @@ extern int pclose(FILE *stream);
 
 ssize_t getline(char **lineptr, size_t *n, FILE *stream);
 
+/*@ assigns \result;
+    assigns \result \from maj, min; */
+extern dev_t makedev(int maj, int min);
+
 FILE __fc_initial_stdout =
   {.__fc_FILE_id = (unsigned int)1, .__fc_FILE_data = 0U};
 FILE *__fc_stdout = & __fc_initial_stdout;
@@ -7531,14 +7535,44 @@ extern int setitimer(int which,
 extern int select(int nfds, fd_set *readfds, fd_set *writefds,
                   fd_set *errorfds, struct timeval *timeout);
 
-/*@ requires valid_string_path: valid_read_string(path);
+/*@ requires valid_path: valid_read_string(path);
+    requires valid_buf: \valid(buf);
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result, *buf;
+    assigns \result
+      \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path))));
+    assigns *buf
+      \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path))));
+ */
+extern int lstat(char const *path, struct stat *buf);
+
+/*@ requires valid_path: valid_read_string(path);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
     assigns \result;
     assigns \result
-      \from (indirect: path), (indirect: *(path + (0 ..))), (indirect: mode);
+      \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path)))),
+            (indirect: mode);
  */
 extern int mkdir(char const *path, mode_t mode);
 
+/*@ requires valid_path: valid_read_string(path);
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result
+      \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path)))),
+            (indirect: mode);
+ */
+extern int mkfifo(char const *path, mode_t mode);
+
+/*@ requires valid_path: valid_read_string(path);
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result
+      \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path)))),
+            (indirect: mode), (indirect: dev);
+ */
+extern int mknod(char const *path, mode_t mode, dev_t dev);
+
 /*@ requires valid_pathname: valid_read_string(pathname);
     requires valid_buf: \valid(buf);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
@@ -7546,8 +7580,8 @@ extern int mkdir(char const *path, mode_t mode);
       init_on_success: initialization: buf:
         \result ≡ 0 ⇒ \initialized(\old(buf));
     assigns \result, *buf;
-    assigns \result \from *(pathname + (0 ..));
-    assigns *buf \from *(pathname + (0 ..));
+    assigns \result \from *(pathname + (0 .. strlen{Old}(pathname)));
+    assigns *buf \from *(pathname + (0 .. strlen{Old}(pathname)));
  */
 extern int stat(char const *pathname, struct stat *buf);
 

tests/libc/oracle/sys_stat_h.res.oracle

@@ -28,12 +28,12 @@
   Called from tests/libc/sys_stat_h.c:17.
 [eva] using specification for function mkdir
 [eva] tests/libc/sys_stat_h.c:17: 
-  function mkdir: precondition 'valid_string_path' got status valid.
+  function mkdir: precondition 'valid_path' got status valid.
 [eva] Done for function mkdir
 [eva] computing for function mkdir <- main.
   Called from tests/libc/sys_stat_h.c:20.
 [eva:alarm] tests/libc/sys_stat_h.c:20: Warning: 
-  function mkdir: precondition 'valid_string_path' got status invalid.
+  function mkdir: precondition 'valid_path' got status invalid.
 [eva] Done for function mkdir
 [eva] computing for function mkdir <- main.
   Called from tests/libc/sys_stat_h.c:20.
@@ -45,6 +45,32 @@
 [eva] computing for function umask <- main.
   Called from tests/libc/sys_stat_h.c:22.
 [eva] Done for function umask
+[eva] computing for function lstat <- main.
+  Called from tests/libc/sys_stat_h.c:23.
+[eva] using specification for function lstat
+[eva] tests/libc/sys_stat_h.c:23: 
+  function lstat: precondition 'valid_path' got status valid.
+[eva] tests/libc/sys_stat_h.c:23: 
+  function lstat: precondition 'valid_buf' got status valid.
+[eva] Done for function lstat
+[eva] computing for function lstat <- main.
+  Called from tests/libc/sys_stat_h.c:23.
+[eva] Done for function lstat
+[eva] computing for function mkfifo <- main.
+  Called from tests/libc/sys_stat_h.c:24.
+[eva] using specification for function mkfifo
+[eva] tests/libc/sys_stat_h.c:24: 
+  function mkfifo: precondition 'valid_path' got status valid.
+[eva] Done for function mkfifo
+[eva] computing for function mknod <- main.
+  Called from tests/libc/sys_stat_h.c:25.
+[eva] using specification for function mknod
+[eva] tests/libc/sys_stat_h.c:25: 
+  function mknod: precondition 'valid_path' got status valid.
+[eva] Done for function mknod
+[eva] computing for function mknod <- main.
+  Called from tests/libc/sys_stat_h.c:25.
+[eva] Done for function mknod
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -55,4 +81,7 @@
   r ∈ {-1; 0}
   r_mkdir ∈ {-1; 0}
   old_mask ∈ [--..--]
+  r2 ∈ {-1; 0}
+  r3 ∈ {-1; 0}
+  r4 ∈ {-1; 0}
   __retres ∈ {-1; 0; 1; 2; 3}

tests/libc/oracle/sys_types.res.oracle

+[kernel] Parsing tests/libc/sys_types.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 makedev <- main.
+  Called from tests/libc/sys_types.c:4.
+[eva] using specification for function makedev
+[eva] Done for function makedev
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  dev ∈ [--..--]
+  __retres ∈ {0}

tests/libc/sys_stat_h.c

@@ -20,5 +20,8 @@ int main() {
     mkdir(non_terminated, 0422);
   }
   mode_t old_mask = umask(0644);
+  int r2 = lstat("/tmp/bla", &st);
+  int r3 = mkfifo("/tmp/fifo", 0644);
+  int r4 = mknod("/tmp/fifo2", 0644, 42);
   return 0;
 }

tests/libc/sys_types.c

+#include <sys/types.h>
+
+int main() {
+  dev_t dev = makedev(1, 42);
+  return 0;
+}