From 0a02f7e9306dc44fc76ef1bca0304fe9502dc36a Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 22 Jan 2019 18:58:39 +0100
Subject: [PATCH] [Libc] add several specs
---
share/libc/signal.h | 32 +++-
share/libc/stdlib.h | 12 +-
share/libc/string.h | 15 +-
share/libc/unistd.h | 34 +++-
tests/builtins/oracle/imprecise.res.oracle | 12 ++
tests/builtins/oracle/memcpy.res.oracle | 25 ++-
tests/builtins/oracle/memcpy2.res.oracle | 2 +
tests/builtins/oracle/strnlen.res.oracle | 2 +
tests/builtins/oracle/write-const.res.oracle | 8 +
tests/libc/oracle/coverage.res.oracle | 2 +-
tests/libc/oracle/fc_libc.0.res.oracle | 102 +++++------
tests/libc/oracle/fc_libc.1.res.oracle | 96 ++++++++++
tests/libc/oracle/netdb_c.res.oracle | 1 +
tests/libc/oracle/signal_h.res.oracle | 177 +++++++++++++++++++
tests/libc/oracle/stdlib_h.res.oracle | 8 +
tests/libc/oracle/string_h.res.oracle | 30 ++--
tests/libc/oracle/unistd_h.0.res.oracle | 50 ++++--
tests/libc/oracle/unistd_h.1.res.oracle | 50 ++++--
tests/libc/signal_h.c | 11 ++
tests/libc/stdlib_h.c | 4 +
tests/libc/string_h.c | 3 +-
tests/libc/unistd_h.c | 4 +
22 files changed, 576 insertions(+), 104 deletions(-)
diff --git a/share/libc/signal.h b/share/libc/signal.h
index f1eb5d6cc1b..d39758a71cc 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -96,7 +96,8 @@ typedef __fc_sighandler_t sig_t;
#define SIGSYS 31
#define SIGUNUSED 31
-
+#define SIGRTMIN 32
+#define SIGRTMAX 64
#define SA_NOCLDSTOP 0x00000001
#define SA_NOCLDWAIT 0x00000002
@@ -198,9 +199,25 @@ extern int sigdelset(sigset_t *set, int signum);
*/
extern int sigismember(const sigset_t *set, int signum);
-extern int sigaction(int signum, const struct sigaction *act,
- struct sigaction *oldact);
-
+extern struct sigaction __fc_sigaction[SIGRTMAX+1];
+extern struct sigaction *__fc_p_sigaction = __fc_sigaction;
+
+/*@ // missing: errno may be set to EINVAL when trying to set some signals
+ requires valid_signal: 0 <= signum <= SIGRTMAX;
+ requires valid_oldact_or_null: oldact == \null || \valid(oldact);
+ requires valid_read_act_or_null: act == \null || \valid_read(act);
+ requires separation:separated_acts: \separated(act, oldact);
+ assigns oldact == \null ? \empty : *oldact \from __fc_p_sigaction;
+ assigns act == \null ? \empty : __fc_p_sigaction[signum] \from *act;
+ assigns \result \from indirect:signum, indirect:act, indirect:*act,
+ indirect:oldact, indirect:*oldact;
+ ensures act_changed: act == \null || \subset(__fc_p_sigaction[signum], *act);
+ ensures oldact_assigned: oldact == \null ||
+ \subset({*oldact}, __fc_p_sigaction[signum]);
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+ */
+extern int sigaction(int signum, const struct sigaction *restrict act,
+ struct sigaction *restrict oldact);
/*@ // missing: assigns *oldset \from 'previous mask in process'
requires valid_set_or_null: set == \null || \valid_read(set);
@@ -226,6 +243,13 @@ extern int sigprocmask(int how, const sigset_t * restrict set,
*/
extern int kill(pid_t pid, int sig);
+/*@ // missing: errno may be set to EINVAL, EPERM, ESRCH
+ // missing: assigns 'other processes' \from 'other processes'
+ assigns \result \from indirect:pgrp, indirect: sig;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int killpg(pid_t pgrp, int sig);
+
__END_DECLS
__POP_FC_STDLIB
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index e69ed2aa5b7..98a172ccdb0 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -593,7 +593,6 @@ extern size_t wcstombs(char * restrict s,
const wchar_t * restrict pwcs,
size_t n);
-
// Note: this specification should ideally use a more specific predicate,
// such as 'is_allocable_aligned(alignment, size)'.
/*@
@@ -622,6 +621,17 @@ extern size_t wcstombs(char * restrict s,
*/
extern int posix_memalign(void **memptr, size_t alignment, size_t size);
+/*@
+ // missing: requires 'last 6 characters of template must be XXXXXX'
+ // missing: assigns \result, template[0..] \from 'filesystem', 'RNG';
+ requires valid_template: valid_string(template);
+ assigns template[0..] \from \nothing;
+ assigns \result \from \nothing;
+ ensures result_error_or_valid_fd: \result == -1 ||
+ 0 <= \result < __FC_FOPEN_MAX;
+ */
+extern int mkstemp(char *template);
+
__END_DECLS
__POP_FC_STDLIB
diff --git a/share/libc/string.h b/share/libc/string.h
index b9e46ee597e..1721e2dde50 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -502,15 +502,24 @@ extern char *strdup (const char *s);
extern char *strndup (const char *s, size_t n);
// More POSIX, non-C99 functions
-#ifdef _POSIX_C_SOURCE
extern char *stpncpy(char *restrict dest, const char *restrict src, size_t n);
//extern int strcoll_l(const char *s1, const char *s2, locale_t locale);
//extern char *strerror_l(int errnum, locale_t locale);
extern int strerror_r(int errnum, char *strerrbuf, size_t buflen);
-extern char *strsignal(int sig);
+
+extern char __fc_strsignal[64];
+char * const __fc_p_strsignal = __fc_strsignal;
+
+/*@ //missing: requires valid_signal(signum);
+ @ assigns \result \from __fc_p_strsignal, indirect:signum;
+ @ ensures result_internal_str: \result == __fc_p_strsignal;
+ @ ensures result_nul_terminated: \result[63] == 0;
+ @ ensures result_valid_string: valid_read_string(\result);
+ @*/
+extern char *strsignal(int signum);
+
//extern size_t strxfrm_l(char *restrict s1, const char *restrict s2, size_t n,
// locale_t locale);
-#endif
__END_DECLS
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index d3e906a43b3..a966cf7cbf7 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -900,7 +900,15 @@ extern char *getlogin(void);
extern int getlogin_r(char *, size_t);
extern int getpagesize(void);
extern char *getpass(const char *);
-extern pid_t getpgid(pid_t);
+
+/*@ //missing: assigns \result \from 'process PGID'
+ assigns \result \from indirect:pid;
+*/
+extern pid_t getpgid(pid_t pid);
+
+/*@ //missing: assigns \result \from 'calling process PGID'
+ assigns \result \from \nothing;
+*/
extern pid_t getpgrp(void);
/*@ //missing: assigns \result \from 'process id'
@@ -998,7 +1006,13 @@ extern int seteuid(uid_t uid);
*/
extern int setgid(gid_t gid);
-extern int setpgid(pid_t, pid_t);
+/*@ // missing: may assign to errno
+ // missing: assigns \result \from 'processes'
+ assigns \result \from indirect:pid, indirect:pgid;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int setpgid(pid_t pid, pid_t pgid);
+
extern pid_t setpgrp(void);
/*@ // missing: may assign errno to EINVAL, EPERM or EAGAIN
@@ -1063,12 +1077,16 @@ 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 *);
-// usleep is not POSIX anymore since 200809
-#if (_XOPEN_SOURCE >= 500) && ! (_POSIX_C_SOURCE >= 200809L) \
- || /* Glibc since 2.19: */ defined _DEFAULT_SOURCE \
- || /* Glibc versions <= 2.19: */ defined _BSD_SOURCE
+/*@ // missing: may assign errno
+ // missing: assigns 'filesystem' \from path[0..];
+ // missing: assigns \result \from 'filesystem';
+ requires valid_string_path: valid_read_string(path);
+ assigns \result \from path[0..];
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+ */
+extern int unlink(const char *path);
+
/*@
assigns \result \from indirect:usec, indirect:Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
@@ -1076,8 +1094,6 @@ extern int unlink(const char *);
*/
extern int usleep(useconds_t usec);
-#endif
-
extern pid_t vfork(void);
/*@
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index 14a7a8fc9c7..d77f1466122 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -59,6 +59,8 @@
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
i ∈ {1}
j ∈ {1; 2}
k[0..4] ∈ [--..--]
@@ -143,6 +145,8 @@
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
v ∈ [--..--]
addr ∈ [--..--]
v1.[bits 0 to 7] ∈ {1}
@@ -179,6 +183,8 @@
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
v ∈ [--..--]
addr ∈ [--..--]
v1.[bits 0 to 7] ∈ {1}
@@ -624,6 +630,8 @@
__fc_strtok_ptr ∈ {{ NULL ; &S___fc_strtok_ptr[0] }}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
i ∈ {1}
j ∈ {1; 2}
k[0..4] ∈ [--..--]
@@ -702,6 +710,8 @@
__fc_strtok_ptr ∈ {{ NULL ; &S___fc_strtok_ptr[0] }}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
v ∈ [--..--]
addr ∈ [--..--]
v1.[bits 0 to 7] ∈ {1}
@@ -741,6 +751,8 @@
__fc_strtok_ptr ∈ {{ NULL ; &S___fc_strtok_ptr[0] }}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
v ∈ [--..--]
addr ∈ [--..--]
v1.[bits 0 to 7] ∈ {1}
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 34325075722..c767cf17fb5 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -400,6 +400,8 @@
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
i ∈ [--..--]
src[0..19] ∈ {0}
dst1[0..19] ∈ {0}
@@ -1718,6 +1720,23 @@
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid.
+--------------------------------------------------------------------------------
+--- Properties of Function 'strsignal'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'result_internal_str'
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition 'result_nul_terminated'
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition 'result_valid_string'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 514)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'bzero'
--------------------------------------------------------------------------------
@@ -2166,9 +2185,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 158 Completely validated
- 225 Considered valid
+ 159 Completely validated
+ 230 Considered valid
29 To be validated
4 Alarms emitted
- 416 Total
+ 422 Total
--------------------------------------------------------------------------------
diff --git a/tests/builtins/oracle/memcpy2.res.oracle b/tests/builtins/oracle/memcpy2.res.oracle
index bd415ec9eac..912286440a4 100644
--- a/tests/builtins/oracle/memcpy2.res.oracle
+++ b/tests/builtins/oracle/memcpy2.res.oracle
@@ -27,6 +27,8 @@
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
c ∈ [--..--]
v ∈ {{ NULL ; &S_v[0] }}
t[0..510] ∈ {0} or UNINITIALIZED
diff --git a/tests/builtins/oracle/strnlen.res.oracle b/tests/builtins/oracle/strnlen.res.oracle
index 9cacd457242..097bcf8ac85 100644
--- a/tests/builtins/oracle/strnlen.res.oracle
+++ b/tests/builtins/oracle/strnlen.res.oracle
@@ -47,6 +47,8 @@
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
t1[0] ∈ {97}
[1] ∈ {98}
[2] ∈ {99}
diff --git a/tests/builtins/oracle/write-const.res.oracle b/tests/builtins/oracle/write-const.res.oracle
index 35487069277..8b39ca3d183 100644
--- a/tests/builtins/oracle/write-const.res.oracle
+++ b/tests/builtins/oracle/write-const.res.oracle
@@ -24,6 +24,8 @@
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
v ∈ [--..--]
a ∈ {-1}
b ∈ {1}
@@ -49,6 +51,8 @@
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
v ∈ [--..--]
a ∈ {-1}
b ∈ {84215045}
@@ -71,6 +75,8 @@
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
v ∈ [--..--]
a ∈ {-1}
b ∈ {1}
@@ -92,6 +98,8 @@
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
__fc_p_strerror ∈ {{ &__fc_strerror[0] }}
+ __fc_strsignal[0..63] ∈ [--..--]
+ __fc_p_strsignal ∈ {{ &__fc_strsignal[0] }}
v ∈ [--..--]
a ∈ {-1}
b ∈ {2}
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index 81b8f86a27e..abb4e7886a7 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 78)
+ Syntactically reachable functions = 2 (out of 80)
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 32c4f831a3a..461bda59470 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 (367)
+ Undefined functions (375)
=========================
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);
@@ -93,25 +93,26 @@
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);
- logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
- malloc (7 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
- memoverlap (1 call); mkdir (0 call); mktime (0 call); nan (0 call);
- nanf (0 call); nanl (0 call); nanosleep (0 call); ntohl (0 call);
- ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
- openlog (0 call); pathconf (0 call); pclose (0 call); perror (0 call);
- pipe (0 call); poll (0 call); popen (0 call); pow (0 call); powf (0 call);
+ 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); kill (0 call);
+ killpg (0 call); labs (0 call); ldiv (0 call); listen (0 call);
+ llabs (0 call); lldiv (0 call); localtime (0 call); log (0 call);
+ log10 (0 call); log10f (0 call); log10l (0 call); log2 (0 call);
+ log2f (0 call); log2l (0 call); logf (0 call); logl (0 call);
+ longjmp (0 call); lrand48 (0 call); malloc (7 calls); mblen (0 call);
+ mbstowcs (0 call); mbtowc (0 call); memoverlap (1 call); mkdir (0 call);
+ mkstemp (0 call); mktime (0 call); nan (0 call); nanf (0 call);
+ nanl (0 call); nanosleep (0 call); ntohl (0 call); ntohs (0 call);
+ open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
+ pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
+ poll (0 call); popen (0 call); pow (0 call); powf (0 call);
pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
pthread_cond_init (0 call); pthread_cond_wait (0 call);
pthread_create (0 call); pthread_join (0 call);
@@ -125,40 +126,41 @@
roundf (0 call); roundl (0 call); select (0 call); send (0 call);
setbuf (0 call); setegid (0 call); seteuid (0 call); setgid (0 call);
sethostname (0 call); setitimer (0 call); setjmp (0 call);
- setlogmask (0 call); setpriority (0 call); setregid (0 call);
- setresgid (0 call); setresuid (0 call); setreuid (0 call);
- setrlimit (0 call); setsid (0 call); setsockopt (0 call);
+ setlogmask (0 call); setpgid (0 call); setpriority (0 call);
+ setregid (0 call); setresgid (0 call); setresuid (0 call);
+ setreuid (0 call); setrlimit (0 call); setsid (0 call); setsockopt (0 call);
settimeofday (0 call); setuid (0 call); setvbuf (0 call); shutdown (0 call);
- sigaddset (0 call); sigdelset (0 call); sigemptyset (0 call);
- sigfillset (0 call); sigismember (0 call); siglongjmp (0 call);
- signal (0 call); sigprocmask (0 call); sin (0 call); sinf (0 call);
- 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); 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);
+ sigaction (0 call); sigaddset (0 call); sigdelset (0 call);
+ sigemptyset (0 call); sigfillset (0 call); sigismember (0 call);
+ siglongjmp (0 call); signal (0 call); sigprocmask (0 call); sin (0 call);
+ sinf (0 call); 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); strlcat (0 call); strlcpy (0 call);
+ strncasecmp (0 call); strpbrk (0 call); strsep (0 call); strsignal (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); unlink (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 (18)
+ 'Extern' global variables (20)
==============================
__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_ttyname; __fc_wctomb_state; optarg; opterr; optopt;
- tzname
+ __fc_sigaction; __fc_strerror; __fc_strsignal; __fc_ttyname;
+ __fc_wctomb_state; optarg; opterr; optopt; tzname
Potential entry points (1)
==========================
@@ -168,13 +170,13 @@
==============
Sloc = 1026
Decision point = 195
- Global variables = 61
+ Global variables = 65
If = 186
Loop = 42
Goto = 84
Assignment = 415
Exit point = 76
- Function = 443
+ Function = 451
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 e56f5e98e8c..88c0df5a8f9 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -122,6 +122,28 @@ typedef int pid_t;
typedef unsigned int gid_t;
typedef unsigned int uid_t;
typedef unsigned long sigset_t;
+union sigval {
+ int sival_int ;
+ void *sival_ptr ;
+};
+struct __anonstruct_siginfo_t_20 {
+ int si_signo ;
+ int si_code ;
+ union sigval si_value ;
+ int si_errno ;
+ pid_t si_pid ;
+ uid_t si_uid ;
+ void *si_addr ;
+ int si_status ;
+ int si_band ;
+};
+typedef struct __anonstruct_siginfo_t_20 siginfo_t;
+struct sigaction {
+ void (*sa_handler)(int ) ;
+ void (*sa_sigaction)(int , siginfo_t *, void *) ;
+ sigset_t sa_mask ;
+ int sa_flags ;
+};
typedef unsigned int socklen_t;
typedef unsigned short sa_family_t;
struct sockaddr {
@@ -1923,6 +1945,15 @@ extern size_t wcstombs(char * __restrict s, wchar_t const * __restrict pwcs,
int posix_memalign(void **memptr, size_t alignment, size_t size);
+/*@ requires valid_template: valid_string(template);
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(template + (0 ..)), \result;
+ assigns *(template + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+extern int mkstemp(char *template);
+
int glob(char const *pattern, int flags,
int (*errfunc)(char const *epath, int eerrno), glob_t *pglob)
{
@@ -2898,6 +2929,33 @@ extern int sigdelset(sigset_t *set, int signum);
*/
extern int sigismember(sigset_t const *set, int signum);
+extern struct sigaction __fc_sigaction[64 + 1];
+
+struct sigaction *__fc_p_sigaction = __fc_sigaction;
+/*@ requires valid_signal: 0 ≤ signum ≤ 64;
+ requires valid_oldact_or_null: oldact ≡ \null ∨ \valid(oldact);
+ requires valid_read_act_or_null: act ≡ \null ∨ \valid_read(act);
+ requires separation: separated_acts: \separated(act, oldact);
+ ensures
+ act_changed:
+ \old(act) ≡ \null ∨
+ \subset(*(__fc_p_sigaction + \old(signum)), *\old(act));
+ ensures
+ oldact_assigned:
+ \old(oldact) ≡ \null ∨
+ *\old(oldact) ∈ *(__fc_p_sigaction + \old(signum));
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns oldact ≡ \null? \empty: *oldact,
+ act ≡ \null? \empty: *(__fc_p_sigaction + signum), \result;
+ assigns oldact ≡ \null? \empty: *oldact \from __fc_p_sigaction;
+ assigns act ≡ \null? \empty: *(__fc_p_sigaction + signum) \from *act;
+ assigns \result
+ \from (indirect: signum), (indirect: act), (indirect: *act),
+ (indirect: oldact), (indirect: *oldact);
+ */
+extern int sigaction(int signum, struct sigaction const * __restrict act,
+ struct sigaction * __restrict oldact);
+
/*@ requires valid_set_or_null: set ≡ \null ∨ \valid_read(set);
requires valid_how: set ≢ \null ⇒ how ∈ {0, 2, 1};
requires valid_oldset_or_null: oldset ≡ \null ∨ \valid(oldset);
@@ -2923,6 +2981,12 @@ extern int sigprocmask(int how, sigset_t const * __restrict set,
*/
extern int kill(pid_t pid, int sig);
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result \from (indirect: pgrp), (indirect: sig);
+ */
+extern int killpg(pid_t pgrp, int sig);
+
/*@ ghost struct __fc_sockfds_type __fc_sockfds[1024]; */
/*@ ghost extern int __fc_socket_counter __attribute__((__FRAMA_C_MODEL__));
*/
@@ -3524,6 +3588,17 @@ char *strdup(char const *s);
char *strndup(char const *s, size_t n);
+extern char __fc_strsignal[64];
+
+char * const __fc_p_strsignal = __fc_strsignal;
+/*@ ensures result_internal_str: \result ≡ __fc_p_strsignal;
+ ensures result_nul_terminated: *(\result + 63) ≡ 0;
+ ensures result_valid_string: valid_read_string(\result);
+ assigns \result;
+ assigns \result \from __fc_p_strsignal, (indirect: signum);
+ */
+extern char *strsignal(int signum);
+
/*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
ensures
s_initialized: initialization:
@@ -7191,6 +7266,14 @@ extern int gethostname(char *name, size_t len);
*/
extern int sethostname(char const *name, size_t len);
+/*@ assigns \result;
+ assigns \result \from (indirect: pid); */
+extern pid_t getpgid(pid_t pid);
+
+/*@ assigns \result;
+ assigns \result \from \nothing; */
+extern pid_t getpgrp(void);
+
/*@ assigns \result;
assigns \result \from \nothing; */
extern pid_t getpid(void);
@@ -7263,6 +7346,12 @@ extern int seteuid(uid_t uid);
*/
extern int setgid(gid_t gid);
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result \from (indirect: pid), (indirect: pgid);
+ */
+extern int setpgid(pid_t pid, pid_t pgid);
+
/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
assigns \result \from (indirect: rgid), (indirect: egid);
@@ -7304,6 +7393,13 @@ char *__fc_p_ttyname = (char *)(__fc_ttyname);
*/
extern char *ttyname(int fildes);
+/*@ requires valid_string_path: valid_read_string(path);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result \from *(path + (0 ..));
+ */
+extern int unlink(char const *path);
+
/*@ 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 1ceb0a03241..fcd756cf744 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -33,6 +33,7 @@
\return(strncat) == 0 (auto)
\return(strdup) == 0 (auto)
\return(strndup) == 0 (auto)
+ \return(strsignal) == 0 (auto)
\return(bind) == 0 (auto)
\return(socket) == -1 (auto)
\return(signal) == 0 (auto)
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 1d3c95b0de4..f09d621e64d 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -99,12 +99,189 @@
Called from tests/libc/signal_h.c:42.
[eva] using specification for function kill
[eva] Done for function kill
+[eva] computing for function sigaction <- main.
+ Called from tests/libc/signal_h.c:45.
+[eva] using specification for function sigaction
+[eva] tests/libc/signal_h.c:45:
+ function sigaction: precondition 'valid_signal' got status valid.
+[eva] tests/libc/signal_h.c:45:
+ function sigaction: precondition 'valid_oldact_or_null' got status valid.
+[eva] tests/libc/signal_h.c:45:
+ function sigaction: precondition 'valid_read_act_or_null' got status valid.
+[eva] tests/libc/signal_h.c:45:
+ function sigaction: precondition 'separation,separated_acts' got status valid.
+[eva] Done for function sigaction
+[eva] computing for function sigaction <- main.
+ Called from tests/libc/signal_h.c:45.
+[eva] Done for function sigaction
+[eva] computing for function sigaction <- main.
+ Called from tests/libc/signal_h.c:48.
+[eva] tests/libc/signal_h.c:48:
+ function sigaction: precondition 'valid_signal' got status valid.
+[eva] tests/libc/signal_h.c:48:
+ function sigaction: precondition 'valid_oldact_or_null' got status valid.
+[eva] tests/libc/signal_h.c:48:
+ function sigaction: precondition 'valid_read_act_or_null' got status valid.
+[eva] tests/libc/signal_h.c:48:
+ function sigaction: precondition 'separation,separated_acts' got status valid.
+[eva] share/libc/signal.h:214:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic coercion struct sigaction -> set<struct sigaction>
+[eva] Done for function sigaction
+[eva] computing for function sigaction <- main.
+ Called from tests/libc/signal_h.c:51.
+[eva] tests/libc/signal_h.c:51:
+ function sigaction: precondition 'valid_signal' got status valid.
+[eva] tests/libc/signal_h.c:51:
+ function sigaction: precondition 'valid_oldact_or_null' got status valid.
+[eva] tests/libc/signal_h.c:51:
+ function sigaction: precondition 'valid_read_act_or_null' got status valid.
+[eva] tests/libc/signal_h.c:51:
+ function sigaction: precondition 'separation,separated_acts' got status valid.
+[eva] Done for function sigaction
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_sigaction[0]{.sa_handler; .sa_sigaction} ∈ {0}
+ [0]{.sa_mask; .sa_flags} ∈ [--..--]
+ [1]{.sa_handler; .sa_sigaction} ∈ {0}
+ [1]{.sa_mask; .sa_flags} ∈ [--..--]
+ [2]{.sa_handler; .sa_sigaction} ∈ {0}
+ [2]{.sa_mask; .sa_flags} ∈ [--..--]
+ [3]{.sa_handler; .sa_sigaction} ∈ {0}
+ [3]{.sa_mask; .sa_flags} ∈ [--..--]
+ [4]{.sa_handler; .sa_sigaction} ∈ {0}
+ [4]{.sa_mask; .sa_flags} ∈ [--..--]
+ [5]{.sa_handler; .sa_sigaction} ∈ {0}
+ [5]{.sa_mask; .sa_flags} ∈ [--..--]
+ [6]{.sa_handler; .sa_sigaction} ∈ {0}
+ [6]{.sa_mask; .sa_flags} ∈ [--..--]
+ [7]{.sa_handler; .sa_sigaction} ∈ {0}
+ [7]{.sa_mask; .sa_flags} ∈ [--..--]
+ [8]{.sa_handler; .sa_sigaction} ∈ {0}
+ [8]{.sa_mask; .sa_flags} ∈ [--..--]
+ [9]{.sa_handler; .sa_sigaction} ∈ {0}
+ [9]{.sa_mask; .sa_flags} ∈ [--..--]
+ [10] ∈
+ {{ garbled mix of &{__fc_sigaction}
+ (origin: Library function) }}
+ [11]{.sa_handler; .sa_sigaction} ∈ {0}
+ [11]{.sa_mask; .sa_flags} ∈ [--..--]
+ [12]{.sa_handler; .sa_sigaction} ∈ {0}
+ [12]{.sa_mask; .sa_flags} ∈ [--..--]
+ [13]{.sa_handler; .sa_sigaction} ∈ {0}
+ [13]{.sa_mask; .sa_flags} ∈ [--..--]
+ [14]{.sa_handler; .sa_sigaction} ∈ {0}
+ [14]{.sa_mask; .sa_flags} ∈ [--..--]
+ [15]{.sa_handler; .sa_sigaction} ∈ {0}
+ [15]{.sa_mask; .sa_flags} ∈ [--..--]
+ [16]{.sa_handler; .sa_sigaction} ∈ {0}
+ [16]{.sa_mask; .sa_flags} ∈ [--..--]
+ [17]{.sa_handler; .sa_sigaction} ∈ {0}
+ [17]{.sa_mask; .sa_flags} ∈ [--..--]
+ [18] ∈
+ {{ garbled mix of &{__fc_sigaction}
+ (origin: Library function) }}
+ [19]{.sa_handler; .sa_sigaction} ∈ {0}
+ [19]{.sa_mask; .sa_flags} ∈ [--..--]
+ [20]{.sa_handler; .sa_sigaction} ∈ {0}
+ [20]{.sa_mask; .sa_flags} ∈ [--..--]
+ [21]{.sa_handler; .sa_sigaction} ∈ {0}
+ [21]{.sa_mask; .sa_flags} ∈ [--..--]
+ [22]{.sa_handler; .sa_sigaction} ∈ {0}
+ [22]{.sa_mask; .sa_flags} ∈ [--..--]
+ [23]{.sa_handler; .sa_sigaction} ∈ {0}
+ [23]{.sa_mask; .sa_flags} ∈ [--..--]
+ [24]{.sa_handler; .sa_sigaction} ∈ {0}
+ [24]{.sa_mask; .sa_flags} ∈ [--..--]
+ [25]{.sa_handler; .sa_sigaction} ∈ {0}
+ [25]{.sa_mask; .sa_flags} ∈ [--..--]
+ [26]{.sa_handler; .sa_sigaction} ∈ {0}
+ [26]{.sa_mask; .sa_flags} ∈ [--..--]
+ [27]{.sa_handler; .sa_sigaction} ∈ {0}
+ [27]{.sa_mask; .sa_flags} ∈ [--..--]
+ [28]{.sa_handler; .sa_sigaction} ∈ {0}
+ [28]{.sa_mask; .sa_flags} ∈ [--..--]
+ [29]{.sa_handler; .sa_sigaction} ∈ {0}
+ [29]{.sa_mask; .sa_flags} ∈ [--..--]
+ [30]{.sa_handler; .sa_sigaction} ∈ {0}
+ [30]{.sa_mask; .sa_flags} ∈ [--..--]
+ [31]{.sa_handler; .sa_sigaction} ∈ {0}
+ [31]{.sa_mask; .sa_flags} ∈ [--..--]
+ [32]{.sa_handler; .sa_sigaction} ∈ {0}
+ [32]{.sa_mask; .sa_flags} ∈ [--..--]
+ [33]{.sa_handler; .sa_sigaction} ∈ {0}
+ [33]{.sa_mask; .sa_flags} ∈ [--..--]
+ [34]{.sa_handler; .sa_sigaction} ∈ {0}
+ [34]{.sa_mask; .sa_flags} ∈ [--..--]
+ [35]{.sa_handler; .sa_sigaction} ∈ {0}
+ [35]{.sa_mask; .sa_flags} ∈ [--..--]
+ [36]{.sa_handler; .sa_sigaction} ∈ {0}
+ [36]{.sa_mask; .sa_flags} ∈ [--..--]
+ [37]{.sa_handler; .sa_sigaction} ∈ {0}
+ [37]{.sa_mask; .sa_flags} ∈ [--..--]
+ [38]{.sa_handler; .sa_sigaction} ∈ {0}
+ [38]{.sa_mask; .sa_flags} ∈ [--..--]
+ [39]{.sa_handler; .sa_sigaction} ∈ {0}
+ [39]{.sa_mask; .sa_flags} ∈ [--..--]
+ [40]{.sa_handler; .sa_sigaction} ∈ {0}
+ [40]{.sa_mask; .sa_flags} ∈ [--..--]
+ [41]{.sa_handler; .sa_sigaction} ∈ {0}
+ [41]{.sa_mask; .sa_flags} ∈ [--..--]
+ [42]{.sa_handler; .sa_sigaction} ∈ {0}
+ [42]{.sa_mask; .sa_flags} ∈ [--..--]
+ [43]{.sa_handler; .sa_sigaction} ∈ {0}
+ [43]{.sa_mask; .sa_flags} ∈ [--..--]
+ [44]{.sa_handler; .sa_sigaction} ∈ {0}
+ [44]{.sa_mask; .sa_flags} ∈ [--..--]
+ [45]{.sa_handler; .sa_sigaction} ∈ {0}
+ [45]{.sa_mask; .sa_flags} ∈ [--..--]
+ [46]{.sa_handler; .sa_sigaction} ∈ {0}
+ [46]{.sa_mask; .sa_flags} ∈ [--..--]
+ [47]{.sa_handler; .sa_sigaction} ∈ {0}
+ [47]{.sa_mask; .sa_flags} ∈ [--..--]
+ [48]{.sa_handler; .sa_sigaction} ∈ {0}
+ [48]{.sa_mask; .sa_flags} ∈ [--..--]
+ [49]{.sa_handler; .sa_sigaction} ∈ {0}
+ [49]{.sa_mask; .sa_flags} ∈ [--..--]
+ [50]{.sa_handler; .sa_sigaction} ∈ {0}
+ [50]{.sa_mask; .sa_flags} ∈ [--..--]
+ [51]{.sa_handler; .sa_sigaction} ∈ {0}
+ [51]{.sa_mask; .sa_flags} ∈ [--..--]
+ [52]{.sa_handler; .sa_sigaction} ∈ {0}
+ [52]{.sa_mask; .sa_flags} ∈ [--..--]
+ [53]{.sa_handler; .sa_sigaction} ∈ {0}
+ [53]{.sa_mask; .sa_flags} ∈ [--..--]
+ [54]{.sa_handler; .sa_sigaction} ∈ {0}
+ [54]{.sa_mask; .sa_flags} ∈ [--..--]
+ [55]{.sa_handler; .sa_sigaction} ∈ {0}
+ [55]{.sa_mask; .sa_flags} ∈ [--..--]
+ [56]{.sa_handler; .sa_sigaction} ∈ {0}
+ [56]{.sa_mask; .sa_flags} ∈ [--..--]
+ [57]{.sa_handler; .sa_sigaction} ∈ {0}
+ [57]{.sa_mask; .sa_flags} ∈ [--..--]
+ [58]{.sa_handler; .sa_sigaction} ∈ {0}
+ [58]{.sa_mask; .sa_flags} ∈ [--..--]
+ [59]{.sa_handler; .sa_sigaction} ∈ {0}
+ [59]{.sa_mask; .sa_flags} ∈ [--..--]
+ [60]{.sa_handler; .sa_sigaction} ∈ {0}
+ [60]{.sa_mask; .sa_flags} ∈ [--..--]
+ [61]{.sa_handler; .sa_sigaction} ∈ {0}
+ [61]{.sa_mask; .sa_flags} ∈ [--..--]
+ [62]{.sa_handler; .sa_sigaction} ∈ {0}
+ [62]{.sa_mask; .sa_flags} ∈ [--..--]
+ [63]{.sa_handler; .sa_sigaction} ∈ {0}
+ [63]{.sa_mask; .sa_flags} ∈ [--..--]
+ [64]{.sa_handler; .sa_sigaction} ∈ {0}
+ [64]{.sa_mask; .sa_flags} ∈ [--..--]
s ∈ [--..--]
uninit ∈ UNINITIALIZED
old ∈ [--..--] or UNINITIALIZED
kill_res ∈ {-1; 0}
+ sa1 ∈
+ {{ garbled mix of &{__fc_sigaction}
+ (origin: Library function) }} or UNINITIALIZED
+ sa2 ∈
+ {{ garbled mix of &{__fc_sigaction}
+ (origin: Library function {tests/libc/signal_h.c:48}) }} or UNINITIALIZED
__retres ∈ {-1; 0; 1; 2; 3}
diff --git a/tests/libc/oracle/stdlib_h.res.oracle b/tests/libc/oracle/stdlib_h.res.oracle
index c9beadd4b2c..f5a2bec1be1 100644
--- a/tests/libc/oracle/stdlib_h.res.oracle
+++ b/tests/libc/oracle/stdlib_h.res.oracle
@@ -232,6 +232,12 @@
function bsearch: precondition 'valid_function_compar' got status valid.
[eva] Done for function bsearch
[eva:alarm] tests/libc/stdlib_h.c:68: Warning: assertion got status unknown.
+[eva] computing for function mkstemp <- main.
+ Called from tests/libc/stdlib_h.c:82.
+[eva] using specification for function mkstemp
+[eva] tests/libc/stdlib_h.c:82:
+ function mkstemp: precondition 'valid_template' got status valid.
+[eva] Done for function mkstemp
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -261,4 +267,6 @@
[3] ∈ {20}
key ∈ {-1}
p ∈ {{ &ai[1] }}
+ tempFilename[0..9] ∈ [--..--]
+ r ∈ [-1..19]
__retres ∈ {0}
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index dd500d0409a..913d0fe0a7c 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -257,34 +257,39 @@
[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.
+ Called from tests/libc/string_h.c:123.
[eva] using specification for function strlcpy
-[eva] tests/libc/string_h.c:124:
+[eva] tests/libc/string_h.c:123:
function strlcpy: precondition 'valid_string_src' got status valid.
-[eva] tests/libc/string_h.c:124:
+[eva] tests/libc/string_h.c:123:
function strlcpy: precondition 'room_nstring' got status valid.
-[eva] tests/libc/string_h.c:124:
+[eva] tests/libc/string_h.c:123:
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:
+ Called from tests/libc/string_h.c:124.
+[eva] tests/libc/string_h.c:124:
function strlcpy: precondition 'valid_string_src' got status valid.
-[eva] tests/libc/string_h.c:125:
+[eva] tests/libc/string_h.c:124:
function strlcpy: precondition 'room_nstring' got status valid.
-[eva] tests/libc/string_h.c:125:
+[eva] tests/libc/string_h.c:124:
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.
+ Called from tests/libc/string_h.c:125.
[eva] using specification for function strlcat
-[eva:alarm] tests/libc/string_h.c:126: Warning:
+[eva:alarm] tests/libc/string_h.c:125: Warning:
function strlcat: precondition 'valid_string_src' got status unknown.
-[eva:alarm] tests/libc/string_h.c:126: Warning:
+[eva:alarm] tests/libc/string_h.c:125: Warning:
function strlcat: precondition 'valid_string_dest' got status unknown.
-[eva] tests/libc/string_h.c:126:
+[eva] tests/libc/string_h.c:125:
function strlcat: precondition 'room_nstring' got status valid.
[eva] Done for function strlcat
+[eva] computing for function strsignal <- main.
+ Called from tests/libc/string_h.c:126.
+[eva] using specification for function strsignal
+[eva] Done for function strsignal
+[eva] tests/libc/string_h.c:127: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -336,4 +341,5 @@
r1 ∈ {18}
r2 ∈ {5}
r3 ∈ [--..--]
+ strsig ∈ {{ &__fc_strsignal[0] }}
__retres ∈ {0}
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 8acd40bd2d4..78a30b4a80a 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -5,15 +5,18 @@
\return(dup) == -1 (auto)
\return(getcwd) == 0 (auto)
\return(gethostname) == 0 (auto)
+ \return(getpgrp) == 0 (auto)
\return(isatty) == 0 (auto)
\return(setegid) == 0 (auto)
\return(seteuid) == 0 (auto)
\return(setgid) == 0 (auto)
+ \return(setpgid) == 0 (auto)
\return(setregid) == 0 (auto)
\return(setreuid) == 0 (auto)
\return(setsid) == 0 (auto)
\return(setuid) == 0 (auto)
\return(ttyname) == 0 (auto)
+ \return(unlink) == 0 (auto)
\return(usleep) == 0 (auto)
\return(getresuid) == 0 (auto)
\return(setresuid) == 0 (auto)
@@ -471,35 +474,62 @@
[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.
+[eva] computing for function getpgid <- main.
+ Called from tests/libc/unistd_h.c:75.
+[eva] using specification for function getpgid
+[eva] Done for function getpgid
+[eva] computing for function getpgid <- main.
+ Called from tests/libc/unistd_h.c:75.
+[eva] Done for function getpgid
+[eva] computing for function setpgid <- main.
+ Called from tests/libc/unistd_h.c:75.
+[eva] using specification for function setpgid
+[eva] Done for function setpgid
+[eva] computing for function setpgid <- main.
+ Called from tests/libc/unistd_h.c:75.
+[eva] Done for function setpgid
+[eva] computing for function getpgrp <- main.
+ Called from tests/libc/unistd_h.c:76.
+[eva] using specification for function getpgrp
+[eva] Done for function getpgrp
+[eva] computing for function getpgrp <- main.
Called from tests/libc/unistd_h.c:76.
+[eva] Done for function getpgrp
+[eva] computing for function unlink <- main.
+ Called from tests/libc/unistd_h.c:78.
+[eva] using specification for function unlink
+[eva] tests/libc/unistd_h.c:78:
+ function unlink: precondition 'valid_string_path' got status valid.
+[eva] Done for function unlink
+[eva] computing for function isatty <- main.
+ Called from tests/libc/unistd_h.c:80.
[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.
+ Called from tests/libc/unistd_h.c:80.
[eva] Done for function isatty
-[eva] tests/libc/unistd_h.c:77: assertion got status valid.
+[eva] tests/libc/unistd_h.c:81: assertion got status valid.
[eva] computing for function ttyname <- main.
- Called from tests/libc/unistd_h.c:78.
+ Called from tests/libc/unistd_h.c:82.
[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.
+ Called from tests/libc/unistd_h.c:82.
[eva] Done for function ttyname
[eva] computing for function chown <- main.
- Called from tests/libc/unistd_h.c:80.
+ Called from tests/libc/unistd_h.c:84.
[eva] using specification for function chown
-[eva] tests/libc/unistd_h.c:80:
+[eva] tests/libc/unistd_h.c:84:
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.
+ Called from tests/libc/unistd_h.c:84.
[eva] Done for function chown
[eva] computing for function chown <- main.
- Called from tests/libc/unistd_h.c:80.
+ Called from tests/libc/unistd_h.c:84.
[eva] Done for function chown
[eva] computing for function chown <- main.
- Called from tests/libc/unistd_h.c:80.
+ Called from tests/libc/unistd_h.c:84.
[eva] Done for function chown
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 39a11b77b4e..78e0c0de0e6 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -5,15 +5,18 @@
\return(dup) == -1 (auto)
\return(getcwd) == 0 (auto)
\return(gethostname) == 0 (auto)
+ \return(getpgrp) == 0 (auto)
\return(isatty) == 0 (auto)
\return(setegid) == 0 (auto)
\return(seteuid) == 0 (auto)
\return(setgid) == 0 (auto)
+ \return(setpgid) == 0 (auto)
\return(setregid) == 0 (auto)
\return(setreuid) == 0 (auto)
\return(setsid) == 0 (auto)
\return(setuid) == 0 (auto)
\return(ttyname) == 0 (auto)
+ \return(unlink) == 0 (auto)
\return(usleep) == 0 (auto)
\return(getresuid) == 0 (auto)
\return(setresuid) == 0 (auto)
@@ -471,35 +474,62 @@
[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.
+[eva] computing for function getpgid <- main.
+ Called from tests/libc/unistd_h.c:75.
+[eva] using specification for function getpgid
+[eva] Done for function getpgid
+[eva] computing for function getpgid <- main.
+ Called from tests/libc/unistd_h.c:75.
+[eva] Done for function getpgid
+[eva] computing for function setpgid <- main.
+ Called from tests/libc/unistd_h.c:75.
+[eva] using specification for function setpgid
+[eva] Done for function setpgid
+[eva] computing for function setpgid <- main.
+ Called from tests/libc/unistd_h.c:75.
+[eva] Done for function setpgid
+[eva] computing for function getpgrp <- main.
+ Called from tests/libc/unistd_h.c:76.
+[eva] using specification for function getpgrp
+[eva] Done for function getpgrp
+[eva] computing for function getpgrp <- main.
Called from tests/libc/unistd_h.c:76.
+[eva] Done for function getpgrp
+[eva] computing for function unlink <- main.
+ Called from tests/libc/unistd_h.c:78.
+[eva] using specification for function unlink
+[eva] tests/libc/unistd_h.c:78:
+ function unlink: precondition 'valid_string_path' got status valid.
+[eva] Done for function unlink
+[eva] computing for function isatty <- main.
+ Called from tests/libc/unistd_h.c:80.
[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.
+ Called from tests/libc/unistd_h.c:80.
[eva] Done for function isatty
-[eva] tests/libc/unistd_h.c:77: assertion got status valid.
+[eva] tests/libc/unistd_h.c:81: assertion got status valid.
[eva] computing for function ttyname <- main.
- Called from tests/libc/unistd_h.c:78.
+ Called from tests/libc/unistd_h.c:82.
[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.
+ Called from tests/libc/unistd_h.c:82.
[eva] Done for function ttyname
[eva] computing for function chown <- main.
- Called from tests/libc/unistd_h.c:80.
+ Called from tests/libc/unistd_h.c:84.
[eva] using specification for function chown
-[eva] tests/libc/unistd_h.c:80:
+[eva] tests/libc/unistd_h.c:84:
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.
+ Called from tests/libc/unistd_h.c:84.
[eva] Done for function chown
[eva] computing for function chown <- main.
- Called from tests/libc/unistd_h.c:80.
+ Called from tests/libc/unistd_h.c:84.
[eva] Done for function chown
[eva] computing for function chown <- main.
- Called from tests/libc/unistd_h.c:80.
+ Called from tests/libc/unistd_h.c:84.
[eva] Done for function chown
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/libc/signal_h.c b/tests/libc/signal_h.c
index 289f4c365e8..f8aa063de2e 100644
--- a/tests/libc/signal_h.c
+++ b/tests/libc/signal_h.c
@@ -41,5 +41,16 @@ int main() {
int kill_res = kill(42, SIGTERM);
+ struct sigaction sa1, sa2;
+ if (sigaction(SIGCHLD, 0, &sa1)) {
+ return -1;
+ }
+ if (sigaction(SIGCONT, &sa1, &sa2)) {
+ return -1;
+ }
+ if (sigaction(SIGUSR1, &sa2, 0)) {
+ return -1;
+ }
+
return 0;
}
diff --git a/tests/libc/stdlib_h.c b/tests/libc/stdlib_h.c
index 160cf1d2bfc..dec6260f59f 100644
--- a/tests/libc/stdlib_h.c
+++ b/tests/libc/stdlib_h.c
@@ -77,5 +77,9 @@ int main() {
char *v = getenv("MUTABLE");
if (v[8] != 'n') return 1; // possible only if imprecise
}*/
+
+ char tempFilename[] = "blaXXXXXX";
+ int r = mkstemp(tempFilename);
+
return 0;
}
diff --git a/tests/libc/string_h.c b/tests/libc/string_h.c
index 9dd3b05c2b9..27065864dd5 100644
--- a/tests/libc/string_h.c
+++ b/tests/libc/string_h.c
@@ -118,11 +118,12 @@ 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);
+ char *strsig = strsignal(1);
+ //@ assert valid_read_string(strsig);
return 0;
}
diff --git a/tests/libc/unistd_h.c b/tests/libc/unistd_h.c
index d665ec88fa9..b6eba6c732c 100644
--- a/tests/libc/unistd_h.c
+++ b/tests/libc/unistd_h.c
@@ -72,6 +72,10 @@ int main() {
r = setuid(ruid);
r = setregid(rgid, egid);
r = setreuid(ruid, euid);
+ r = setpgid(p, getpgid(0));
+ r = getpgrp();
+
+ r = unlink("/tmp/test_unlink");
r = isatty(1);
//@ assert r == 0 || r == 1;
--
GitLab