Merge branch 'feature/andre/libc-chdir-chroot' into 'master'

[Libc] add specs for chdir/chroot

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

share/libc/unistd.h

@@ -745,7 +745,25 @@ extern int          access(const char *path, int amode);
 
 extern unsigned int alarm(unsigned int);
 extern int          brk(void *);
+
+/*@ // missing: may assign to errno: EACCES, ELOOP, ENAMETOOLONG, ENOENT,
+    //                               ENOTDIR
+    // missing: assigns \result \from 'filesystem'
+  requires valid_string_path: valid_read_string(path);
+  assigns \result \from indirect:path, indirect:path[0..];
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
 extern int          chdir(const char *path);
+
+
+/*@ // missing: may assign to errno: EACCES, ELOOP, ENAMETOOLONG, ENOENT,
+    //                               ENOTDIR, EPERM
+    // missing: assigns \result \from 'filesystem, permissions'
+    // missing: assigns 'filesystem view' \from path[0..];
+  requires valid_string_path: valid_read_string(path);
+  assigns \result \from indirect:path, indirect:path[0..];
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
 extern int          chroot(const char *path);
 
 

src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle

-[variadic] FRAMAC_SHARE/libc/unistd.h:795: 
+[variadic] FRAMAC_SHARE/libc/unistd.h:813: 
   Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:800: 
+[variadic] FRAMAC_SHARE/libc/unistd.h:818: 
   Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:805: 
+[variadic] FRAMAC_SHARE/libc/unistd.h:823: 
   Declaration of variadic function execlp.
 [variadic] tests/erroneous/exec.c:5: Warning: 
   Incorrect type for argument 3. The argument will be cast from int to char *.

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

-[variadic] FRAMAC_SHARE/libc/unistd.h:795: 
+[variadic] FRAMAC_SHARE/libc/unistd.h:813: 
   Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:800: 
+[variadic] FRAMAC_SHARE/libc/unistd.h:818: 
   Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:805: 
+[variadic] FRAMAC_SHARE/libc/unistd.h:823: 
   Declaration of variadic function execlp.
 [variadic] tests/known/exec.c:9: Translating call to execle to a call to execve.
 [variadic] tests/known/exec.c:11: Warning: 

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

-[variadic] FRAMAC_SHARE/libc/unistd.h:795: 
+[variadic] FRAMAC_SHARE/libc/unistd.h:813: 
   Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:800: 
+[variadic] FRAMAC_SHARE/libc/unistd.h:818: 
   Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:805: 
+[variadic] FRAMAC_SHARE/libc/unistd.h:823: 
   Declaration of variadic function execlp.
 [variadic] tests/known/exec_failed_requirement.c:7: 
   Translating call to execl to a call to execv.

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 (379)
+  Undefined functions (381)
   =========================
    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);
@@ -73,48 +73,49 @@
    atan2f (0 call); atanf (0 call); atanl (0 call); atexit (0 call);
    atof (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); chown (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); drand48 (0 call); dup (0 call);
-   dup2 (0 call); erand48 (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); getpgid (0 call); getpgrp (0 call);
-   getpid (0 call); getppid (0 call); getpriority (0 call); getpwnam (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 (2 calls);
-   inet_ntoa (0 call); inet_ntop (0 call); inet_pton (0 call);
-   isascii (0 call); isatty (0 call); jrand48 (0 call); kill (0 call);
-   killpg (0 call); labs (0 call); lcong48 (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 (7 calls); mblen (0 call);
-   mbstowcs (0 call); mbtowc (0 call); mkdir (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); pathconf (0 call); pclose (0 call); perror (0 call);
-   pipe (0 call); poll (0 call); popen (0 call); pow (0 call); powf (0 call);
+   ceilf (0 call); ceill (0 call); chdir (0 call); chown (0 call);
+   chroot (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); drand48 (0 call);
+   dup (0 call); dup2 (0 call); erand48 (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); getpgid (0 call);
+   getpgrp (0 call); getpid (0 call); getppid (0 call); getpriority (0 call);
+   getpwnam (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 (2 calls); inet_ntoa (0 call); inet_ntop (0 call);
+   inet_pton (0 call); isascii (0 call); isatty (0 call); jrand48 (0 call);
+   kill (0 call); killpg (0 call); labs (0 call); lcong48 (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 (7 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+   mkdir (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); 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);
@@ -177,7 +178,7 @@
   Goto = 89
   Assignment = 438
   Exit point = 82
-  Function = 461
+  Function = 463
   Function call = 89
   Pointer dereferencing = 158
   Cyclomatic complexity = 286

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

@@ -7318,6 +7318,20 @@ extern int tcsetattr(int fd, int optional_actions, struct termios *termios_p);
  */
 extern int access(char const *path, int amode);
 
