diff --git a/tests/libc/dirent_h.c b/tests/libc/dirent_h.c new file mode 100644 index 0000000000000000000000000000000000000000..858b0264bcfcf12eb7974cf43f2fccfcb2952f57 --- /dev/null +++ b/tests/libc/dirent_h.c @@ -0,0 +1,41 @@ +// 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; +} diff --git a/tests/libc/langinfo_h.c b/tests/libc/langinfo_h.c new file mode 100644 index 0000000000000000000000000000000000000000..b4665fe044e8322dc2074937ee585db21cc2233e --- /dev/null +++ b/tests/libc/langinfo_h.c @@ -0,0 +1,14 @@ +#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; +} diff --git a/tests/libc/oracle/dirent_h.res.oracle b/tests/libc/oracle/dirent_h.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..f702224612b7705f5d168daccdab03c0c3b1d264 --- /dev/null +++ b/tests/libc/oracle/dirent_h.res.oracle @@ -0,0 +1,70 @@ +[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:garbled-mix:assigns] dirent_h.c:23: + The specification of function readdir + has generated a garbled mix of addresses for assigns clause __fc_errno. +[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 ∈ + {{ garbled mix of &{__fc_opendir} + (origin: Library function {dirent_h.c:23}) }} + __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] ∈ [--..--] diff --git a/tests/libc/oracle/langinfo_h.res.oracle b/tests/libc/oracle/langinfo_h.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..ad179177763407379da1d4b0c83b5674e5eff032 --- /dev/null +++ b/tests/libc/oracle/langinfo_h.res.oracle @@ -0,0 +1,37 @@ +[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 diff --git a/tests/libc/oracle/sys_sem_h.res.oracle b/tests/libc/oracle/sys_sem_h.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..85ea5aa1481e6f602bec130fab957d3fdee73d84 --- /dev/null +++ b/tests/libc/oracle/sys_sem_h.res.oracle @@ -0,0 +1,109 @@ +[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} diff --git a/tests/libc/oracle/utmp_h.res.oracle b/tests/libc/oracle/utmp_h.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..9240a6b3f17331d3fc8cdedfbc49aeaba129cd04 --- /dev/null +++ b/tests/libc/oracle/utmp_h.res.oracle @@ -0,0 +1,142 @@ +[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} diff --git a/tests/libc/sys_sem_h.c b/tests/libc/sys_sem_h.c new file mode 100644 index 0000000000000000000000000000000000000000..d0dc820347ba5553d41213270c1f138b8ba8e3f1 --- /dev/null +++ b/tests/libc/sys_sem_h.c @@ -0,0 +1,72 @@ +#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; +} diff --git a/tests/libc/utmp_h.c b/tests/libc/utmp_h.c new file mode 100644 index 0000000000000000000000000000000000000000..496569bad7e303afb3adc785479588bc0270288d --- /dev/null +++ b/tests/libc/utmp_h.c @@ -0,0 +1,40 @@ +#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; +}