Merge branch 'feature/andre/libc-more-tests' into 'master'

[libc] add some tests based on manpages

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

share/libc/dirent.h

@@ -59,7 +59,7 @@ extern int alphasort(const struct dirent **a, const struct dirent **b);
 /*@
   requires dirp_valid_dir_stream: \subset(dirp,&__fc_opendir[0 .. __FC_FOPEN_MAX-1]);
   assigns \result \from dirp, *dirp, __fc_p_opendir;
-  assigns errno \from dirp, *dirp, __fc_p_opendir;
+  assigns errno \from indirect:dirp, indirect:*dirp, indirect:__fc_p_opendir;
   assigns *dirp \from dirp, *dirp, __fc_p_opendir;
   ensures err_or_closed_on_success: 
     (\result == 0 && dirp->__fc_dir_inode == \null) || \result == -1;
@@ -80,7 +80,7 @@ extern DIR *fdopendir(int fd);
 
 /*@
   assigns \result \from path[0..], __fc_p_opendir;
-  assigns errno \from path[0..], __fc_p_opendir;
+  assigns errno \from indirect:path[0..], indirect:__fc_p_opendir;
   ensures result_null_or_valid: \result == \null || \valid(\result);
   ensures valid_dir_stream_on_success: 
     \result != \null ==> \result == &__fc_opendir[\result->__fc_dir_id];
@@ -93,7 +93,7 @@ extern DIR *opendir(const char *path);
   requires dirp_valid_dir_stream: \subset(dirp, &__fc_opendir[0 .. __FC_FOPEN_MAX-1]);
   assigns \result \from *dirp, __fc_p_opendir;
   assigns dirp->__fc_dir_position \from dirp->__fc_dir_position;
-  assigns errno \from dirp, *dirp, __fc_p_opendir;
+  assigns errno \from indirect:dirp, indirect:*dirp, indirect:__fc_p_opendir;
   ensures result_null_or_valid: \result == \null || \valid(\result);
 */
 extern struct dirent *readdir(DIR *dirp);

tests/libc/dirent_h.c

+// Example from the POSIX manpage for fdopendir(3p)
+
+#include <stdio.h>
+#include <dirent.h>
+#include <fcntl.h>
+#include <sys/stat.h>
+#include <stdint.h>
+#include <stdlib.h>
+#include <unistd.h>
+
+int
+main(int argc, char *argv[])
+{
+  struct stat statbuf;
+  DIR *d;
+  struct dirent *dp;
+  int dfd, ffd;
+
+  if ((d = fdopendir((dfd = open("./tmp", O_RDONLY)))) == NULL) {
+    fprintf(stderr, "Cannot open ./tmp directory\n");
+    exit(1);
+  }
+  while ((dp = readdir(d)) != NULL) {
+    if (dp->d_name[0] == '.')
+      continue;
+    /* there is a possible race condition here as the file
+     * could be renamed between the readdir and the open */
+    if ((ffd = openat(dfd, dp->d_name, O_RDONLY)) == -1) {
+      perror(dp->d_name);
+      continue;
+    }
+    if (fstat(ffd, &statbuf) == 0 && statbuf.st_size > (1024*1024)) {
+      /* found it ... */
+      printf("%s: %jdK\n", dp->d_name,
+             (intmax_t)(statbuf.st_size / 1024));
+    }
+    close(ffd);
+  }
+  closedir(d); // note this implicitly closes dfd
+  return 0;
+}

tests/libc/langinfo_h.c

+#include <langinfo.h>
+#include <locale.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int main(void) {
+  setlocale(LC_CTYPE, "");
+  setlocale(LC_NUMERIC, "");
+
+  printf("%s\n", nl_langinfo(CODESET));
+  printf("%s\n", nl_langinfo(RADIXCHAR));
+
+  return EXIT_SUCCESS;
+}

tests/libc/oracle/dirent_h.res.oracle

