[Libc] add specs for basename and dirname

share/libc/libgen.h

@@ -20,13 +20,36 @@
 /*                                                                        */
 /**************************************************************************/
 
-#ifndef __FC_LIBGEN
-#define __FC_LIBGEN
+#ifndef __FC_LIBGEN_H
+#define __FC_LIBGEN_H
 #include "features.h"
+#include "__fc_machdep.h"
+#include "__fc_string_axiomatic.h"
 __PUSH_FC_STDLIB
 __BEGIN_DECLS
 
+extern char __fc_basename[__FC_PATH_MAX];
+char *__fc_p_basename = __fc_basename;
+
+/*@ // missing: assigns path[0 ..], __fc_p_basename[0 ..] \from 'filesystem';
+  requires null_or_valid_string_path: path == \null || valid_read_string(path);
+  assigns path[0 ..], __fc_basename[0 ..] \from path[0 ..], __fc_basename[0 ..];
+  assigns \result \from __fc_p_basename, path;
+  ensures result_points_to_internal_storage_or_path:
+    \subset(\result, {__fc_p_basename, path});
+*/
 extern char *basename(char *path);
+
+extern char __fc_dirname[__FC_PATH_MAX];
+char *__fc_p_dirname = __fc_dirname;
+
+/*@ // missing: assigns path[0 ..], __fc_p_dirname[0 ..] \from 'filesystem';
+  requires null_or_valid_string_path: path == \null || valid_read_string(path);
+  assigns path[0 ..], __fc_dirname[0 ..] \from path[0 ..], __fc_dirname[0 ..];
+  assigns \result \from __fc_p_dirname, path;
+  ensures result_points_to_internal_storage_or_path:
+    \subset(\result, {__fc_p_dirname, path});
+*/
 extern char *dirname(char *path);
 
 __END_DECLS

tests/libc/libgen_h.c

+/*run.config
+
+*/
+
+#include <libgen.h>
+
+int main() {
+  char path[128] = "/tmp/bla/ble.c";
+  char *base = basename(path);
+  //@ assert valid_string(base);
+  char *base2 = basename(0);
+  //@ assert valid_string(base2);
+
+  char *dir = dirname(path);
+  //@ assert valid_string(dir);
+  char *dir2 = dirname(0);
+  //@ assert valid_string(dir2);
+
+  return 0;
+}

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

@@ -37,7 +37,7 @@
    wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call);
    wmemset (0 call); 
   
-  Undefined functions (358)
+  Undefined functions (360)
   =========================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
    Frama_C_abort (1 call); Frama_C_char_interval (0 call);
@@ -69,34 +69,35 @@
    alloca (0 call); asin (0 call); asinf (0 call); asinl (0 call);
    at_quick_exit (0 call); atan (0 call); atan2 (0 call); atan2f (0 call);
    atanf (0 call); atanl (0 call); atexit (0 call); atof (0 call);
