diff --git a/share/libc/__fc_machdep.h b/share/libc/__fc_machdep.h
index 34752edcb40c7f10b325068e1670f17831ed9f50..f6f2d7e9a6d71c73f7cc7a786e0f77a6190bce45 100644
--- a/share/libc/__fc_machdep.h
+++ b/share/libc/__fc_machdep.h
@@ -447,6 +447,7 @@
/* Note: MSVC does not define this constant, but because it is used in an ACSL
specification, it is safer to define it anyway. */
#define __FC_HOST_NAME_MAX 255
+#define __FC_TTY_NAME_MAX 32
/* Optional */
#define __INT8_T signed char
diff --git a/share/libc/__fc_machdep_linux_shared.h b/share/libc/__fc_machdep_linux_shared.h
index 0b0760b19e339a05a22e0b114fa8ea815b93216d..ebe92fc6617a09dc6f8640cb84d5b093c4a1eeb5 100644
--- a/share/libc/__fc_machdep_linux_shared.h
+++ b/share/libc/__fc_machdep_linux_shared.h
@@ -102,6 +102,7 @@
#define __FC_PATH_MAX 256
// Note: POSIX requires HOST_NAME_MAX >= 255, but Linux uses 64
#define __FC_HOST_NAME_MAX 64
+#define __FC_TTY_NAME_MAX 32
/* for stdarg.h */
#define __FC_VA_LIST_T __builtin_va_list
diff --git a/share/libc/limits.h b/share/libc/limits.h
index 703571925dcddcba60c9ec3df8feee73d755276f..d42a1f75a550ee2764c4a7091bc6e55a6217172d 100644
--- a/share/libc/limits.h
+++ b/share/libc/limits.h
@@ -85,6 +85,9 @@
Note: Mac OS does not define this constant. */
#define HOST_NAME_MAX __FC_HOST_NAME_MAX
+/* Maximum length of a terminal device name. */
+#define TTY_NAME_MAX __FC_TTY_NAME_MAX
+
/* Maximum length of argument to the exec functions including environment data.
Minimum Acceptable Value: {_POSIX_ARG_MAX} (4096 in POSIX.1-2008)
"... the total space used to store the environment and the arguments to the
diff --git a/share/libc/pwd.h b/share/libc/pwd.h
index 17cca2f73e46b400a9f5656a76902982db557ed3..c93e3126becd9bd2cc455f9cd2783fa1d10ef277 100644
--- a/share/libc/pwd.h
+++ b/share/libc/pwd.h
@@ -26,6 +26,7 @@
__PUSH_FC_STDLIB
#include "__fc_define_uid_and_gid.h"
+#include "__fc_string_axiomatic.h"
// for size_t
#include "stddef.h"
@@ -37,6 +38,7 @@ struct passwd {
char *pw_passwd; // not POSIX, but allowed by it, and present in glibc
uid_t pw_uid;
gid_t pw_gid;
+ char *pw_gecos; // not POSIX, but present in most implementations
char *pw_dir;
char *pw_shell;
};
@@ -48,7 +50,7 @@ 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 =
+struct passwd __fc_pwd =
{.pw_name = __fc_getpwuid_pw_name,
.pw_passwd = __fc_getpwuid_pw_passwd,
.pw_uid = __fc_getpwuid_pw_uid,
@@ -56,16 +58,24 @@ struct passwd __fc_getpwuid =
.pw_dir = __fc_getpwuid_pw_dir,
.pw_shell = __fc_getpwuid_pw_shell};
-struct passwd *__fc_p_getpwuid = & __fc_getpwuid;
+struct passwd *__fc_p_pwd = & __fc_pwd;
+/*@
+ // missing: may assign to errno: EIO, EINTR, EMFILE, ENFILE
+ // missing: assigns \result, __fc_pwd[0..] \from 'password database'
+ requires valid_name: valid_read_string(name);
+ assigns \result \from __fc_p_pwd, indirect:name[0..];
+ assigns __fc_pwd \from indirect:name[0..];
+ ensures result_null_or_internal_struct:
+ \result == \null || \result == __fc_p_pwd;
+*/
+extern struct passwd *getpwnam(const char *name);
-extern struct passwd *getpwnam(const char *);
-
-/*@ // missing: assigns \result, __fc_getpwuid[0..] \from 'password database'
- assigns \result \from __fc_p_getpwuid, indirect:uid;
- assigns __fc_getpwuid \from indirect:uid;
+/*@ // missing: assigns \result, __fc_pwd[0..] \from 'password database'
+ assigns \result \from __fc_p_pwd, indirect:uid;
+ assigns __fc_pwd \from indirect:uid;
ensures result_null_or_internal_struct:
- \result == \null || \result == __fc_p_getpwuid;
+ \result == \null || \result == __fc_p_pwd;
*/
extern struct passwd *getpwuid(uid_t uid);
diff --git a/share/libc/string.h b/share/libc/string.h
index f810f9a8067f6cdceadb0bea39c93ec3bd01c8e8..b9e46ee597ed4f3a042c3289e0490e1fbdea9331 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -374,6 +374,18 @@ extern char *strcpy(char *restrict dest, const char *restrict src);
extern char *strncpy(char *restrict dest,
const char *restrict src, size_t n);
+/*@ // Non-POSIX, but often present
+ @ requires valid_string_src: valid_read_string(src);
+ @ requires room_nstring: \valid(dest+(0..n-1));
+ @ requires separation:
+ @ \separated(dest+(0..n-1), src+(0..\max(n-1,strlen(src))));
+ @ assigns dest[0..n-1] \from src[0..n-1];
+ @ assigns \result \from indirect:src, indirect:src[0..n-1], indirect:n;
+ @ ensures initialization: \initialized(dest+(0..\min(strlen(src),n-1)));
+ @ ensures bounded_result: \result == strlen(src);
+ */
+size_t strlcpy(char * restrict dest, const char * restrict src, size_t n);
+
// stpcpy is POSIX.1-2008
#ifdef _POSIX_C_SOURCE
# if _POSIX_C_SOURCE >= 200809L
@@ -429,6 +441,17 @@ extern char *strcat(char *restrict dest, const char *restrict src);
@*/
extern char *strncat(char *restrict dest, const char *restrict src, size_t n);
+/*@ // Non-POSIX, but often present
+ @ // missing: separation
+ @ requires valid_string_src: valid_read_string(src);
+ @ requires valid_string_dest: valid_string(dest);
+ @ requires room_nstring: \valid(dest+(0..n-1));
+ @ assigns dest[strlen(dest)..n] \from indirect:n, src[0..strlen(src)];
+ @ assigns \result \from indirect:src, indirect:src[0..n-1], indirect:n;
+ @ ensures bounded_result: \result == strlen(dest) + strlen(src);
+ @*/
+extern size_t strlcat(char *restrict dest, const char *restrict src, size_t n);
+
/*@ // missing: separation
@ requires valid_dest: \valid(dest+(0..n - 1));
@ requires valid_string_src: valid_read_string(src);
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index 7edb5316c3ee84e9f688d89f65d67a5a3d34ac02..d3e906a43b37b56b5c7ec700f3017b254d122a95 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -747,7 +747,18 @@ extern unsigned int alarm(unsigned int);
extern int brk(void *);
extern int chdir(const char *path);
extern int chroot(const char *path);
-extern int chown(const char *, uid_t, gid_t);
+
+
+/*@ // missing: may assign to errno: EACCES, ELOOP, ENAMETOOLONG, ENOENT,
+ // ENOTDIR, EROFS, EIO, EINTR, EINVAL
+ // missing: assigns \result \from 'filesystem, permissions'
+ // missing: assigns 'file permissions' \from owner, group;
+ requires valid_string_path: valid_read_string(path);
+ assigns \result \from indirect:path, indirect:path[0..], indirect:owner,
+ indirect:group;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int chown(const char *path, uid_t owner, gid_t group);
/*@
requires valid_fd: 0 <= fd < __FC_MAX_OPEN_FILES;
@@ -812,7 +823,12 @@ extern int execve(const char *path, char *const argv[], char *const env
*/
extern int execvp(const char *path, char *const argv[]);
+/*@
+ assigns \nothing;
+ ensures never_terminates: \false;
+*/
extern void _exit(int) __attribute__ ((__noreturn__));
+
extern int fchown(int, uid_t, gid_t);
extern int fchdir(int);
extern int fdatasync(int);
@@ -908,7 +924,13 @@ extern pid_t getsid(pid_t);
extern uid_t getuid(void);
extern char *getwd(char *);
-extern int isatty(int);
+
+/*@ //missing: may assign to errno: EBADF, ENOTTY (POSIX) / EINVAL (Linux)
+ assigns \result \from indirect:fd, indirect:__fc_fds[fd];
+ ensures result_true_or_false: \result == 0 || \result == 1;
+ */
+extern int isatty(int fd);
+
extern int lchown(const char *, uid_t, gid_t);
extern int link(const char *, const char *);
extern int lockf(int, int, off_t);
@@ -1028,7 +1050,17 @@ extern long int sysconf(int name);
extern pid_t tcgetpgrp(int);
extern int tcsetpgrp(int, pid_t);
extern int truncate(const char *, off_t);
-extern char *ttyname(int);
+
+extern volatile char __fc_ttyname[TTY_NAME_MAX];
+extern char *__fc_p_ttyname = __fc_ttyname;
+
+/*@
+ // missing: may assign to errno: EBADF, ENOTTY
+ assigns \result \from __fc_p_ttyname, indirect:fildes;
+ ensures result_name_or_null: \result == __fc_p_ttyname || \result == \null;
+ */
+extern char *ttyname(int fildes);
+
extern int ttyname_r(int, char *, size_t);
extern useconds_t ualarm(useconds_t, useconds_t);
extern int unlink(const char *);
diff --git a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
index e97d595d452253448f981c86ed558bf51104b2c4..7e86be9c572d9ccbcd807afe986f33adeef1e7d3 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
@@ -1,8 +1,8 @@
-[variadic] FRAMAC_SHARE/libc/unistd.h:784:
+[variadic] FRAMAC_SHARE/libc/unistd.h:795:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:789:
+[variadic] FRAMAC_SHARE/libc/unistd.h:800:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:794:
+[variadic] FRAMAC_SHARE/libc/unistd.h:805:
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 *.
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index d71aa38a8b712bf367843c6b8bf435fb29b87c80..1b512fc679b89c4510d6b4a843c1a11641ac3bb6 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -1,8 +1,8 @@
-[variadic] FRAMAC_SHARE/libc/unistd.h:784:
+[variadic] FRAMAC_SHARE/libc/unistd.h:795:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:789:
+[variadic] FRAMAC_SHARE/libc/unistd.h:800:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:794:
+[variadic] FRAMAC_SHARE/libc/unistd.h:805:
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:
diff --git a/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle b/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
index 089a6c792a3d13ee3a71b2ea68cb5da2a0cf4b0f..3bdfda3fde92ac91809fd788abeebf71639c9929 100644
--- a/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
@@ -1,8 +1,8 @@
-[variadic] FRAMAC_SHARE/libc/unistd.h:784:
+[variadic] FRAMAC_SHARE/libc/unistd.h:795:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:789:
+[variadic] FRAMAC_SHARE/libc/unistd.h:800:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:794:
+[variadic] FRAMAC_SHARE/libc/unistd.h:805:
Declaration of variadic function execlp.
[variadic] tests/known/exec_failed_requirement.c:7:
Translating call to execl to a call to execv.
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 056a7d23f9316f95d9dada935a0a42ab3796252d..34325075722573f2b05936a38e2822674bfdb142 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -1547,6 +1547,23 @@
[ Valid ] Behavior 'partial'
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function 'strlcpy'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'initialization'
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition 'bounded_result'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/string.h, line 382)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 382)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 383)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'strcat'
--------------------------------------------------------------------------------
@@ -1559,11 +1576,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'result_ptr'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 397)
+[ Extern ] Assigns (file share/libc/string.h, line 409)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 397)
+[ Extern ] Froms (file share/libc/string.h, line 409)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 400)
+[ Extern ] Froms (file share/libc/string.h, line 412)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1578,23 +1595,23 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'partial' 'sum_of_bounded_lengths'
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'complete' (file share/libc/string.h, line 417)
+[ Extern ] Assigns for 'complete' (file share/libc/string.h, line 429)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 411)
+[ Extern ] Assigns (file share/libc/string.h, line 423)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 425)
+[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 437)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'complete' (file share/libc/string.h, line 417)
+[ Extern ] Froms for 'complete' (file share/libc/string.h, line 429)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'complete' (file share/libc/string.h, line 419)
+[ Extern ] Froms for 'complete' (file share/libc/string.h, line 431)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 411)
+[ Extern ] Froms (file share/libc/string.h, line 423)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 412)
+[ Extern ] Froms (file share/libc/string.h, line 424)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'partial' (file share/libc/string.h, line 425)
+[ Extern ] Froms for 'partial' (file share/libc/string.h, line 437)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'partial' (file share/libc/string.h, line 427)
+[ Extern ] Froms for 'partial' (file share/libc/string.h, line 439)
Unverifiable but considered Valid.
[ Valid ] Behavior 'complete'
by Frama-C kernel.
@@ -1603,15 +1620,30 @@
[ Valid ] Behavior 'partial'
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function 'strlcat'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'bounded_result'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/string.h, line 449)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 449)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 450)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'strxfrm'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/string.h, line 435)
+[ Extern ] Assigns (file share/libc/string.h, line 458)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 435)
+[ Extern ] Froms (file share/libc/string.h, line 458)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 436)
+[ Extern ] Froms (file share/libc/string.h, line 459)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1626,19 +1658,19 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'no_allocation' 'result_null'
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 447)
+[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 470)
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Extern ] Assigns for 'no_allocation' nothing
Unverifiable but considered Valid.
-[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 447)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 470)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 448)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 471)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 444)
+[ Extern ] Froms (file share/libc/string.h, line 467)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 454)
+[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 477)
Unverifiable but considered Valid.
[ Valid ] Behavior 'allocation'
by Frama-C kernel.
@@ -1646,7 +1678,7 @@
by Frama-C kernel.
[ Valid ] Behavior 'no_allocation'
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 443)
+[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 466)
Unverifiable but considered Valid.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid.
@@ -1661,19 +1693,19 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'no_allocation' 'result_null'
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 465)
+[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 488)
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Extern ] Assigns for 'no_allocation' nothing
Unverifiable but considered Valid.
-[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 465)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 488)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 466)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 489)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 461)
+[ Extern ] Froms (file share/libc/string.h, line 484)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 475)
+[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 498)
Unverifiable but considered Valid.
[ Valid ] Behavior 'allocation'
by Frama-C kernel.
@@ -1681,7 +1713,7 @@
by Frama-C kernel.
[ Valid ] Behavior 'no_allocation'
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 460)
+[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 483)
Unverifiable but considered Valid.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid.
@@ -2134,9 +2166,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 156 Completely validated
- 216 Considered valid
+ 158 Completely validated
+ 225 Considered valid
29 To be validated
4 Alarms emitted
- 405 Total
+ 416 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index 6c5fe3be202d1c7a64d8bd4f0dbc15e336cac7d4..81b8f86a27e7a7a613c8d725aaf40e1ee5d8ad51 100644
--- a/tests/libc/oracle/coverage.res.oracle
+++ b/tests/libc/oracle/coverage.res.oracle
@@ -28,7 +28,7 @@
main: 4 stmts out of 4 (100.0%)
[metrics] Eva coverage statistics
=======================
- Syntactically reachable functions = 2 (out of 76)
+ Syntactically reachable functions = 2 (out of 78)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index b48eca2cad51fdf2242e6c45aedffac3c1f01bc1..32c4f831a3aca48a4593fe3ed92573a3f2dd412b 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -38,7 +38,7 @@
wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call);
wmemset (0 call);
- Undefined functions (360)
+ Undefined functions (367)
=========================
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 (1 call);
@@ -64,43 +64,44 @@
__va_fcntl_int (0 call); __va_fcntl_void (0 call); __va_ioctl_int (0 call);
__va_ioctl_ptr (0 call); __va_ioctl_void (0 call);
__va_open_mode_t (0 call); __va_open_void (0 call);
- __va_openat_mode_t (0 call); __va_openat_void (0 call); abort (0 call);
- accept (0 call); access (0 call); acos (0 call); acosf (0 call);
- acosh (0 call); acoshf (0 call); acoshl (0 call); acosl (0 call);
- 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); 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 (2 calls); inet_ntoa (0 call); inet_ntop (0 call);
- inet_pton (0 call); isascii (0 call); kill (0 call); labs (0 call);
+ __va_openat_mode_t (0 call); __va_openat_void (0 call); _exit (0 call);
+ abort (0 call); accept (0 call); access (0 call); acos (0 call);
+ acosf (0 call); acosh (0 call); acoshf (0 call); acoshl (0 call);
+ acosl (0 call); 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); 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); 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); 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); 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);
@@ -134,28 +135,30 @@
sinl (0 call); socket (0 call); socketpair (0 call); sqrt (0 call);
sqrtf (0 call); sqrtl (0 call); srand (0 call); srand48 (0 call);
srandom (0 call); stat (0 call); strcoll (0 call); strcspn (0 call);
- strftime (0 call); strncasecmp (0 call); strpbrk (0 call); strsep (0 call);
- strspn (0 call); strtod (0 call); strtof (0 call); strtoimax (0 call);
- strtok (0 call); strtok_r (0 call); strtol (0 call); strtold (0 call);
- strtoll (0 call); strtoul (0 call); strtoull (0 call); strxfrm (0 call);
- sync (0 call); sysconf (0 call); syslog (0 call); system (0 call);
- tcgetattr (0 call); tcsetattr (0 call); time (0 call); times (0 call);
- tmpfile (0 call); tmpnam (0 call); trunc (0 call); truncf (0 call);
- truncl (0 call); tzset (0 call); umask (0 call); ungetc (0 call);
- usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
- vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
- vsyslog (0 call); wait (0 call); waitpid (0 call); wcschr (0 call);
- wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
- wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
- wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
- wmemcmp (0 call); wmemmove (0 call); write (0 call);
+ strftime (0 call); strlcat (0 call); strlcpy (0 call); strncasecmp (0 call);
+ strpbrk (0 call); strsep (0 call); strspn (0 call); strtod (0 call);
+ strtof (0 call); strtoimax (0 call); strtok (0 call); strtok_r (0 call);
+ strtol (0 call); strtold (0 call); strtoll (0 call); strtoul (0 call);
+ strtoull (0 call); strxfrm (0 call); sync (0 call); sysconf (0 call);
+ syslog (0 call); system (0 call); tcgetattr (0 call); tcsetattr (0 call);
+ time (0 call); times (0 call); tmpfile (0 call); tmpnam (0 call);
+ trunc (0 call); truncf (0 call); truncl (0 call); ttyname (0 call);
+ tzset (0 call); umask (0 call); ungetc (0 call); usleep (0 call);
+ utimes (0 call); vfprintf (0 call); vfscanf (0 call); vprintf (0 call);
+ vscanf (0 call); vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call);
+ wait (0 call); waitpid (0 call); wcschr (0 call); wcscmp (0 call);
+ wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call);
+ wcspbrk (0 call); wcsrchr (0 call); 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 (17)
+ 'Extern' global variables (18)
==============================
__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
+ __fc_strerror; __fc_ttyname; __fc_wctomb_state; optarg; opterr; optopt;
+ tzname
Potential entry points (1)
==========================
@@ -165,13 +168,13 @@
==============
Sloc = 1026
Decision point = 195
- Global variables = 59
+ Global variables = 61
If = 186
Loop = 42
Goto = 84
Assignment = 415
Exit point = 76
- Function = 436
+ Function = 443
Function call = 84
Pointer dereferencing = 157
Cyclomatic complexity = 271
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8fbee9224b0558cc49a4f482ba14631703f85fe3..e56f5e98e8c872547a2d14eb5df95aa6a03e182f 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -310,6 +310,7 @@ struct passwd {
char *pw_passwd ;
uid_t pw_uid ;
gid_t pw_gid ;
+ char *pw_gecos ;
char *pw_dir ;
char *pw_shell ;
};
@@ -3473,10 +3474,42 @@ char *strcpy(char *dest, char const *src);
char *strncpy(char *dest, char const *src, size_t n);
+/*@ requires valid_string_src: valid_read_string(src);
+ requires room_nstring: \valid(dest + (0 .. n - 1));
+ requires
+ separation:
+ \separated(
+ dest + (0 .. n - 1), src + (0 .. \max(n - 1, strlen(src)))
+ );
+ ensures
+ initialization:
+ \initialized(\old(dest) + (0 .. \min(strlen(\old(src)), \old(n) - 1)));
+ ensures bounded_result: \result ≡ strlen(\old(src));
+ assigns *(dest + (0 .. n - 1)), \result;
+ assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
+ assigns \result
+ \from (indirect: src), (indirect: *(src + (0 .. n - 1))), (indirect: n);
+ */
+size_t strlcpy(char * __restrict dest, char const * __restrict src, size_t n);
+
char *strcat(char *dest, char const *src);
char *strncat(char *dest, char const *src, size_t n);
+/*@ requires valid_string_src: valid_read_string(src);
+ requires valid_string_dest: valid_string(dest);
+ requires room_nstring: \valid(dest + (0 .. n - 1));
+ ensures
+ bounded_result: \result ≡ strlen(\old(dest)) + strlen(\old(src));
+ assigns *(dest + (strlen{Old}(dest) .. n)), \result;
+ assigns *(dest + (strlen{Old}(dest) .. n))
+ \from (indirect: n), *(src + (0 .. strlen{Old}(src)));
+ assigns \result
+ \from (indirect: src), (indirect: *(src + (0 .. n - 1))), (indirect: n);
+ */
+extern size_t strlcat(char * __restrict dest, char const * __restrict src,
+ size_t n);
+
/*@ requires valid_dest: \valid(dest + (0 .. n - 1));
requires valid_string_src: valid_read_string(src);
assigns *(dest + (0 .. n - 1)), \result;
@@ -6758,20 +6791,31 @@ extern char __fc_getpwuid_pw_dir[64];
extern char __fc_getpwuid_pw_shell[64];
-struct passwd __fc_getpwuid =
+struct passwd __fc_pwd =
{.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_gecos = (char *)0,
.pw_dir = __fc_getpwuid_pw_dir,
.pw_shell = __fc_getpwuid_pw_shell};
-struct passwd *__fc_p_getpwuid = & __fc_getpwuid;
+struct passwd *__fc_p_pwd = & __fc_pwd;
+/*@ requires valid_name: valid_read_string(name);
+ ensures
+ result_null_or_internal_struct:
+ \result ≡ \null ∨ \result ≡ __fc_p_pwd;
+ assigns \result, __fc_pwd;
+ assigns \result \from __fc_p_pwd, (indirect: *(name + (0 ..)));
+ assigns __fc_pwd \from (indirect: *(name + (0 ..)));
+ */
+extern struct passwd *getpwnam(char const *name);
+
/*@ 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);
+ \result ≡ \null ∨ \result ≡ __fc_p_pwd;
+ assigns \result, __fc_pwd;
+ assigns \result \from __fc_p_pwd, (indirect: uid);
+ assigns __fc_pwd \from (indirect: uid);
*/
extern struct passwd *getpwuid(uid_t uid);
@@ -7011,6 +7055,15 @@ 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 ..))),
+ (indirect: owner), (indirect: group);
+ */
+extern int chown(char const *path, uid_t owner, gid_t group);
+
/*@ requires valid_fd: 0 ≤ fd < 1024;
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns __fc_fds[fd], \result;
@@ -7084,6 +7137,10 @@ extern int execve(char const *path, char * const *argv, char * const *env);
*/
extern int execvp(char const *path, char * const *argv);
+/*@ ensures never_terminates: \false;
+ assigns \nothing; */
+extern __attribute__((__noreturn__)) void _exit(int);
+
/*@ ensures
result_ok_child_or_error:
\result ≡ 0 ∨ \result > 0 ∨ \result ≡ -1;
@@ -7150,6 +7207,12 @@ extern pid_t getsid(pid_t);
assigns \result \from \nothing; */
extern uid_t getuid(void);
+/*@ ensures result_true_or_false: \result ≡ 0 ∨ \result ≡ 1;
+ assigns \result;
+ assigns \result \from (indirect: fd), (indirect: __fc_fds[fd]);
+ */
+extern int isatty(int fd);
+
/*@ requires valid_path: valid_read_string(path);
assigns \result;
assigns \result \from (indirect: *(path + (0 ..))), (indirect: name);
@@ -7231,6 +7294,16 @@ extern void sync(void);
assigns \result \from (indirect: name); */
extern long sysconf(int name);
+extern char volatile __fc_ttyname[32];
+
+char *__fc_p_ttyname = (char *)(__fc_ttyname);
+/*@ ensures
+ result_name_or_null: \result ≡ __fc_p_ttyname ∨ \result ≡ \null;
+ assigns \result;
+ assigns \result \from __fc_p_ttyname, (indirect: fildes);
+ */
+extern char *ttyname(int fildes);
+
/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns \result, Frama_C_entropy_source;
assigns \result
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index d928b74c99c4288108e90321e18e9267c38640e8..1ceb0a03241f85b3da6db15f8f7abcaed67fc928 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -14,6 +14,7 @@
\return(getenv) == 0 (auto)
\return(bsearch) == 0 (auto)
\return(getcwd) == 0 (auto)
+ \return(ttyname) == 0 (auto)
\return(memchr) == 0 (auto)
\return(memcpy) == 0 (auto)
\return(memmove) == 0 (auto)
diff --git a/tests/libc/oracle/pwd_h.res.oracle b/tests/libc/oracle/pwd_h.res.oracle
index 3eca6d0e89b983073071c40135ceee07c627421e..d0fdf54a69e71a2fbb4baea87e475e354e6a9645 100644
--- a/tests/libc/oracle/pwd_h.res.oracle
+++ b/tests/libc/oracle/pwd_h.res.oracle
@@ -12,16 +12,24 @@
[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] computing for function getpwnam <- main.
+ Called from tests/libc/pwd_h.c:18.
+[eva] using specification for function getpwnam
+[eva] tests/libc/pwd_h.c:18:
+ function getpwnam: precondition 'valid_name' got status valid.
+[eva] Done for function getpwnam
+[eva:alarm] tests/libc/pwd_h.c:21: Warning: assertion got status unknown.
+[eva:alarm] tests/libc/pwd_h.c:22: Warning: assertion got status unknown.
+[eva:alarm] tests/libc/pwd_h.c:23: Warning: assertion got status unknown.
+[eva:alarm] tests/libc/pwd_h.c:24: 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 }}
+ __fc_pwd.pw_name ∈ {{ NULL + [--..--] ; &__fc_getpwuid_pw_name[0] }}
+ .pw_passwd ∈ {{ NULL + [--..--] ; &__fc_getpwuid_pw_passwd[0] }}
+ {.pw_uid; .pw_gid; .pw_gecos} ∈ [--..--]
+ .pw_dir ∈ {{ NULL + [--..--] ; &__fc_getpwuid_pw_dir[0] }}
+ .pw_shell ∈ {{ NULL + [--..--] ; &__fc_getpwuid_pw_shell[0] }}
+ pw ∈ {{ NULL ; &__fc_pwd }}
__retres ∈ {0}
diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index b49c71f34ab5dea43bd062fa944ac47d83a35cb9..7dc1cf2aedc6feefe779fa8f9084dddffb19c524 100644
--- a/tests/libc/oracle/string_c.res.oracle
+++ b/tests/libc/oracle/string_c.res.oracle
@@ -485,13 +485,13 @@
function strlen: precondition 'valid_string_s' got status valid.
[eva] Recording results for strlen
[eva] Done for function strlen
-[eva] share/libc/string.h:399:
+[eva] share/libc/string.h:411:
function strcat: postcondition 'sum_of_lengths' got status valid.
-[eva] share/libc/string.h:402:
+[eva] share/libc/string.h:414:
function strcat: postcondition 'initialization,dest' got status valid.
-[eva] share/libc/string.h:403:
+[eva] share/libc/string.h:415:
function strcat: postcondition 'dest_null_terminated' got status valid.
-[eva] share/libc/string.h:404:
+[eva] share/libc/string.h:416:
function strcat: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcat
[eva] Done for function strcat
diff --git a/tests/libc/oracle/string_c_generic.res.oracle b/tests/libc/oracle/string_c_generic.res.oracle
index 091a7fd4bb210c9e210866854ed63890331776e6..3431164e2afbe4604967c749dada73fe8b96d09e 100644
--- a/tests/libc/oracle/string_c_generic.res.oracle
+++ b/tests/libc/oracle/string_c_generic.res.oracle
@@ -252,9 +252,9 @@
function strlen: postcondition 'acsl_c_equiv' got status valid.
[eva] Recording results for strlen
[eva] Done for function strlen
-[eva] share/libc/string.h:413:
+[eva] share/libc/string.h:425:
function strncat: postcondition 'result_ptr' got status valid.
-[eva] share/libc/string.h:428:
+[eva] share/libc/string.h:440:
function strncat, behavior partial: postcondition 'sum_of_bounded_lengths' got status valid.
[eva] Recording results for strncat
[eva] Done for function strncat
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index e9d3b49300859231b11a81fb34ae09a42caddeac..dd500d0409a4378d30868ee18d352a65de94c277 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -256,6 +256,35 @@
Consider adding ./share/libc/string.c to the analyzed source files.
[eva] tests/libc/string_h.c:120: Warning: ignoring unsupported \allocates clause
[eva] Done for function strndup
+[eva] computing for function strlcpy <- main.
+ Called from tests/libc/string_h.c:124.
+[eva] using specification for function strlcpy
+[eva] tests/libc/string_h.c:124:
+ function strlcpy: precondition 'valid_string_src' got status valid.
+[eva] tests/libc/string_h.c:124:
+ function strlcpy: precondition 'room_nstring' got status valid.
+[eva] tests/libc/string_h.c:124:
+ function strlcpy: precondition 'separation' got status valid.
+[eva] Done for function strlcpy
+[eva] computing for function strlcpy <- main.
+ Called from tests/libc/string_h.c:125.
+[eva] tests/libc/string_h.c:125:
+ function strlcpy: precondition 'valid_string_src' got status valid.
+[eva] tests/libc/string_h.c:125:
+ function strlcpy: precondition 'room_nstring' got status valid.
+[eva] tests/libc/string_h.c:125:
+ function strlcpy: precondition 'separation' got status valid.
+[eva] Done for function strlcpy
+[eva] computing for function strlcat <- main.
+ Called from tests/libc/string_h.c:126.
+[eva] using specification for function strlcat
+[eva:alarm] tests/libc/string_h.c:126: Warning:
+ function strlcat: precondition 'valid_string_src' got status unknown.
+[eva:alarm] tests/libc/string_h.c:126: Warning:
+ function strlcat: precondition 'valid_string_dest' got status unknown.
+[eva] tests/libc/string_h.c:126:
+ function strlcat: precondition 'room_nstring' got status valid.
+[eva] Done for function strlcat
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -301,4 +330,10 @@
__fc_strtok_ptr ∈ {{ "constant!" + [0..--] }}
a ∈ [--..--]
b ∈ [--..--]
+ buf[0..15] ∈ [--..--]
+ buf2[0..5] ∈ [--..--]
+ [6..31] ∈ [--..--] or UNINITIALIZED
+ r1 ∈ {18}
+ r2 ∈ {5}
+ r3 ∈ [--..--]
__retres ∈ {0}
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index b3c282aca8b923b282ddb7a0b4b20aef5ee7ef9f..8acd40bd2d4580f5b0bed8763e743d007b0da385 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -1,9 +1,11 @@
[kernel] Parsing tests/libc/unistd_h.c (with preprocessing)
[eva] Splitting return states on:
\return(access) == 0 (auto)
+ \return(chown) == 0 (auto)
\return(dup) == -1 (auto)
\return(getcwd) == 0 (auto)
\return(gethostname) == 0 (auto)
+ \return(isatty) == 0 (auto)
\return(setegid) == 0 (auto)
\return(seteuid) == 0 (auto)
\return(setgid) == 0 (auto)
@@ -11,6 +13,7 @@
\return(setreuid) == 0 (auto)
\return(setsid) == 0 (auto)
\return(setuid) == 0 (auto)
+ \return(ttyname) == 0 (auto)
\return(usleep) == 0 (auto)
\return(getresuid) == 0 (auto)
\return(setresuid) == 0 (auto)
@@ -468,6 +471,36 @@
[eva] computing for function setreuid <- main.
Called from tests/libc/unistd_h.c:74.
[eva] Done for function setreuid
+[eva] computing for function isatty <- main.
+ Called from tests/libc/unistd_h.c:76.
+[eva] using specification for function isatty
+[eva] Done for function isatty
+[eva] computing for function isatty <- main.
+ Called from tests/libc/unistd_h.c:76.
+[eva] Done for function isatty
+[eva] tests/libc/unistd_h.c:77: assertion got status valid.
+[eva] computing for function ttyname <- main.
+ Called from tests/libc/unistd_h.c:78.
+[eva] using specification for function ttyname
+[eva] Done for function ttyname
+[eva] computing for function ttyname <- main.
+ Called from tests/libc/unistd_h.c:78.
+[eva] Done for function ttyname
+[eva] computing for function chown <- main.
+ Called from tests/libc/unistd_h.c:80.
+[eva] using specification for function chown
+[eva] tests/libc/unistd_h.c:80:
+ function chown: precondition 'valid_string_path' got status valid.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+ Called from tests/libc/unistd_h.c:80.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+ Called from tests/libc/unistd_h.c:80.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+ Called from tests/libc/unistd_h.c:80.
+[eva] Done for function chown
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -491,4 +524,5 @@
egid ∈ [--..--] or UNINITIALIZED
sgid ∈ [--..--] or UNINITIALIZED
p ∈ [--..--]
+ tty ∈ {{ NULL ; &__fc_ttyname[0] }}
__retres ∈ {0; 1}
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 2b8e38fde21be6b2a210316f37aea41ee8d236a8..39a11b77b4e4ae5530789d3936f5737a6b77bc10 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -1,9 +1,11 @@
[kernel] Parsing tests/libc/unistd_h.c (with preprocessing)
[eva] Splitting return states on:
\return(access) == 0 (auto)
+ \return(chown) == 0 (auto)
\return(dup) == -1 (auto)
\return(getcwd) == 0 (auto)
\return(gethostname) == 0 (auto)
+ \return(isatty) == 0 (auto)
\return(setegid) == 0 (auto)
\return(seteuid) == 0 (auto)
\return(setgid) == 0 (auto)
@@ -11,6 +13,7 @@
\return(setreuid) == 0 (auto)
\return(setsid) == 0 (auto)
\return(setuid) == 0 (auto)
+ \return(ttyname) == 0 (auto)
\return(usleep) == 0 (auto)
\return(getresuid) == 0 (auto)
\return(setresuid) == 0 (auto)
@@ -468,6 +471,36 @@
[eva] computing for function setreuid <- main.
Called from tests/libc/unistd_h.c:74.
[eva] Done for function setreuid
+[eva] computing for function isatty <- main.
+ Called from tests/libc/unistd_h.c:76.
+[eva] using specification for function isatty
+[eva] Done for function isatty
+[eva] computing for function isatty <- main.
+ Called from tests/libc/unistd_h.c:76.
+[eva] Done for function isatty
+[eva] tests/libc/unistd_h.c:77: assertion got status valid.
+[eva] computing for function ttyname <- main.
+ Called from tests/libc/unistd_h.c:78.
+[eva] using specification for function ttyname
+[eva] Done for function ttyname
+[eva] computing for function ttyname <- main.
+ Called from tests/libc/unistd_h.c:78.
+[eva] Done for function ttyname
+[eva] computing for function chown <- main.
+ Called from tests/libc/unistd_h.c:80.
+[eva] using specification for function chown
+[eva] tests/libc/unistd_h.c:80:
+ function chown: precondition 'valid_string_path' got status valid.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+ Called from tests/libc/unistd_h.c:80.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+ Called from tests/libc/unistd_h.c:80.
+[eva] Done for function chown
+[eva] computing for function chown <- main.
+ Called from tests/libc/unistd_h.c:80.
+[eva] Done for function chown
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -491,4 +524,5 @@
egid ∈ [--..--] or UNINITIALIZED
sgid ∈ [--..--] or UNINITIALIZED
p ∈ [--..--]
+ tty ∈ {{ NULL ; &__fc_ttyname[0] }}
__retres ∈ {0; 1}
diff --git a/tests/libc/pwd_h.c b/tests/libc/pwd_h.c
index 78abed115d3dfb2967fac487d9e6b7ce46e7c1a4..6d69824821e5b461d73a218a0c7ccb7d93ace3de 100644
--- a/tests/libc/pwd_h.c
+++ b/tests/libc/pwd_h.c
@@ -15,4 +15,12 @@ int main() {
//@ assert valid_read_string(pw->pw_dir);
//@ assert valid_read_string(pw->pw_shell);
}
+ pw = getpwnam("root");
+ 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);
+ }
}
diff --git a/tests/libc/string_h.c b/tests/libc/string_h.c
index 600dfa7008399c4f088136387c9da04e1a72e782..9dd3b05c2b9d5cce31c68fd7529a0fb11d3a73d1 100644
--- a/tests/libc/string_h.c
+++ b/tests/libc/string_h.c
@@ -118,5 +118,11 @@ int main(int argc, char **argv)
test_strtok_r();
char *a = strdup("bla"); // unsound; specification currently unsupported
char *b = strndup("bla", 2); // unsound; specification currently unsupported
+
+ char buf[16];
+ char buf2[32];
+ size_t r1 = strlcpy(buf, "longer than buffer", 16);
+ size_t r2 = strlcpy(buf2, "short", 16);
+ size_t r3 = strlcat(buf2, buf, 32);
return 0;
}
diff --git a/tests/libc/unistd_h.c b/tests/libc/unistd_h.c
index d0f26a9bb533cfcd4ecc21ea3368c432382d277c..d665ec88fa9055339d43cb3ba706867b93bee864 100644
--- a/tests/libc/unistd_h.c
+++ b/tests/libc/unistd_h.c
@@ -73,5 +73,10 @@ int main() {
r = setregid(rgid, egid);
r = setreuid(ruid, euid);
+ r = isatty(1);
+ //@ assert r == 0 || r == 1;
+ char *tty = ttyname(1);
+
+ r = chown("/tmp/a.txt", 01000, 01000);
return 0;
}