+[kernel] Parsing dirent_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 __va_open_void <- main.
+  Called from dirent_h.c:19.
+[eva] using specification for function __va_open_void
+[eva] dirent_h.c:19: 
+  function __va_open_void: precondition 'valid_filename' got status valid.
+[eva] dirent_h.c:19: 
+  function __va_open_void: precondition 'flag_not_CREAT' got status valid.
+[eva] Done for function __va_open_void
+[eva] computing for function fdopendir <- main.
+  Called from dirent_h.c:19.
+[eva] using specification for function fdopendir
+[eva:garbled-mix:assigns] dirent_h.c:19: 
+  The specification of function fdopendir
+  has generated a garbled mix of addresses for assigns clause \result.
+[eva] Done for function fdopendir
+[eva:alarm] dirent_h.c:19: Warning: 
+  pointer comparison. assert \pointer_comparable((void *)d, (void *)0);
+[eva] computing for function fprintf_va_1 <- main.
+  Called from dirent_h.c:20.
+[eva] using specification for function fprintf
+[eva] dirent_h.c:20: function fprintf_va_1: precondition got status valid.
+[eva] Done for function fprintf_va_1
+[eva] computing for function exit <- main.
+  Called from dirent_h.c:21.
+[eva] using specification for function exit
+[eva] Done for function exit
+[eva] computing for function readdir <- main.
+  Called from dirent_h.c:23.
+[eva] using specification for function readdir
+[eva:alarm] dirent_h.c:23: Warning: 
+  function readdir: precondition 'dirp_valid_dir_stream' got status unknown.
+[eva] Done for function readdir
+[eva] computing for function closedir <- main.
+  Called from dirent_h.c:39.
+[eva] using specification for function closedir
+[eva] dirent_h.c:39: 
+  function closedir: precondition 'dirp_valid_dir_stream' got status valid.
+[eva:garbled-mix:assigns] dirent_h.c:39: 
+  The specification of function closedir
+  has generated a garbled mix of addresses for assigns clause *dirp.
+[eva] Done for function closedir
+[eva] Recording results for main
+[eva] Done for function main
+[eva:garbled-mix:summary] 
+  Origins of garbled mix generated during analysis:
+    dirent_h.c:19: assigns clause on addresses
+      (read in 2 statements, propagated through 2 statements)
+      garbled mix of &{__fc_opendir}
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __fc_errno ∈ [--..--]
+  __fc_opendir[0..15] ∈
+              {{ garbled mix of &{__fc_opendir}
+               (origin: Library function {dirent_h.c:39}) }}
+  d ∈ {{ &__fc_opendir + [0..240],0%16 }}
+  dp ∈ {0}
+  dfd ∈ [-1..1023]
+  __retres ∈ {0}
+  S___fc_stderr[0..1] ∈ [--..--]

tests/libc/oracle/langinfo_h.res.oracle

+[kernel] Parsing langinfo_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 setlocale <- main.
+  Called from langinfo_h.c:7.
+[eva] using specification for function setlocale
+[eva] langinfo_h.c:7: 
+  function setlocale: precondition 'locale_null_or_valid_string' got status valid.
+[eva] Done for function setlocale
+[eva] computing for function setlocale <- main.
+  Called from langinfo_h.c:8.
+[eva] langinfo_h.c:8: 
+  function setlocale: precondition 'locale_null_or_valid_string' got status valid.
+[eva] Done for function setlocale
+[kernel:annot:missing-spec] langinfo_h.c:10: Warning: 
+  Neither code nor specification for function nl_langinfo,
+   generating default assigns. See -generated-spec-* options for more info
+[eva] computing for function nl_langinfo <- main.
+  Called from langinfo_h.c:10.
+[eva] using specification for function nl_langinfo
+[eva] Done for function nl_langinfo
+[eva] computing for function printf_va_1 <- main.
+  Called from langinfo_h.c:10.
+[eva] using specification for function printf
+[eva:alarm] langinfo_h.c:10: Warning: 
+  function printf_va_1: precondition valid_read_string(param0) got status invalid.
+[eva] langinfo_h.c:10: 
+  function printf_va_1: no state left, precondition valid_read_string(format) got status valid.
+[eva] Done for function printf_va_1
+[eva] Recording results for main
+[eva] Done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  NON TERMINATING FUNCTION

tests/libc/oracle/sys_sem_h.res.oracle