+/*@ requires valid_string_path: valid_read_string(path);
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: path), (indirect: *(path + (0 ..)));
+ */
+extern int chdir(char const *path);
+
+/*@ requires valid_string_path: valid_read_string(path);
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: path), (indirect: *(path + (0 ..)));
+ */
+extern int chroot(char const *path);
+
 /*@ requires valid_string_path: valid_read_string(path);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
     assigns \result;

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

 [kernel] Parsing tests/libc/unistd_h.c (with preprocessing)
 [eva] Splitting return states on:
   \return(access) == 0 (auto)
+  \return(chdir) == 0 (auto)
+  \return(chroot) == 0 (auto)
   \return(chown) == 0 (auto)
   \return(dup) == -1 (auto)
   \return(getcwd) == 0 (auto)
@@ -501,6 +503,21 @@
 [eva] computing for function chown <- main.
   Called from tests/libc/unistd_h.c:84.
 [eva] Done for function chown
+[eva] computing for function chdir <- main.
+  Called from tests/libc/unistd_h.c:86.
+[eva] using specification for function chdir
+[eva] tests/libc/unistd_h.c:86: 
+  function chdir: precondition 'valid_string_path' got status valid.
+[eva] Done for function chdir
+[eva] computing for function chroot <- main.
+  Called from tests/libc/unistd_h.c:88.
+[eva] using specification for function chroot
+[eva] tests/libc/unistd_h.c:88: 
+  function chroot: precondition 'valid_string_path' got status valid.
+[eva] Done for function chroot
+[eva] computing for function chroot <- main.
+  Called from tests/libc/unistd_h.c:88.
+[eva] Done for function chroot
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======

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

 [kernel] Parsing tests/libc/unistd_h.c (with preprocessing)
 [eva] Splitting return states on:
   \return(access) == 0 (auto)
+  \return(chdir) == 0 (auto)
+  \return(chroot) == 0 (auto)
   \return(chown) == 0 (auto)
   \return(dup) == -1 (auto)
   \return(getcwd) == 0 (auto)
@@ -501,6 +503,21 @@
 [eva] computing for function chown <- main.
   Called from tests/libc/unistd_h.c:84.
 [eva] Done for function chown
+[eva] computing for function chdir <- main.
+  Called from tests/libc/unistd_h.c:86.
+[eva] using specification for function chdir
+[eva] tests/libc/unistd_h.c:86: 
+  function chdir: precondition 'valid_string_path' got status valid.
+[eva] Done for function chdir
+[eva] computing for function chroot <- main.
+  Called from tests/libc/unistd_h.c:88.
+[eva] using specification for function chroot
+[eva] tests/libc/unistd_h.c:88: 
+  function chroot: precondition 'valid_string_path' got status valid.
+[eva] Done for function chroot
+[eva] computing for function chroot <- main.
+  Called from tests/libc/unistd_h.c:88.
+[eva] Done for function chroot
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======

tests/libc/unistd_h.c

@@ -82,5 +82,10 @@ int main() {
   char *tty = ttyname(1);
 
   r = chown("/tmp/a.txt", 01000, 01000);
+
+  r = chdir("/tmp/");
+
+  r = chroot("/tmp");
+
   return 0;
 }