From 69895c90773d353a9a3b01ff8ede1826b399e658 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 25 Feb 2019 10:02:43 +0100
Subject: [PATCH] [Libc] remove obsoleted ifdefs
---
share/libc/math.h | 28 +--
share/libc/signal.h | 2 -
share/libc/stddef.h | 2 -
share/libc/string.h | 6 -
share/libc/unistd.h | 2 -
.../report/tests/report/oracle/csv.csv | 2 +-
tests/builtins/oracle/memcpy.res.oracle | 168 +++++++------
tests/idct/oracle/ieee_1180_1990.res.oracle | 233 +++++++++---------
tests/libc/oracle/coverage.res.oracle | 2 +-
tests/libc/oracle/fc_libc.0.res.oracle | 40 +--
tests/libc/oracle/fc_libc.1.res.oracle | 27 ++
tests/libc/oracle/netdb_c.res.oracle | 4 +-
tests/libc/oracle/signal_h.res.oracle | 2 +-
tests/libc/oracle/stdlib_c_env.res.oracle | 2 +-
tests/libc/oracle/string_c.res.oracle | 26 +-
tests/libc/oracle/string_c_generic.res.oracle | 22 +-
tests/misc/oracle/pragma-pack.0.res.oracle | 2 +
17 files changed, 307 insertions(+), 263 deletions(-)
diff --git a/share/libc/math.h b/share/libc/math.h
index a7a0ef9dbf6..f8d414b78b5 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 d39758a71cc..458175c0aef 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 */
diff --git a/share/libc/stddef.h b/share/libc/stddef.h
index e32d8548e86..38c32691d7e 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/string.h b/share/libc/string.h
index 1721e2dde50..c8f5b3d8ec3 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);
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index a966cf7cbf7..3e790d21269 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -1109,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'
@@ -1159,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 27957ca3cfa..18a0e92bcf7 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/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index c767cf17fb5..649c1f67a8f 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -1385,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'
--------------------------------------------------------------------------------
@@ -1397,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.
@@ -1409,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.
@@ -1444,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 297)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 299)
+[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 307)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 309)
+[ 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.
@@ -1456,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)
+[ 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 299)
- 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.
@@ -1481,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.
@@ -1502,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.
@@ -1515,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.
@@ -1536,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.
@@ -1557,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.
@@ -1578,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.
@@ -1597,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.
@@ -1628,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.
@@ -1641,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.
@@ -1660,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.
@@ -1680,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.
@@ -1695,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.
@@ -1715,7 +1745,7 @@
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.
@@ -1732,7 +1762,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 514)
+[ Extern ] Froms (file share/libc/string.h, line 508)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -2185,9 +2215,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 159 Completely validated
- 230 Considered valid
+ 161 Completely validated
+ 238 Considered valid
29 To be validated
4 Alarms emitted
- 422 Total
+ 432 Total
--------------------------------------------------------------------------------
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 2c7e41c81de..288eef68b4c 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 abb4e7886a7..6e7f751bf3c 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 80)
+ 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 461bda59470..15885d81a20 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 (375)
+ 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);
@@ -135,24 +135,24 @@
siglongjmp (0 call); signal (0 call); sigprocmask (0 call); sin (0 call);
sinf (0 call); sinl (0 call); socket (0 call); socketpair (0 call);
sqrt (0 call); sqrtf (0 call); sqrtl (0 call); srand (0 call);
- srand48 (0 call); srandom (0 call); stat (0 call); strcoll (0 call);
- strcspn (0 call); strftime (0 call); strlcat (0 call); strlcpy (0 call);
- strncasecmp (0 call); strpbrk (0 call); strsep (0 call); strsignal (0 call);
- strspn (0 call); strtod (0 call); strtof (0 call); strtoimax (0 call);
- strtok (0 call); strtok_r (0 call); strtol (0 call); strtold (0 call);
- strtoll (0 call); strtoul (0 call); strtoull (0 call); strxfrm (0 call);
- sync (0 call); sysconf (0 call); syslog (0 call); system (0 call);
- tcgetattr (0 call); tcsetattr (0 call); time (0 call); times (0 call);
- tmpfile (0 call); tmpnam (0 call); trunc (0 call); truncf (0 call);
- truncl (0 call); ttyname (0 call); tzset (0 call); umask (0 call);
- ungetc (0 call); unlink (0 call); usleep (0 call); utimes (0 call);
- vfprintf (0 call); vfscanf (0 call); vprintf (0 call); vscanf (0 call);
- vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call); wait (0 call);
- waitpid (0 call); wcschr (0 call); wcscmp (0 call); wcscspn (0 call);
- wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call);
- wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call); wcstombs (0 call);
- wctomb (0 call); wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call);
- write (0 call);
+ 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); 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 (20)
==============================
@@ -176,7 +176,7 @@
Goto = 84
Assignment = 415
Exit point = 76
- Function = 451
+ 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 88c0df5a8f9..aecfd20abf2 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3391,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,
@@ -3556,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);
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index fcd756cf744..419fd8ae3f5 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -23,12 +23,14 @@
\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)
@@ -245,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 f09d621e64d..42c80f2642d 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -124,7 +124,7 @@
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] tests/libc/signal_h.c:48:
function sigaction: precondition 'separation,separated_acts' got status valid.
-[eva] share/libc/signal.h:214:
+[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.
diff --git a/tests/libc/oracle/stdlib_c_env.res.oracle b/tests/libc/oracle/stdlib_c_env.res.oracle
index bb422440f6d..5322b2985d4 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/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index 7dc1cf2aedc..d4cb7a56f16 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 3431164e2af..79cc74ecd4c 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/misc/oracle/pragma-pack.0.res.oracle b/tests/misc/oracle/pragma-pack.0.res.oracle
index a129933710f..4ca3caef6f2 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
--
GitLab