+[kernel] Parsing sys_sem_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
+  
+[kernel:annot:missing-spec] sys_sem_h.c:20: Warning: 
+  Neither code nor specification for function ftok,
+   generating default assigns. See -generated-spec-* options for more info
+[eva] computing for function ftok <- main.
+  Called from sys_sem_h.c:20.
+[eva] using specification for function ftok
+[eva] Done for function ftok
+[eva] computing for function perror <- main.
+  Called from sys_sem_h.c:21.
+[eva] using specification for function perror
+[eva] sys_sem_h.c:21: 
+  function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
+[kernel:annot:missing-spec] sys_sem_h.c:25: Warning: 
+  Neither code nor specification for function semget,
+   generating default assigns. See -generated-spec-* options for more info
+[eva] computing for function semget <- main.
+  Called from sys_sem_h.c:25.
+[eva] using specification for function semget
+[eva] Done for function semget
+[eva] computing for function semget <- main.
+  Called from sys_sem_h.c:28.
+[eva] Done for function semget
+[kernel:annot:missing-spec] sys_sem_h.c:36: Warning: 
+  Neither code nor specification for function semctl,
+   generating default assigns. See -generated-spec-* options for more info
+[eva] computing for function semctl <- main.
+  Called from sys_sem_h.c:36.
+[eva] using specification for function semctl
+[eva] Done for function semctl
+[kernel:annot:missing-spec] sys_sem_h.c:37: Warning: 
+  Neither code nor specification for function semop,
+   generating default assigns. See -generated-spec-* options for more info
+[eva] computing for function semop <- main.
+  Called from sys_sem_h.c:37.
+[eva] using specification for function semop
+[eva] Done for function semop
+[eva] computing for function perror <- main.
+  Called from sys_sem_h.c:38.
+[eva] sys_sem_h.c:38: 
+  function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
+[eva] computing for function semget <- main.
+  Called from sys_sem_h.c:42.
+[eva] Done for function semget
+[eva] computing for function perror <- main.
+  Called from sys_sem_h.c:43.
+[eva] sys_sem_h.c:43: 
+  function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
+[eva] computing for function perror <- main.
+  Called from sys_sem_h.c:48.
+[eva] sys_sem_h.c:48: 
+  function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
+[eva] computing for function semctl <- main.
+  Called from sys_sem_h.c:58.
+[eva] Done for function semctl
+[eva] computing for function perror <- main.
+  Called from sys_sem_h.c:59.
+[eva] sys_sem_h.c:59: 
+  function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
+[eva:alarm] sys_sem_h.c:61: Warning: 
+  accessing uninitialized left-value. assert \initialized(&ds.sem_otime);
+[eva] computing for function semop <- main.
+  Called from sys_sem_h.c:68.
+[eva] Done for function semop
+[eva] computing for function perror <- main.
+  Called from sys_sem_h.c:69.
+[eva] sys_sem_h.c:69: 
+  function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
+[eva] computing for function exit <- main.
+  Called from sys_sem_h.c:69.
+[eva] using specification for function exit
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+  Called from sys_sem_h.c:59.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+  Called from sys_sem_h.c:48.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+  Called from sys_sem_h.c:43.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+  Called from sys_sem_h.c:38.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+  Called from sys_sem_h.c:21.
+[eva] Done for function exit
+[eva] Recording results for main
+[eva] Done for function main
+[eva] sys_sem_h.c:61: assertion 'Eva,initialization' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __fc_stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
+  semkey ∈ [0..4294967294]
+  semid ∈ [--..--]
+  sbuf ∈ [--..--]
+  arg ∈ {0}
+  __retres ∈ {0}

tests/libc/oracle/utmp_h.res.oracle