-   atol (0 call); atoll (0 call); bind (0 call); bsearch (0 call);
-   bzero (0 call); ceil (0 call); ceilf (0 call); ceill (0 call);
-   clearerr (0 call); clearerr_unlocked (0 call); clock (0 call);
-   clock_gettime (0 call); clock_nanosleep (0 call); close (0 call);
-   closedir (0 call); closelog (0 call); connect (0 call); cos (0 call);
-   cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
-   difftime (0 call); div (0 call); dup (0 call); dup2 (0 call);
-   execl (0 call); execle (0 call); execlp (0 call); execv (0 call);
-   execve (0 call); execvp (0 call); exit (0 call); exp (0 call);
-   expf (0 call); fabsl (0 call); fclose (0 call); fcntl (0 call);
-   fdopen (0 call); feof (2 calls); feof_unlocked (0 call); ferror (2 calls);
-   ferror_unlocked (0 call); fflush (0 call); fgetc (1 call); fgetpos (0 call);
-   fgets (0 call); fgetws (0 call); fileno (0 call); fileno_unlocked (0 call);
-   flock (0 call); flockfile (0 call); floor (0 call); floorf (0 call);
-   floorl (0 call); fmod (0 call); fmodf (0 call); fopen (0 call);
-   fork (0 call); fputc (0 call); fputs (0 call); fread (0 call);
-   free (1 call); freeaddrinfo (0 call); freopen (0 call); fseek (0 call);
-   fsetpos (0 call); ftell (0 call); ftrylockfile (0 call);
-   funlockfile (0 call); fwrite (0 call); gai_strerror (0 call); getc (0 call);
-   getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
-   getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
-   gethostname (0 call); getitimer (0 call); getopt (0 call);
-   getopt_long (0 call); getopt_long_only (0 call); getpid (0 call);
-   getppid (0 call); getpriority (0 call); getpwuid (0 call);
-   getresgid (0 call); getresuid (0 call); getrlimit (0 call);
-   getrusage (0 call); gets (0 call); getsid (0 call); getsockopt (0 call);
-   gettimeofday (0 call); getuid (0 call); gmtime (0 call); htonl (0 call);
-   htons (0 call); iconv (0 call); iconv_close (0 call); iconv_open (0 call);
+   atol (0 call); atoll (0 call); basename (0 call); bind (0 call);
+   bsearch (0 call); bzero (0 call); ceil (0 call); ceilf (0 call);
+   ceill (0 call); clearerr (0 call); clearerr_unlocked (0 call);
+   clock (0 call); clock_gettime (0 call); clock_nanosleep (0 call);
+   close (0 call); closedir (0 call); closelog (0 call); connect (0 call);
+   cos (0 call); cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
+   difftime (0 call); dirname (0 call); div (0 call); dup (0 call);
+   dup2 (0 call); execl (0 call); execle (0 call); execlp (0 call);
+   execv (0 call); execve (0 call); execvp (0 call); exit (0 call);
+   exp (0 call); expf (0 call); fabsl (0 call); fclose (0 call);
+   fcntl (0 call); fdopen (0 call); feof (2 calls); feof_unlocked (0 call);
+   ferror (2 calls); ferror_unlocked (0 call); fflush (0 call); fgetc (1 call);
+   fgetpos (0 call); fgets (0 call); fgetws (0 call); fileno (0 call);
+   fileno_unlocked (0 call); flock (0 call); flockfile (0 call);
+   floor (0 call); floorf (0 call); floorl (0 call); fmod (0 call);
+   fmodf (0 call); fopen (0 call); fork (0 call); fputc (0 call);
+   fputs (0 call); fread (0 call); free (1 call); freeaddrinfo (0 call);
+   freopen (0 call); fseek (0 call); fsetpos (0 call); ftell (0 call);
+   ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call);
+   gai_strerror (0 call); getc (0 call); getc_unlocked (0 call);
+   getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
+   getegid (0 call); geteuid (0 call); getgid (0 call); gethostname (0 call);
+   getitimer (0 call); getopt (0 call); getopt_long (0 call);
+   getopt_long_only (0 call); getpid (0 call); getppid (0 call);
+   getpriority (0 call); getpwuid (0 call); getresgid (0 call);
+   getresuid (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
+   getsid (0 call); getsockopt (0 call); gettimeofday (0 call);
+   getuid (0 call); gmtime (0 call); htonl (0 call); htons (0 call);
+   iconv (0 call); iconv_close (0 call); iconv_open (0 call);
    inet_addr (0 call); inet_ntoa (0 call); inet_ntop (0 call);
    inet_pton (0 call); isascii (0 call); kill (0 call); labs (0 call);
    ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
@@ -148,12 +149,12 @@
    wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
    wmemcmp (0 call); wmemmove (0 call); write (0 call); 
   
-  'Extern' global variables (15)
+  'Extern' global variables (17)
   ==============================
-   __fc_getpwuid_pw_dir; __fc_getpwuid_pw_gid; __fc_getpwuid_pw_name;
-   __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_getpwuid_pw_uid;
-   __fc_hostname; __fc_mblen_state; __fc_mbtowc_state; __fc_strerror;
-   __fc_wctomb_state; optarg; opterr; optopt; tzname
+   __fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_gid;
+   __fc_getpwuid_pw_name; __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell;
+   __fc_getpwuid_pw_uid; __fc_hostname; __fc_mblen_state; __fc_mbtowc_state;
+   __fc_strerror; __fc_wctomb_state; optarg; opterr; optopt; tzname
   
   Potential entry points (1)
   ==========================
@@ -163,13 +164,13 @@
   ============== 
   Sloc = 948
   Decision point = 183
-  Global variables = 54
+  Global variables = 58
   If = 174
   Loop = 40
   Goto = 78
   Assignment = 379
   Exit point = 73
-  Function = 431
+  Function = 433
   Function call = 73
   Pointer dereferencing = 146
   Cyclomatic complexity = 256
@@ -193,6 +194,7 @@
 #include "glob.h"
 #include "iconv.h"
 #include "inttypes.h"
+#include "libgen.h"
 #include "locale.c"
 #include "locale.h"
 #include "math.c"

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

@@ -6427,6 +6427,36 @@ extern int iconv_close(iconv_t);
  */
 extern iconv_t iconv_open(char const *tocode, char const *fromcode);
 
+extern char __fc_basename[256];
+
+char *__fc_p_basename = __fc_basename;
+/*@ requires
+      null_or_valid_string_path: path ≡ \null ∨ valid_read_string(path);
+    ensures
+      result_points_to_internal_storage_or_path:
+        \subset(\result, \union(__fc_p_basename, \old(path)));
+    assigns *(path + (0 ..)), __fc_basename[0 ..], \result;
+    assigns *(path + (0 ..)) \from *(path + (0 ..)), __fc_basename[0 ..];
+    assigns __fc_basename[0 ..] \from *(path + (0 ..)), __fc_basename[0 ..];
+    assigns \result \from __fc_p_basename, path;
+ */
+extern char *basename(char *path);
+
+extern char __fc_dirname[256];
+
+char *__fc_p_dirname = __fc_dirname;
+/*@ requires
+      null_or_valid_string_path: path ≡ \null ∨ valid_read_string(path);
+    ensures
+      result_points_to_internal_storage_or_path:
+        \subset(\result, \union(__fc_p_dirname, \old(path)));
+    assigns *(path + (0 ..)), __fc_dirname[0 ..], \result;
+    assigns *(path + (0 ..)) \from *(path + (0 ..)), __fc_dirname[0 ..];
+    assigns __fc_dirname[0 ..] \from *(path + (0 ..)), __fc_dirname[0 ..];
+    assigns \result \from __fc_p_dirname, path;
+ */
+extern char *dirname(char *path);
+
 /*@ requires valid_file_descriptors: \valid(fds + (0 .. nfds - 1));
     ensures
       error_timeout_or_bounded:

tests/libc/oracle/libgen_h.res.oracle

+[kernel] Parsing tests/libc/libgen_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 basename <- main.
+  Called from tests/libc/libgen_h.c:9.
+[eva] using specification for function basename
+[eva] tests/libc/libgen_h.c:9: 
+  function basename: precondition 'null_or_valid_string_path' got status valid.
+[eva] Done for function basename
+[eva:alarm] tests/libc/libgen_h.c:10: Warning: assertion got status unknown.
+[eva] computing for function basename <- main.
+  Called from tests/libc/libgen_h.c:11.
+[eva] tests/libc/libgen_h.c:11: 
+  function basename: precondition 'null_or_valid_string_path' got status valid.
+[eva] tests/libc/libgen_h.c:11: Warning: 
+  Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
+[eva] Done for function basename
+[eva:alarm] tests/libc/libgen_h.c:12: Warning: assertion got status unknown.
+[eva] computing for function dirname <- main.
+  Called from tests/libc/libgen_h.c:14.
+[eva] using specification for function dirname
+[eva:alarm] tests/libc/libgen_h.c:14: Warning: 
+  function dirname: precondition 'null_or_valid_string_path' got status unknown.
+[eva] Done for function dirname
+[eva:alarm] tests/libc/libgen_h.c:15: Warning: assertion got status unknown.
+[eva] computing for function dirname <- main.
+  Called from tests/libc/libgen_h.c:16.
+[eva] tests/libc/libgen_h.c:16: 
+  function dirname: precondition 'null_or_valid_string_path' got status valid.
+[eva] tests/libc/libgen_h.c:16: Warning: 
+  Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
+[eva] Done for function dirname
+[eva:alarm] tests/libc/libgen_h.c:17: Warning: assertion got status unknown.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __fc_basename[0..255] ∈ [--..--]
+  __fc_dirname[0..255] ∈ [--..--]
+  path[0..127] ∈ [--..--]
+  base ∈ {{ &__fc_basename[0] ; &path[0] }}
+  base2 ∈ {{ NULL ; &__fc_basename[0] }}
+  dir ∈ {{ &__fc_dirname[0] ; &path[0] }}
+  dir2 ∈ {{ NULL ; &__fc_dirname[0] }}
+  __retres ∈ {0}