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

[Libc] add specs for getpwuid, getcwd and pathconf

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

share/libc/locale.c

@@ -27,7 +27,7 @@ struct lconv __C_locale = {".","","","","","","","","","",CHAR_MAX,CHAR_MAX,CHAR
 
 struct lconv *__frama_c_locale=&__C_locale;
 
-char*__frama_c_locale_names[1]={"C"};
+char*__frama_c_locale_names[512]={"C"};
 char *setlocale(int category, const char *locale) {
   if (*locale == 'C') 
     { __frama_c_locale = &__C_locale;

share/libc/locale.h

@@ -132,7 +132,7 @@ struct lconv
                                   )
 
 extern struct lconv* __frama_c_locale;
-extern char*__frama_c_locale_names[];
+extern char*__frama_c_locale_names[512];
 
 /*@ 
   requires locale_null_or_valid_string: locale == \null || valid_read_string(locale);

share/libc/pwd.h

@@ -41,8 +41,35 @@ struct passwd {
   char    *pw_shell;
 };
 
+extern char __fc_getpwuid_pw_name[64];
+extern char __fc_getpwuid_pw_passwd[64];
+extern uid_t __fc_getpwuid_pw_uid;
+extern gid_t __fc_getpwuid_pw_gid;
+extern char __fc_getpwuid_pw_dir[64];
+extern char __fc_getpwuid_pw_shell[64];
+
+struct passwd __fc_getpwuid =
+  {.pw_name = __fc_getpwuid_pw_name,
+   .pw_passwd = __fc_getpwuid_pw_passwd,
+   .pw_uid = __fc_getpwuid_pw_uid,
+   .pw_gid = __fc_getpwuid_pw_gid,
+   .pw_dir = __fc_getpwuid_pw_dir,
+   .pw_shell = __fc_getpwuid_pw_shell};
+
+struct passwd *__fc_p_getpwuid = & __fc_getpwuid;
+
+
 extern struct passwd *getpwnam(const char *);
-extern struct passwd *getpwuid(uid_t);
+
+/*@ // missing: assigns \result, __fc_getpwuid[0..] \from 'password database'
+  assigns \result \from __fc_p_getpwuid, indirect:uid;
+  assigns __fc_getpwuid \from indirect:uid;
+  ensures result_null_or_internal_struct:
+    \result == \null || \result == __fc_p_getpwuid;
+*/
+extern struct passwd *getpwuid(uid_t uid);
+
+
 extern int            getpwnam_r(const char *, struct passwd *, char *,
 			  size_t, struct passwd **);
 extern int            getpwuid_r(uid_t, struct passwd *, char *,

share/libc/unistd.h

@@ -828,7 +828,18 @@ extern pid_t        fork(void);
 extern long int     fpathconf(int, int);
 extern int          fsync(int);
 extern int          ftruncate(int, off_t);
-extern char        *getcwd(char *, size_t);
+
+/*@ // missing: assigns buf[0..size-1] \from 'cwd'
+    // missing: may assign to errno: EACCES, EINVAL, ENAMETOOLONG, ENOENT,
+    //                               ENOMEM, ERANGE
+  requires valid_buf: \valid(buf + (0 .. size-1));
+  assigns buf[0 .. size-1], \result;
+  assigns buf[0 .. size-1] \from indirect:buf, indirect:size;
+  assigns \result \from buf, indirect: size;
+  ensures result_ok_or_error: \result == \null || \result == buf;
+*/
+extern char        *getcwd(char *buf, size_t size);
+
 extern int          getdtablesize(void);
 extern gid_t        getegid(void);
 extern uid_t        geteuid(void);
@@ -874,7 +885,14 @@ extern int          link(const char *, const char *);
 extern int          lockf(int, int, off_t);
 extern off_t        lseek(int, off_t, int);
 extern int          nice(int);
-extern long int     pathconf(const char *, int);
+
+/*@ // missing: may assign to errno: EACCES, EINVAL, ELOOP, ENOENT, ENOTDIR
+    // missing: assigns \result \from 'file path in filesystem'
+  requires valid_path: valid_read_string(path);
+  assigns \result \from indirect:path[0 ..], indirect:name;
+*/
+extern long pathconf(char const *path, int name);
+
 extern int          pause(void);
 
 /*@

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 (338)
+  Undefined functions (341)
   =========================
    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);
@@ -88,24 +88,25 @@
    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); gethostname (0 call);
-   getitimer (0 call); getopt (0 call); getopt_long (0 call);
-   getopt_long_only (0 call); getpriority (0 call); getrlimit (0 call);
-   getrusage (0 call); gets (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);
-   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);
-   malloc (6 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
-   memoverlap (1 call); mkdir (0 call); mktime (0 call); nan (0 call);
-   nanf (0 call); nanl (0 call); nanosleep (0 call); ntohl (0 call);
-   ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
-   openlog (0 call); pclose (0 call); perror (0 call); pipe (0 call);
-   poll (0 call); popen (0 call); pow (0 call); powf (0 call);
+   getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
+   gethostname (0 call); getitimer (0 call); getopt (0 call);
+   getopt_long (0 call); getopt_long_only (0 call); getpriority (0 call);
+   getpwuid (0 call); getrlimit (0 call); getrusage (0 call); gets (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); 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); malloc (6 calls); mblen (0 call);
+   mbstowcs (0 call); mbtowc (0 call); memoverlap (1 call); mkdir (0 call);
+   mktime (0 call); nan (0 call); nanf (0 call); nanl (0 call);
+   nanosleep (0 call); ntohl (0 call); ntohs (0 call); open (0 call);
+   openat (0 call); opendir (0 call); openlog (0 call); pathconf (0 call);
+   pclose (0 call); perror (0 call); pipe (0 call); poll (0 call);
+   popen (0 call); pow (0 call); powf (0 call);
    pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
    pthread_cond_init (0 call); pthread_cond_wait (0 call);
    pthread_create (0 call); pthread_join (0 call);
@@ -142,8 +143,10 @@
    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 (9)
-  =============================
+  'Extern' global variables (15)
+  ==============================
+   __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
   
@@ -155,13 +158,13 @@
   ============== 
   Sloc = 948
   Decision point = 183
-  Global variables = 44
+  Global variables = 52
   If = 174
   Loop = 40
   Goto = 78
   Assignment = 379
   Exit point = 73
-  Function = 411
+  Function = 414
   Function call = 73
   Pointer dereferencing = 146
   Cyclomatic complexity = 256
@@ -193,6 +196,7 @@
 #include "netdb.h"
 #include "poll.h"
 #include "pthread.h"
+#include "pwd.h"
 #include "setjmp.h"
 #include "signal.h"
 #include "stdarg.h"

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

@@ -291,6 +291,14 @@ struct pollfd {
    short revents ;
 };
 typedef unsigned long nfds_t;
+struct passwd {
+   char *pw_name ;
+   char *pw_passwd ;
+   uid_t pw_uid ;
+   gid_t pw_gid ;
+   char *pw_dir ;
+   char *pw_shell ;
+};
 typedef int ( jmp_buf)[5];
 struct __anonstruct_sigjmp_buf_43 {
    jmp_buf buf ;
@@ -2032,7 +2040,7 @@ imaxdiv_t imaxdiv(intmax_t numer, intmax_t denom)
 
 struct lconv *__frama_c_locale;
 
-char *__frama_c_locale_names[1];
+char *__frama_c_locale_names[512];
 
 char *setlocale(int category, char const *locale);
 
@@ -2064,7 +2072,7 @@ struct lconv __C_locale =
    .int_p_sign_posn = (char)127,
    .int_n_sign_posn = (char)127};
 struct lconv *__frama_c_locale = & __C_locale;
-char *__frama_c_locale_names[1] = {(char *)"C"};
+char *__frama_c_locale_names[512] = {(char *)"C"};
 /*@ requires
       locale_null_or_valid_string:
         locale ≡ \null ∨ valid_read_string(locale);
@@ -6498,6 +6506,35 @@ extern int pthread_mutex_lock(pthread_mutex_t *mutex);
  */
 extern int pthread_mutex_unlock(pthread_mutex_t *mutex);
 
+extern char __fc_getpwuid_pw_name[64];
+
+extern char __fc_getpwuid_pw_passwd[64];
+
+extern uid_t __fc_getpwuid_pw_uid;
+
+extern gid_t __fc_getpwuid_pw_gid;
+
+extern char __fc_getpwuid_pw_dir[64];
+
+extern char __fc_getpwuid_pw_shell[64];
+
+struct passwd __fc_getpwuid =
+  {.pw_name = __fc_getpwuid_pw_name,
+   .pw_passwd = __fc_getpwuid_pw_passwd,
+   .pw_uid = __fc_getpwuid_pw_uid,
+   .pw_gid = __fc_getpwuid_pw_gid,
+   .pw_dir = __fc_getpwuid_pw_dir,
+   .pw_shell = __fc_getpwuid_pw_shell};
+struct passwd *__fc_p_getpwuid = & __fc_getpwuid;
+/*@ ensures
+      result_null_or_internal_struct:
+        \result ≡ \null ∨ \result ≡ __fc_p_getpwuid;
+    assigns \result, __fc_getpwuid;
+    assigns \result \from __fc_p_getpwuid, (indirect: uid);
+    assigns __fc_getpwuid \from (indirect: uid);
+ */
+extern struct passwd *getpwuid(uid_t uid);
+
 /*@ assigns *(env + (0 .. 4)); */
 extern int setjmp(int * /*[5]*/ env);
 
@@ -6815,6 +6852,14 @@ extern int execvp(char const *path, char * const *argv);
  */
 extern pid_t fork(void);
 
+/*@ requires valid_buf: \valid(buf + (0 .. size - 1));
+    ensures result_ok_or_error: \result ≡ \null ∨ \result ≡ \old(buf);
+    assigns *(buf + (0 .. size - 1)), \result;
+    assigns *(buf + (0 .. size - 1)) \from (indirect: buf), (indirect: size);
+    assigns \result \from buf, (indirect: size);
+ */
+extern char *getcwd(char *buf, size_t size);
+
 extern char volatile __fc_hostname[64];
 
 /*@ requires name_has_room: \valid(name + (0 .. len - 1));
@@ -6841,6 +6886,12 @@ extern int sethostname(char const *name, size_t len);
     assigns \result \from \nothing; */
 extern uid_t getuid(void);
 
+/*@ requires valid_path: valid_read_string(path);
+    assigns \result;
+    assigns \result \from (indirect: *(path + (0 ..))), (indirect: name);
+ */
+extern long pathconf(char const *path, int name);
+
 /*@ ensures initialization: pipefd: \initialized(\old(pipefd) + (0 .. 1));
     ensures valid_fd0: 0 ≤ *(\old(pipefd) + 0) < 1024;
     ensures valid_fd1: 0 ≤ *(\old(pipefd) + 1) < 1024;

tests/libc/oracle/netdb_c.res.oracle

@@ -13,6 +13,7 @@
   \return(realloc) == 0 (auto)
   \return(getenv) == 0 (auto)
   \return(bsearch) == 0 (auto)
+  \return(getcwd) == 0 (auto)
   \return(memchr) == 0 (auto)
   \return(memcpy) == 0 (auto)
   \return(memmove) == 0 (auto)

tests/libc/oracle/pwd_h.res.oracle

+[kernel] Parsing tests/libc/pwd_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
+  uid ∈ [--..--]
+[eva] computing for function getpwuid <- main.
+  Called from tests/libc/pwd_h.c:10.
+[eva] using specification for function getpwuid
+[eva] Done for function getpwuid
+[eva:alarm] tests/libc/pwd_h.c:13: Warning: assertion got status unknown.
+[eva:alarm] tests/libc/pwd_h.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/libc/pwd_h.c:15: Warning: assertion got status unknown.
+[eva:alarm] tests/libc/pwd_h.c:16: 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_getpwuid.pw_name ∈ {{ NULL + [--..--] ; &__fc_getpwuid_pw_name[0] }}
+               .pw_passwd ∈
+               {{ NULL + [--..--] ; &__fc_getpwuid_pw_passwd[0] }}
+               {.pw_uid; .pw_gid} ∈ [--..--]
+               .pw_dir ∈ {{ NULL + [--..--] ; &__fc_getpwuid_pw_dir[0] }}
+               .pw_shell ∈
+               {{ NULL + [--..--] ; &__fc_getpwuid_pw_shell[0] }}
+  pw ∈ {{ NULL ; &__fc_getpwuid }}
+  __retres ∈ {0}

tests/libc/oracle/unistd_h.0.res.oracle

@@ -77,6 +77,20 @@
   Called from tests/libc/unistd_h.c:39.
 [eva] using specification for function sysconf
 [eva] Done for function sysconf
+[eva] computing for function getcwd <- main.
+  Called from tests/libc/unistd_h.c:42.
+[eva] using specification for function getcwd
+[eva] tests/libc/unistd_h.c:42: 
+  function getcwd: precondition 'valid_buf' got status valid.
+[eva] Done for function getcwd
+[eva] tests/libc/unistd_h.c:44: assertion got status valid.
+[eva:alarm] tests/libc/unistd_h.c:45: Warning: assertion got status unknown.
+[eva] computing for function pathconf <- main.
+  Called from tests/libc/unistd_h.c:48.
+[eva] using specification for function pathconf
+[eva] tests/libc/unistd_h.c:48: 
+  function pathconf: precondition 'valid_path' got status valid.
+[eva] Done for function pathconf
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -88,4 +102,7 @@
   fd2 ∈ [-1..1023]
   pid ∈ [-1..2147483647]
   l ∈ [--..--]
+  cwd[0..63] ∈ [--..--] or UNINITIALIZED
+  res_getcwd ∈ {{ NULL ; &cwd[0] }}
+  pconf ∈ [--..--]
   __retres ∈ {0; 1}

tests/libc/oracle/unistd_h.1.res.oracle

@@ -77,6 +77,20 @@
   Called from tests/libc/unistd_h.c:39.
 [eva] using specification for function sysconf
 [eva] Done for function sysconf
+[eva] computing for function getcwd <- main.
+  Called from tests/libc/unistd_h.c:42.
+[eva] using specification for function getcwd
+[eva] tests/libc/unistd_h.c:42: 
+  function getcwd: precondition 'valid_buf' got status valid.
+[eva] Done for function getcwd
+[eva] tests/libc/unistd_h.c:44: assertion got status valid.
+[eva:alarm] tests/libc/unistd_h.c:45: Warning: assertion got status unknown.
+[eva] computing for function pathconf <- main.
+  Called from tests/libc/unistd_h.c:48.
+[eva] using specification for function pathconf
+[eva] tests/libc/unistd_h.c:48: 
+  function pathconf: precondition 'valid_path' got status valid.
+[eva] Done for function pathconf
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -88,4 +102,7 @@
   fd2 ∈ [-1..1023]
   pid ∈ [-1..2147483647]
   l ∈ [--..--]
+  cwd[0..63] ∈ [--..--] or UNINITIALIZED
+  res_getcwd ∈ {{ NULL ; &cwd[0] }}
+  pconf ∈ [--..--]
   __retres ∈ {0; 1}

tests/libc/pwd_h.c

+/*run.config
+  STDOPT:
+*/
+#include <pwd.h>
+#include "__fc_string_axiomatic.h"
+
+extern uid_t uid;
+
+int main() {
+  struct passwd *pw = getpwuid(uid);
+  if (pw) {
+    //Note: the assertions below are currently imprecise
+    //@ assert valid_read_string(pw->pw_name);
+    //@ assert valid_read_string(pw->pw_passwd);
+    //@ assert valid_read_string(pw->pw_dir);
+    //@ assert valid_read_string(pw->pw_shell);
+  }
+}

tests/libc/unistd_h.c

@@ -38,5 +38,14 @@ int main() {
 
   long l = sysconf(ARG_MAX);
 
+  char cwd[64];
+  char *res_getcwd = getcwd(cwd, 64);
+  if (res_getcwd) {
+    //@ assert res_getcwd == cwd;
+    //@ assert valid_read_string((char*)cwd); // currently imprecise
+  }
+
+  long pconf = pathconf("/tmp/conf.cfg", _PC_NAME_MAX);
+
   return 0;
 }

tests/misc/log-file.i

 /* run.config
-   STDOPT: #"-kernel-log w:@PTEST_RESULT@/log-file-kernel-warnings.txt,r:@PTEST_RESULT@/log-file-kernel-results.txt -value-log f:@PTEST_RESULT@/log-file-feedback.txt,afewr:@PTEST_RESULT@/log-file-value-all.txt -value-log :@PTEST_RESULT@/log-file-value-default.txt -then -kernel-log f:@PTEST_RESULT@/log-file-feedback.txt"
    LOG: log-file-kernel-warnings.txt
    LOG: log-file-kernel-results.txt
    LOG: log-file-feedback.txt
    LOG: log-file-value-all.txt
    LOG: log-file-value-default.txt
    LOG: plugin-log-all.txt
+   STDOPT: #"-kernel-log w:@PTEST_RESULT@/log-file-kernel-warnings.txt,r:@PTEST_RESULT@/log-file-kernel-results.txt -value-log f:@PTEST_RESULT@/log-file-feedback.txt,afewr:@PTEST_RESULT@/log-file-value-all.txt -value-log :@PTEST_RESULT@/log-file-value-default.txt -then -kernel-log f:@PTEST_RESULT@/log-file-feedback.txt"
    OPT: -load-module tests/misc/plugin_log.ml -kernel-msg-key foo-category -kernel-log=a:@PTEST_RESULT@/plugin-log-all.txt
  */
 int f(void); // generates kernel warning (missing spec)