+[kernel] Parsing utmp_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 system <- main.
+  Called from utmp_h.c:13.
+[eva] using specification for function system
+[eva] utmp_h.c:13: 
+  function system: precondition 'null_or_valid_string_command' got status valid.
+[eva] Done for function system
+[eva] computing for function getpid <- main.
+  Called from utmp_h.c:16.
+[eva] using specification for function getpid
+[eva] Done for function getpid
+[eva] computing for function ttyname <- main.
+  Called from utmp_h.c:17.
+[eva] using specification for function ttyname
+[eva] utmp_h.c:17: 
+  function ttyname: precondition 'valid_fildes' got status valid.
+[eva] Done for function ttyname
+[eva] utmp_h.c:17: Call to builtin strlen
+[eva] utmp_h.c:17: 
+  function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function strcpy <- main.
+  Called from utmp_h.c:17.
+[eva] using specification for function strcpy
+[eva:alarm] utmp_h.c:17: Warning: 
+  function strcpy: precondition 'valid_string_src' got status unknown.
+[eva:alarm] utmp_h.c:17: Warning: 
+  function strcpy: precondition 'room_string' got status unknown.
+[eva] utmp_h.c:17: function strcpy: precondition 'separation' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:441: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
+[eva] Done for function strcpy
+[eva] computing for function ttyname <- main.
+  Called from utmp_h.c:19.
+[eva] utmp_h.c:19: 
+  function ttyname: precondition 'valid_fildes' got status valid.
+[eva] Done for function ttyname
+[eva] utmp_h.c:19: Call to builtin strlen
+[eva] utmp_h.c:19: 
+  function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function strcpy <- main.
+  Called from utmp_h.c:19.
+[eva:alarm] utmp_h.c:19: Warning: 
+  function strcpy: precondition 'valid_string_src' got status unknown.
+[eva:alarm] utmp_h.c:19: Warning: 
+  function strcpy: precondition 'room_string' got status unknown.
+[eva] utmp_h.c:19: function strcpy: precondition 'separation' got status valid.
+[eva] Done for function strcpy
+[eva] computing for function time <- main.
+  Called from utmp_h.c:20.
+[eva] using specification for function time
+[eva] Done for function time
+[eva] computing for function getuid <- main.
+  Called from utmp_h.c:21.
+[eva] using specification for function getuid
+[eva] Done for function getuid
+[eva] computing for function getpwuid <- main.
+  Called from utmp_h.c:21.
+[eva] using specification for function getpwuid
+[eva] Done for function getpwuid
+[eva:alarm] utmp_h.c:21: Warning: 
+  out of bounds read.
+  assert \valid_read(&tmp_4->pw_name);
+  (tmp_4 from getpwuid(getuid()))
+[eva] computing for function strcpy <- main.
+  Called from utmp_h.c:21.
+[eva:alarm] utmp_h.c:21: Warning: 
+  function strcpy: precondition 'valid_string_src' got status unknown.
+[eva:alarm] utmp_h.c:21: Warning: 
+  function strcpy: precondition 'room_string' got status unknown.
+[eva] utmp_h.c:21: function strcpy: precondition 'separation' got status valid.
+[eva] Done for function strcpy
+[eva] utmp_h.c:22: Call to builtin memset
+[eva] utmp_h.c:22: function memset: precondition 'valid_s' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:167: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
+[eva] computing for function setutent <- main.
+  Called from utmp_h.c:24.
+[eva] using specification for function setutent
+[eva] Done for function setutent
+[eva] computing for function pututline <- main.
+  Called from utmp_h.c:25.
+[eva] using specification for function pututline
+[eva:garbled-mix:assigns] utmp_h.c:25: 
+  The specification of function pututline
+  has generated a garbled mix of addresses for assigns clause \result.
+[eva] Done for function pututline
+[eva] computing for function system <- main.
+  Called from utmp_h.c:27.
+[eva] utmp_h.c:27: 
+  function system: precondition 'null_or_valid_string_command' got status valid.
+[eva] Done for function system
+[eva] utmp_h.c:30: Call to builtin memset
+[eva] utmp_h.c:30: function memset: precondition 'valid_s' got status valid.
+[eva] utmp_h.c:32: Call to builtin memset
+[eva] utmp_h.c:32: function memset: precondition 'valid_s' got status valid.
+[eva] computing for function setutent <- main.
+  Called from utmp_h.c:33.
+[eva] Done for function setutent
+[eva] computing for function pututline <- main.
+  Called from utmp_h.c:34.
+[eva:garbled-mix:assigns] utmp_h.c:34: 
+  The specification of function pututline
+  has generated a garbled mix of addresses for assigns clause \result.
+[eva] Done for function pututline
+[eva] computing for function system <- main.
+  Called from utmp_h.c:36.
+[eva] utmp_h.c:36: 
+  function system: precondition 'null_or_valid_string_command' got status valid.
+[eva] Done for function system
+[eva] computing for function endutent <- main.
+  Called from utmp_h.c:38.
+[eva] using specification for function endutent
+[eva] Done for function endutent
+[eva] Recording results for main
+[eva] Done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __fc_pwd.pw_name ∈ {{ &__fc_getpw_pw_name[0] }}
+          .pw_passwd ∈ {{ NULL + [--..--] ; &__fc_getpw_pw_passwd[0] }}
+          {.pw_uid; .pw_gid} ∈ [--..--]
+          .pw_gecos ∈ {{ NULL + [--..--] ; &__fc_getpw_pw_gecos[0] }}
+          .pw_dir ∈ {{ NULL + [--..--] ; &__fc_getpw_pw_dir[0] }}
+          .pw_shell ∈ {{ NULL + [--..--] ; &__fc_getpw_pw_shell[0] }}
+  __fc_utmp ∈ [--..--]
+  entry.ut_type ∈ {8}
+       .[bits 16 to 31] ∈ UNINITIALIZED
+       .ut_pid ∈ [--..--]
+       .ut_line[0..31] ∈ {0}
+       .ut_id[0..3] ∈ [--..--] or UNINITIALIZED
+       {.ut_user[0..31]; .ut_host[0..255]} ∈ {0}
+       {.ut_exit; .ut_session} ∈ [--..--] or UNINITIALIZED
+       .ut_tv.tv_sec ∈ {0}
+       .ut_tv.tv_usec ∈ [--..--] or UNINITIALIZED
+       .ut_addr_v6[0] ∈ {0}
+       {.ut_addr_v6[1..3]; .__glibc_reserved[0..19]} ∈
+       [--..--] or UNINITIALIZED
+  __retres ∈ {0}

