diff --git a/share/libc/math.h b/share/libc/math.h
index a7a0ef9dbf6040e15ff30925742c05f9d1678ed0..f8d414b78b556b749ff9e4c74e78479764c2ab06 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -42,21 +42,19 @@ typedef double double_t;
#define HUGE_VALL 0x1.0p32767L
/* The constants below are not part of C99/C11 but they are defined in POSIX */
-#ifdef _XOPEN_SOURCE
-# define M_E 0x1.5bf0a8b145769p1 /* e */
-# define M_LOG2E 0x1.71547652b82fep0 /* log_2 e */
-# define M_LOG10E 0x1.bcb7b1526e50ep-2 /* log_10 e */
-# define M_LN2 0x1.62e42fefa39efp-1 /* log_e 2 */
-# define M_LN10 0x1.26bb1bbb55516p1 /* log_e 10 */
-# define M_PI 0x1.921fb54442d18p1 /* pi */
-# define M_PI_2 0x1.921fb54442d18p0 /* pi/2 */
-# define M_PI_4 0x1.921fb54442d18p-1 /* pi/4 */
-# define M_1_PI 0x1.45f306dc9c883p-2 /* 1/pi */
-# define M_2_PI 0x1.45f306dc9c883p-1 /* 2/pi */
-# define M_2_SQRTPI 0x1.20dd750429b6dp0 /* 2/sqrt(pi) */
-# define M_SQRT2 0x1.6a09e667f3bcdp0 /* sqrt(2) */
-# define M_SQRT1_2 0x1.6a09e667f3bcdp-1 /* 1/sqrt(2) */
-#endif
+#define M_E 0x1.5bf0a8b145769p1 /* e */
+#define M_LOG2E 0x1.71547652b82fep0 /* log_2 e */
+#define M_LOG10E 0x1.bcb7b1526e50ep-2 /* log_10 e */
+#define M_LN2 0x1.62e42fefa39efp-1 /* log_e 2 */
+#define M_LN10 0x1.26bb1bbb55516p1 /* log_e 10 */
+#define M_PI 0x1.921fb54442d18p1 /* pi */
+#define M_PI_2 0x1.921fb54442d18p0 /* pi/2 */
+#define M_PI_4 0x1.921fb54442d18p-1 /* pi/4 */
+#define M_1_PI 0x1.45f306dc9c883p-2 /* 1/pi */
+#define M_2_PI 0x1.45f306dc9c883p-1 /* 2/pi */
+#define M_2_SQRTPI 0x1.20dd750429b6dp0 /* 2/sqrt(pi) */
+#define M_SQRT2 0x1.6a09e667f3bcdp0 /* sqrt(2) */
+#define M_SQRT1_2 0x1.6a09e667f3bcdp-1 /* 1/sqrt(2) */
/* The following specifications will set errno. */
#define math_errhandling MATH_ERRNO
diff --git a/share/libc/signal.h b/share/libc/signal.h
index f1eb5d6cc1b20256a72059b97021f8219c07661d..458175c0aef5c02d33692115211af148407e4fac 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -44,9 +44,7 @@ typedef void (*__fc_sighandler_t) (int);
#define sighandler_t __fc_sighandler_t
/* for BSD 4.4 */
-#ifdef __USE_MISC
typedef __fc_sighandler_t sig_t;
-#endif
#define SIG_DFL ((__fc_sighandler_t)0) /* default signal handling */
#define SIG_IGN ((__fc_sighandler_t)1) /* ignore signal */
@@ -96,7 +94,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 +197,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 +241,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/stddef.h b/share/libc/stddef.h
index e32d8548e869d1d2bee02714348b5b151cf7d2c1..38c32691d7e9bc2340a191773cef99b6f3f526c6 100644
--- a/share/libc/stddef.h
+++ b/share/libc/stddef.h
@@ -32,9 +32,7 @@ typedef __PTRDIFF_T ptrdiff_t;
#endif
__END_DECLS
#include "__fc_define_size_t.h"
-#ifdef __GNU_C__
#include "__fc_define_ssize_t.h"
-#endif
#include "__fc_define_wchar_t.h"
#include "__fc_define_null.h"
#define offsetof(type, member) __builtin_offsetof(type,member)
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index e69ed2aa5b7dd00a0a704e72dc6e398b8036dfe2..98a172ccdb0cdc17eab4112275724b0984f870b1 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 b9e46ee597ed4f3a042c3289e0490e1fbdea9331..c8f5b3d8ec308565caed422e7debcb744c61c755 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -222,7 +222,6 @@ extern char *strpbrk(const char *s, const char *accept);
@*/
extern char *strstr(const char *haystack, const char *needle);
-#ifdef __USE_GNU
/*@ requires valid_string_haystack: valid_read_string(haystack);
@ requires valid_string_needle: valid_read_string(needle);
@ assigns \result \from haystack, indirect:haystack[0..],
@@ -232,7 +231,6 @@ extern char *strstr(const char *haystack, const char *needle);
@ || (\subset(\result, haystack+(0..)) && \valid_read(\result));
@*/
extern char *strcasestr (const char *haystack, const char *needle);
-#endif
// internal state of strtok
char *__fc_strtok_ptr;
@@ -387,8 +385,6 @@ extern char *strncpy(char *restrict dest,
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
/*@ requires valid_string_src: valid_read_string(src);
@ requires room_string: \valid(dest+(0..strlen(src)));
@ requires separation:
@@ -399,8 +395,6 @@ size_t strlcpy(char * restrict dest, const char * restrict src, size_t n);
@ ensures points_to_end: \result == dest + strlen(dest);
@*/
extern char *stpcpy(char *restrict dest, const char *restrict src);
-# endif
-#endif
/*@ // missing: separation
@ requires valid_string_src: valid_read_string(src);
@@ -502,15 +496,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 d3e906a43b37b56b5c7ec700f3017b254d122a95..3e790d2126994b6800877bfbed1493e67e19ebae 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);
/*@
@@ -1093,7 +1109,6 @@ extern ssize_t write(int fd, const void *buf, size_t count);
extern int setgroups(size_t size, const gid_t *list);
// The following functions are GNU extensions
-#ifdef _GNU_SOURCE
/*@
// missing: assigns \result, *ruid, *euid, *suid \from 'process'
@@ -1143,7 +1158,6 @@ int getresgid(gid_t *rgid, gid_t *egid, gid_t *sgid);
*/
int setresgid(gid_t rgid, gid_t egid, gid_t sgid);
-#endif
__END_DECLS
diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index 27957ca3cfac5d1699e63571fe34539b7c224d83..18a0e92bcf745d267e58b4a630a8962646e626ed 100644
--- a/src/plugins/report/tests/report/oracle/csv.csv
+++ b/src/plugins/report/tests/report/oracle/csv.csv
@@ -1,5 +1,5 @@
directory file line function property kind status property
-FRAMAC_SHARE/libc math.h 528 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc math.h 526 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
tests/report csv.c 11 main1 signed_overflow Unknown -2147483648 ≤ x * x
tests/report csv.c 11 main1 signed_overflow Unknown x * x ≤ 2147483647
tests/report csv.c 12 main1 index_bound Unknown 0 ≤ x
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index 14a7a8fc9c75c9e6d16d8fc506eedc6a96ac5c51..d77f1466122eaff29333291e8a76e978c2c2fbab 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 34325075722573f2b05936a38e2822674bfdb142..649c1f67a8f6a0006d1ee7a14c2927b14c3e86d6 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}
@@ -1383,6 +1385,19 @@
[ Valid ] Default behavior
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function 'strcasestr'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'result_null_or_in_haystack'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 227)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'strtok'
--------------------------------------------------------------------------------
@@ -1395,11 +1410,13 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'resume_str' 'ptr_subset'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 242)
+[ Extern ] Assigns (file share/libc/string.h, line 240)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 255)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 257)
+[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 263)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 265)
+[ Extern ] Froms (file share/libc/string.h, line 240)
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 242)
Unverifiable but considered Valid.
@@ -1407,19 +1424,17 @@
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 246)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 248)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 255)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 257)
- Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 258)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 256)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 259)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 257)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 265)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 263)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 268)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 266)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 271)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 269)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1442,11 +1457,13 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'resume_str' 'saveptr_subset'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 284)
+[ Extern ] Assigns (file share/libc/string.h, line 282)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 299)
+[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 297)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 309)
+[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 307)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 282)
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 284)
Unverifiable but considered Valid.
@@ -1454,19 +1471,17 @@
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 288)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 290)
- Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 299)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 297)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 300)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 298)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 301)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 299)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 309)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 307)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 312)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 310)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 315)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 313)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1479,11 +1494,11 @@
--- Properties of Function 'strsep'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/string.h, line 327)
+[ Extern ] Assigns (file share/libc/string.h, line 325)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 327)
+[ Extern ] Froms (file share/libc/string.h, line 325)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 328)
+[ Extern ] Froms (file share/libc/string.h, line 326)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1500,7 +1515,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 338)
+[ Extern ] Froms (file share/libc/string.h, line 336)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1513,11 +1528,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'result_ptr'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 351)
+[ Extern ] Assigns (file share/libc/string.h, line 349)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 351)
+[ Extern ] Froms (file share/libc/string.h, line 349)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 352)
+[ Extern ] Froms (file share/libc/string.h, line 350)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1534,11 +1549,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'partial' 'equal_prefix'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 363)
+[ Extern ] Assigns (file share/libc/string.h, line 361)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 363)
+[ Extern ] Froms (file share/libc/string.h, line 361)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 364)
+[ Extern ] Froms (file share/libc/string.h, line 362)
Unverifiable but considered Valid.
[ Valid ] Behavior 'complete'
by Frama-C kernel.
@@ -1555,11 +1570,28 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'bounded_result'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 382)
+[ Extern ] Assigns (file share/libc/string.h, line 380)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 380)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 381)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'stpcpy'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'equal_contents'
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition 'points_to_end'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/string.h, line 392)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 382)
+[ Extern ] Froms (file share/libc/string.h, line 392)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 383)
+[ Extern ] Froms (file share/libc/string.h, line 393)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1576,11 +1608,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'result_ptr'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 409)
+[ Extern ] Assigns (file share/libc/string.h, line 403)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 409)
+[ Extern ] Froms (file share/libc/string.h, line 403)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 412)
+[ Extern ] Froms (file share/libc/string.h, line 406)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1595,23 +1627,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 429)
+[ Extern ] Assigns for 'complete' (file share/libc/string.h, line 423)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 423)
+[ Extern ] Assigns (file share/libc/string.h, line 417)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 437)
+[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 431)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'complete' (file share/libc/string.h, line 429)
+[ Extern ] Froms for 'complete' (file share/libc/string.h, line 423)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'complete' (file share/libc/string.h, line 431)
+[ Extern ] Froms for 'complete' (file share/libc/string.h, line 425)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 423)
+[ Extern ] Froms (file share/libc/string.h, line 417)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 424)
+[ Extern ] Froms (file share/libc/string.h, line 418)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'partial' (file share/libc/string.h, line 437)
+[ Extern ] Froms for 'partial' (file share/libc/string.h, line 431)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'partial' (file share/libc/string.h, line 439)
+[ Extern ] Froms for 'partial' (file share/libc/string.h, line 433)
Unverifiable but considered Valid.
[ Valid ] Behavior 'complete'
by Frama-C kernel.
@@ -1626,11 +1658,11 @@
[ Extern ] Post-condition 'bounded_result'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 449)
+[ Extern ] Assigns (file share/libc/string.h, line 443)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 449)
+[ Extern ] Froms (file share/libc/string.h, line 443)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 450)
+[ Extern ] Froms (file share/libc/string.h, line 444)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1639,11 +1671,11 @@
--- Properties of Function 'strxfrm'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/string.h, line 458)
+[ Extern ] Assigns (file share/libc/string.h, line 452)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 458)
+[ Extern ] Froms (file share/libc/string.h, line 452)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 459)
+[ Extern ] Froms (file share/libc/string.h, line 453)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1658,19 +1690,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 470)
+[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 464)
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 470)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 464)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 471)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 465)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 467)
+[ Extern ] Froms (file share/libc/string.h, line 461)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 477)
+[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 471)
Unverifiable but considered Valid.
[ Valid ] Behavior 'allocation'
by Frama-C kernel.
@@ -1678,7 +1710,7 @@
by Frama-C kernel.
[ Valid ] Behavior 'no_allocation'
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 466)
+[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 460)
Unverifiable but considered Valid.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid.
@@ -1693,19 +1725,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 488)
+[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 482)
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 488)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 482)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 489)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 483)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 484)
+[ Extern ] Froms (file share/libc/string.h, line 478)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 498)
+[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 492)
Unverifiable but considered Valid.
[ Valid ] Behavior 'allocation'
by Frama-C kernel.
@@ -1713,11 +1745,28 @@
by Frama-C kernel.
[ Valid ] Behavior 'no_allocation'
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 483)
+[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 477)
Unverifiable but considered Valid.
[ 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 508)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'bzero'
--------------------------------------------------------------------------------
@@ -2166,9 +2215,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 158 Completely validated
- 225 Considered valid
+ 161 Completely validated
+ 238 Considered valid
29 To be validated
4 Alarms emitted
- 416 Total
+ 432 Total
--------------------------------------------------------------------------------
diff --git a/tests/builtins/oracle/memcpy2.res.oracle b/tests/builtins/oracle/memcpy2.res.oracle
index bd415ec9eac9b34f5ed22f65f780b388f791b4a6..912286440a4435cca2a1146eb60e1d541b313ffe 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 9cacd457242f401eae1bff00691a9f9965a1881f..097bcf8ac85f81bbc49e03b7b0a16135a388faf8 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 3548706927775625b2fda28b07dd323884377a37..8b39ca3d183021f676f5240a91aaf3c582e4e66e 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/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 2c7e41c81de51023519cf04af34b7d44f3d10625..288eef68b4c6d877a34f1fdbcfbdd25a17146633 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1,7 +1,4 @@
[kernel] Parsing tests/idct/ieee_1180_1990.c (with preprocessing)
-[kernel:parser:decimal-float] tests/idct/ieee_1180_1990.c:101: Warning:
- Floating-point constant 3.14159265358979323846 is not represented exactly. Will use 0x1.921fb54442d18p1.
- (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[kernel] Parsing tests/idct/idct.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -2142,7 +2139,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 73)
+[ Extern ] Froms (file share/libc/math.h, line 71)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2186,7 +2183,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 97)
+[ Extern ] Froms (file share/libc/math.h, line 95)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2218,28 +2215,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 134)
+[ Extern ] Assigns (file share/libc/math.h, line 132)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 141)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 139)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 134)
+[ Extern ] Froms (file share/libc/math.h, line 132)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 134)
+[ Extern ] Froms (file share/libc/math.h, line 132)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 141)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 139)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 141)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 139)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 137)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 135)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2262,28 +2259,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 148)
+[ Extern ] Assigns (file share/libc/math.h, line 146)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 155)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 153)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 148)
+[ Extern ] Froms (file share/libc/math.h, line 146)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 148)
+[ Extern ] Froms (file share/libc/math.h, line 146)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 155)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 153)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 155)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 153)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 151)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 149)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2306,28 +2303,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 162)
+[ Extern ] Assigns (file share/libc/math.h, line 160)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 169)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 167)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 162)
+[ Extern ] Froms (file share/libc/math.h, line 160)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 162)
+[ Extern ] Froms (file share/libc/math.h, line 160)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 169)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 167)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 169)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 167)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 165)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 163)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2350,28 +2347,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 176)
+[ Extern ] Assigns (file share/libc/math.h, line 174)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 183)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 181)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 176)
+[ Extern ] Froms (file share/libc/math.h, line 174)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 176)
+[ Extern ] Froms (file share/libc/math.h, line 174)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 183)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 181)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 183)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 181)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 179)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 177)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2394,28 +2391,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 190)
+[ Extern ] Assigns (file share/libc/math.h, line 188)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 197)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 195)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 190)
+[ Extern ] Froms (file share/libc/math.h, line 188)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 190)
+[ Extern ] Froms (file share/libc/math.h, line 188)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 197)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 195)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 197)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 195)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 193)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 191)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2438,28 +2435,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 204)
+[ Extern ] Assigns (file share/libc/math.h, line 202)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 211)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 209)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 204)
+[ Extern ] Froms (file share/libc/math.h, line 202)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 204)
+[ Extern ] Froms (file share/libc/math.h, line 202)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 211)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 209)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 211)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 209)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 207)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 205)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2485,7 +2482,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 218)
+[ Extern ] Froms (file share/libc/math.h, line 216)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2505,7 +2502,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 225)
+[ Extern ] Froms (file share/libc/math.h, line 223)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2525,7 +2522,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 232)
+[ Extern ] Froms (file share/libc/math.h, line 230)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2542,7 +2539,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 240)
+[ Extern ] Froms (file share/libc/math.h, line 238)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2559,7 +2556,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 247)
+[ Extern ] Froms (file share/libc/math.h, line 245)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2582,7 +2579,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 255)
+[ Extern ] Froms (file share/libc/math.h, line 253)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2602,7 +2599,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 262)
+[ Extern ] Froms (file share/libc/math.h, line 260)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2622,7 +2619,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 269)
+[ Extern ] Froms (file share/libc/math.h, line 267)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2642,7 +2639,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 276)
+[ Extern ] Froms (file share/libc/math.h, line 274)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2662,7 +2659,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 283)
+[ Extern ] Froms (file share/libc/math.h, line 281)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2682,7 +2679,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 290)
+[ Extern ] Froms (file share/libc/math.h, line 288)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2702,10 +2699,10 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 301)
+[ Extern ] Assigns (file share/libc/math.h, line 299)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 312)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 310)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'infinite' nothing
@@ -2714,22 +2711,22 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 301)
+[ Extern ] Froms (file share/libc/math.h, line 299)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 301)
+[ Extern ] Froms (file share/libc/math.h, line 299)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 312)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 310)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 312)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 310)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 308)
+[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 306)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 304)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 302)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2758,10 +2755,10 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 319)
+[ Extern ] Assigns (file share/libc/math.h, line 317)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 330)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 328)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'infinite' nothing
@@ -2770,22 +2767,22 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 319)
+[ Extern ] Froms (file share/libc/math.h, line 317)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 319)
+[ Extern ] Froms (file share/libc/math.h, line 317)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 330)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 328)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 330)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 328)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 326)
+[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 324)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 322)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 320)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2814,10 +2811,10 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 337)
+[ Extern ] Assigns (file share/libc/math.h, line 335)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 348)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 346)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'infinite' nothing
@@ -2826,22 +2823,22 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 337)
+[ Extern ] Froms (file share/libc/math.h, line 335)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 337)
+[ Extern ] Froms (file share/libc/math.h, line 335)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 348)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 346)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 348)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 346)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 344)
+[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 342)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 340)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 338)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2870,7 +2867,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 376)
+[ Extern ] Froms (file share/libc/math.h, line 374)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2890,7 +2887,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 384)
+[ Extern ] Froms (file share/libc/math.h, line 382)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2907,7 +2904,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 414)
+[ Extern ] Froms (file share/libc/math.h, line 412)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2924,7 +2921,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 421)
+[ Extern ] Froms (file share/libc/math.h, line 419)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2941,7 +2938,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 428)
+[ Extern ] Froms (file share/libc/math.h, line 426)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2958,7 +2955,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 435)
+[ Extern ] Froms (file share/libc/math.h, line 433)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2975,7 +2972,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 442)
+[ Extern ] Froms (file share/libc/math.h, line 440)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2992,7 +2989,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 449)
+[ Extern ] Froms (file share/libc/math.h, line 447)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3009,7 +3006,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 460)
+[ Extern ] Froms (file share/libc/math.h, line 458)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3026,7 +3023,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 467)
+[ Extern ] Froms (file share/libc/math.h, line 465)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3043,7 +3040,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 474)
+[ Extern ] Froms (file share/libc/math.h, line 472)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3068,7 +3065,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 500)
+[ Extern ] Froms (file share/libc/math.h, line 498)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3093,7 +3090,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 508)
+[ Extern ] Froms (file share/libc/math.h, line 506)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3118,7 +3115,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 516)
+[ Extern ] Froms (file share/libc/math.h, line 514)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3135,7 +3132,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 529)
+[ Extern ] Froms (file share/libc/math.h, line 527)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3152,7 +3149,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 536)
+[ Extern ] Froms (file share/libc/math.h, line 534)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3178,7 +3175,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 545)
+[ Extern ] Froms (file share/libc/math.h, line 543)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3198,7 +3195,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 553)
+[ Extern ] Froms (file share/libc/math.h, line 551)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3218,7 +3215,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 561)
+[ Extern ] Froms (file share/libc/math.h, line 559)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3235,7 +3232,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 584)
+[ Extern ] Froms (file share/libc/math.h, line 582)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3252,7 +3249,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 590)
+[ Extern ] Froms (file share/libc/math.h, line 588)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3269,7 +3266,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 597)
+[ Extern ] Froms (file share/libc/math.h, line 595)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3286,7 +3283,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 603)
+[ Extern ] Froms (file share/libc/math.h, line 601)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3303,7 +3300,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 609)
+[ Extern ] Froms (file share/libc/math.h, line 607)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3320,7 +3317,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 615)
+[ Extern ] Froms (file share/libc/math.h, line 613)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3337,7 +3334,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 637)
+[ Extern ] Froms (file share/libc/math.h, line 635)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3354,7 +3351,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 643)
+[ Extern ] Froms (file share/libc/math.h, line 641)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3371,7 +3368,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 649)
+[ Extern ] Froms (file share/libc/math.h, line 647)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3388,7 +3385,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 663)
+[ Extern ] Froms (file share/libc/math.h, line 661)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3405,7 +3402,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 669)
+[ Extern ] Froms (file share/libc/math.h, line 667)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3422,7 +3419,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 675)
+[ Extern ] Froms (file share/libc/math.h, line 673)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3439,7 +3436,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 682)
+[ Extern ] Froms (file share/libc/math.h, line 680)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3456,7 +3453,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 689)
+[ Extern ] Froms (file share/libc/math.h, line 687)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3473,7 +3470,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 710)
+[ Extern ] Froms (file share/libc/math.h, line 708)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3490,7 +3487,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 717)
+[ Extern ] Froms (file share/libc/math.h, line 715)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3507,7 +3504,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 724)
+[ Extern ] Froms (file share/libc/math.h, line 722)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index 81b8f86a27e7a7a613c8d725aaf40e1ee5d8ad51..6e7f751bf3ca6d1d5a1eeefee38a7b5424392b83 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 82)
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 32c4f831a3aca48a4593fe3ed92573a3f2dd412b..15885d81a20c5ef411514cad2ccb94d49ff54c3a 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 (377)
=========================
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);
+ 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); stpcpy (0 call);
+ strcasestr (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); 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);
+ 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 = 453
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 e56f5e98e8c872547a2d14eb5df95aa6a03e182f..aecfd20abf26a67bc0a99da4ee9d7f8dc15b3c52 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__));
*/
@@ -3327,6 +3391,19 @@ extern char *strpbrk(char const *s, char const *accept);
char *strstr(char const *haystack, char const *needle);
+/*@ requires valid_string_haystack: valid_read_string(haystack);
+ requires valid_string_needle: valid_read_string(needle);
+ ensures
+ result_null_or_in_haystack:
+ \result ≡ \null ∨
+ (\subset(\result, \old(haystack) + (0 ..)) ∧ \valid_read(\result));
+ assigns \result;
+ assigns \result
+ \from haystack, (indirect: *(haystack + (0 ..))),
+ (indirect: *(needle + (0 ..)));
+ */
+extern char *strcasestr(char const *haystack, char const *needle);
+
char *__fc_strtok_ptr;
/*@ requires valid_string_delim: valid_read_string(delim);
assigns *(s + (0 ..)), *(__fc_strtok_ptr + (0 ..)), \result,
@@ -3492,6 +3569,20 @@ char *strncpy(char *dest, char const *src, size_t n);
*/
size_t strlcpy(char * __restrict dest, char const * __restrict src, size_t n);
+/*@ requires valid_string_src: valid_read_string(src);
+ requires room_string: \valid(dest + (0 .. strlen(src)));
+ requires
+ separation:
+ \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
+ ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
+ ensures points_to_end: \result ≡ \old(dest) + strlen(\old(dest));
+ assigns *(dest + (0 .. strlen{Old}(src))), \result;
+ assigns *(dest + (0 .. strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+ */
+extern char *stpcpy(char * __restrict dest, char const * __restrict src);
+
char *strcat(char *dest, char const *src);
char *strncat(char *dest, char const *src, size_t n);
@@ -3524,6 +3615,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 +7293,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 +7373,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 +7420,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 1ceb0a03241f85b3da6db15f8f7abcaed67fc928..419fd8ae3f596924cb1de2e8e4a64b6ebe139bf0 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -23,16 +23,19 @@
\return(strrchr) == 0 (auto)
\return(strpbrk) == 0 (auto)
\return(strstr) == 0 (auto)
+ \return(strcasestr) == 0 (auto)
\return(strtok) == 0 (auto)
\return(strtok_r) == 0 (auto)
\return(strsep) == 0 (auto)
\return(strerror) == 0 (auto)
\return(strcpy) == 0 (auto)
\return(strncpy) == 0 (auto)
+ \return(stpcpy) == 0 (auto)
\return(strcat) == 0 (auto)
\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)
@@ -244,7 +247,7 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] share/libc/netdb.c:147:
function strncpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:369:
+[eva] share/libc/string.h:367:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva] Done for function strncpy
[eva] Recording results for gethostbyname
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 1d3c95b0de4f684bf6a1b27b5ba5ff5de3e7fc86..42c80f2642d6fdde9b66d2ab9487b73f4ff7b8a8 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:212:
+ 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_c_env.res.oracle b/tests/libc/oracle/stdlib_c_env.res.oracle
index bb422440f6dd0ea084bbe3a495d1c1fcb56e1ded..5322b2985d4f9b618cd28c574c20c7a7be2d59ee 100644
--- a/tests/libc/oracle/stdlib_c_env.res.oracle
+++ b/tests/libc/oracle/stdlib_c_env.res.oracle
@@ -105,7 +105,7 @@
function strcpy: precondition 'room_string' got status valid.
[eva] tests/libc/stdlib_c_env.c:15:
function strcpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:353:
+[eva] share/libc/string.h:351:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva] Done for function strcpy
[eva] computing for function getenv <- main.
diff --git a/tests/libc/oracle/stdlib_h.res.oracle b/tests/libc/oracle/stdlib_h.res.oracle
index c9beadd4b2c9daef94bfab354009fe86ba8b05e0..f5a2bec1be1185a580dea18a6847f0b06bcaa48f 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_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index 7dc1cf2aedc6feefe779fa8f9084dddffb19c524..d4cb7a56f166e0c86f7e6014fb885161748ef0e9 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:411:
+[eva] share/libc/string.h:405:
function strcat: postcondition 'sum_of_lengths' got status valid.
-[eva] share/libc/string.h:414:
+[eva] share/libc/string.h:408:
function strcat: postcondition 'initialization,dest' got status valid.
-[eva] share/libc/string.h:415:
+[eva] share/libc/string.h:409:
function strcat: postcondition 'dest_null_terminated' got status valid.
-[eva] share/libc/string.h:416:
+[eva] share/libc/string.h:410:
function strcat: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcat
[eva] Done for function strcat
@@ -550,11 +550,11 @@
function strcpy: precondition 'room_string' got status valid.
[eva] tests/libc/string_c.c:142:
function strcpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:353:
+[eva] share/libc/string.h:351:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
-[eva:alarm] share/libc/string.h:353: Warning:
+[eva:alarm] share/libc/string.h:351: Warning:
function strcpy: postcondition 'equal_contents' got status unknown.
-[eva] share/libc/string.h:354:
+[eva] share/libc/string.h:352:
function strcpy: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcpy
[eva] Done for function strcpy
@@ -594,13 +594,13 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:154:
function strncpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:365:
+[eva] share/libc/string.h:363:
function strncpy: postcondition 'result_ptr' got status valid.
-[eva] share/libc/string.h:366:
+[eva] share/libc/string.h:364:
function strncpy: postcondition 'initialization' got status valid.
-[eva] share/libc/string.h:369:
+[eva] share/libc/string.h:367:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
-[eva:alarm] share/libc/string.h:369: Warning:
+[eva:alarm] share/libc/string.h:367: Warning:
function strncpy, behavior complete: postcondition 'equal_after_copy' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
@@ -614,9 +614,9 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:157:
function strncpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:372:
+[eva] share/libc/string.h:370:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
-[eva:alarm] share/libc/string.h:372: Warning:
+[eva:alarm] share/libc/string.h:370: Warning:
function strncpy, behavior partial: postcondition 'equal_prefix' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
diff --git a/tests/libc/oracle/string_c_generic.res.oracle b/tests/libc/oracle/string_c_generic.res.oracle
index 3431164e2afbe4604967c749dada73fe8b96d09e..79cc74ecd4c8d7931621e3703168d0584d862705 100644
--- a/tests/libc/oracle/string_c_generic.res.oracle
+++ b/tests/libc/oracle/string_c_generic.res.oracle
@@ -12,11 +12,11 @@
function strcpy: precondition 'room_string' got status valid.
[eva] tests/libc/string_c_generic.c:56:
function strcpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:353:
+[eva] share/libc/string.h:351:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
-[eva:alarm] share/libc/string.h:353: Warning:
+[eva:alarm] share/libc/string.h:351: Warning:
function strcpy: postcondition 'equal_contents' got status unknown.
-[eva] share/libc/string.h:354:
+[eva] share/libc/string.h:352:
function strcpy: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcpy
[eva] Done for function strcpy
@@ -161,13 +161,13 @@
[eva] tests/libc/string_c_generic.c:73:
function strncpy: precondition 'separation' got status valid.
[eva] share/libc/string.c:212: starting to merge loop iterations
-[eva] share/libc/string.h:365:
+[eva] share/libc/string.h:363:
function strncpy: postcondition 'result_ptr' got status valid.
-[eva] share/libc/string.h:366:
+[eva] share/libc/string.h:364:
function strncpy: postcondition 'initialization' got status valid.
-[eva] share/libc/string.h:369:
+[eva] share/libc/string.h:367:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
-[eva:alarm] share/libc/string.h:369: Warning:
+[eva:alarm] share/libc/string.h:367: Warning:
function strncpy, behavior complete: postcondition 'equal_after_copy' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
@@ -199,9 +199,9 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c_generic.c:78:
function strncpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:372:
+[eva] share/libc/string.h:370:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
-[eva:alarm] share/libc/string.h:372: Warning:
+[eva:alarm] share/libc/string.h:370: Warning:
function strncpy, behavior partial: postcondition 'equal_prefix' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
@@ -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:425:
+[eva] share/libc/string.h:419:
function strncat: postcondition 'result_ptr' got status valid.
-[eva] share/libc/string.h:440:
+[eva] share/libc/string.h:434:
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 dd500d0409a4378d30868ee18d352a65de94c277..913d0fe0a7cdfcf9445e1512f68a3a9491fc5e65 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 8acd40bd2d4580f5b0bed8763e743d007b0da385..78a30b4a80af8682c477b5bdbdb42c3aababec9f 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 39a11b77b4e4ae5530789d3936f5737a6b77bc10..78e0c0de0e69dd98b7adb4fbd0f5bcf9f8f82c0e 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 289f4c365e8762970c7e63c37b05b06c086af7ea..f8aa063de2edf99c21e12b0d14a974e35ab24b0c 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 160cf1d2bfcd044f3ddeb01b308df1055b86fa67..dec6260f59fd24e6aed419f1af823ab1527d2fd6 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 9dd3b05c2b9d5cce31c68fd7529a0fb11d3a73d1..27065864dd54811732a6107eecaeca8386c9422f 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 d665ec88fa9055339d43cb3ba706867b93bee864..b6eba6c732ceee7e6be079621580bfec33ba7991 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;
diff --git a/tests/misc/oracle/pragma-pack.0.res.oracle b/tests/misc/oracle/pragma-pack.0.res.oracle
index a129933710ffda3e3a258680488c531640c4d6c6..4ca3caef6f2bb369a68f39a45945228800208ff8 100644
--- a/tests/misc/oracle/pragma-pack.0.res.oracle
+++ b/tests/misc/oracle/pragma-pack.0.res.oracle
@@ -8,6 +8,8 @@
[kernel:typing:pragma] Pushing fc_stdlib stddef.h
[kernel:typing:pragma] Pushing fc_stdlib __fc_define_size_t.h
[kernel:typing:pragma] Popping fc_stdlib __fc_define_size_t.h
+[kernel:typing:pragma] Pushing fc_stdlib __fc_define_ssize_t.h
+[kernel:typing:pragma] Popping fc_stdlib __fc_define_ssize_t.h
[kernel:typing:pragma] Pushing fc_stdlib __fc_define_wchar_t.h
[kernel:typing:pragma] Popping fc_stdlib __fc_define_wchar_t.h
[kernel:typing:pragma] Popping fc_stdlib stddef.h