tests/libc/sys_sem_h.c

+#include <stdio.h>
+#include <sys/sem.h>
+#include <sys/stat.h>
+#include <errno.h>
+#include <stdlib.h>
+
+// Based on SEMOP(3P) manpage
+
+int main() {
+  key_t semkey;
+  int semid;
+  struct sembuf sbuf;
+  union semun {
+    int val;
+    struct semid_ds *buf;
+    unsigned short *array;
+  } arg;
+  struct semid_ds ds;
+  /* Get unique key for semaphore. */
+  if ((semkey = ftok("/tmp", 'a')) == (key_t) -1) {
+    perror("IPC error: ftok"); exit(1);
+  }
+
+  /* Get semaphore ID associated with this key. */
+  if ((semid = semget(semkey, 0, 0)) == -1) {
+
+    /* Semaphore does not exist - Create. */
+    if ((semid = semget(semkey, 1, IPC_CREAT | IPC_EXCL | S_IRUSR |
+                        S_IWUSR | S_IRGRP | S_IWGRP | S_IROTH | S_IWOTH)) != -1)
+      {
+        /* Initialize the semaphore. */
+        arg.val = 0;
+        sbuf.sem_num = 0;
+        sbuf.sem_op = 2;  /* This is the number of runs without queuing. */
+        sbuf.sem_flg = 0;
+        if (semctl(semid, 0, SETVAL, arg) == -1
+            || semop(semid, &sbuf, 1) == -1) {
+          perror("IPC error: semop"); exit(1);
+        }
+      }
+    else if (errno == EEXIST) {
+      if ((semid = semget(semkey, 0, 0)) == -1) {
+        perror("IPC error 1: semget"); exit(1);
+      }
+      goto check_init;
+    }
+    else {
+      perror("IPC error 2: semget"); exit(1);
+    }
+  }
+  else
+    {
+      /* Check that semid has completed initialization. */
+      /* An application can use a retry loop at this point rather than
+         exiting. */
+    check_init:
+      arg.buf = &ds;
+      if (semctl(semid, 0, IPC_STAT, arg) < 0) {
+        perror("IPC error 3: semctl"); exit(1);
+      }
+      if (ds.sem_otime == 0) {
+        perror("IPC error 4: semctl"); exit(1);
+      }
+    }
+  sbuf.sem_num = 0;
+  sbuf.sem_op = -1;
+  sbuf.sem_flg = SEM_UNDO;
+  if (semop(semid, &sbuf, 1) == -1) {
+    perror("IPC Error: semop"); exit(1);
+  }
+  return 0;
+}

tests/libc/utmp_h.c

+#include <pwd.h>
+#include <stdlib.h>
+#include <string.h>
+#include <time.h>
+#include <unistd.h>
+#include <utmp.h>
+
+// extract based on the getutent(3) man page, 2023-10-31
+
+int main(void) {
+  struct utmp entry;
+
+  system("echo before adding entry:;who");
+
+  entry.ut_type = USER_PROCESS;
+  entry.ut_pid = getpid();
+  strcpy(entry.ut_line, ttyname(STDIN_FILENO) + strlen("/dev/"));
+  /* only correct for ptys named /dev/tty[pqr][0-9a-z] */
+  strcpy(entry.ut_id, ttyname(STDIN_FILENO) + strlen("/dev/tty"));
+  entry.ut_time = time(NULL);
+  strcpy(entry.ut_user, getpwuid(getuid())->pw_name);
+  memset(entry.ut_host, 0, UT_HOSTSIZE);
+  entry.ut_addr = 0;
+  setutent();
+  pututline(&entry);
+
+  system("echo after adding entry:;who");
+
+  entry.ut_type = DEAD_PROCESS;
+  memset(entry.ut_line, 0, UT_LINESIZE);
+  entry.ut_time = 0;
+  memset(entry.ut_user, 0, UT_NAMESIZE);
+  setutent();
+  pututline(&entry);
+
+  system("echo after removing entry:;who");
+
+  endutent();
+  return EXIT_SUCCESS;
+}