diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 37041b02d29df294ff1fa3b9326be5b9dd58aaec..5666f1680d57649e3a5ddb72244a33cd87628e4f 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -191,6 +191,7 @@ share/libc/__fc_gcc_builtins.h: CEA_LGPL
share/libc/__fc_inet.h: CEA_LGPL
share/libc/__fc_machdep.h: CEA_LGPL
share/libc/__fc_machdep_linux_shared.h: CEA_LGPL
+share/libc/__fc_runtime.c: CEA_LGPL
share/libc/__fc_select.h: CEA_LGPL
share/libc/__fc_string_axiomatic.h: CEA_LGPL
share/libc/alloca.h: CEA_LGPL
@@ -206,7 +207,6 @@ share/libc/dlfcn.h: CEA_LGPL
share/libc/endian.h: CEA_LGPL
share/libc/errno.c: CEA_LGPL
share/libc/errno.h: CEA_LGPL
-share/libc/fc_runtime.c: CEA_LGPL
share/libc/fcntl.h: CEA_LGPL
share/libc/features.h: CEA_LGPL
share/libc/fenv.h: CEA_LGPL
@@ -247,6 +247,7 @@ share/libc/resolv.h: CEA_LGPL
share/libc/sched.h: CEA_LGPL
share/libc/semaphore.h: CEA_LGPL
share/libc/setjmp.h: CEA_LGPL
+share/libc/signal.c: CEA_LGPL
share/libc/signal.h: CEA_LGPL
share/libc/stdarg.h: CEA_LGPL
share/libc/stdbool.h: CEA_LGPL
diff --git a/share/libc/__fc_builtin.c b/share/libc/__fc_builtin.c
index 0c099981f983a5d8ac718694a3f3427aa99120a8..3ec9d9c8206b56a5809bd626cbad6951c4d59b7e 100644
--- a/share/libc/__fc_builtin.c
+++ b/share/libc/__fc_builtin.c
@@ -31,7 +31,16 @@ __PUSH_FC_STDLIB
int volatile Frama_C_entropy_source;
//@ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
-extern void Frama_C_update_entropy(void);
+void Frama_C_update_entropy(void) {
+ Frama_C_entropy_source = Frama_C_entropy_source;
+}
+
+void Frama_C_make_unknown(char *p, size_t l) {
+ Frama_C_update_entropy();
+ for (size_t i = 0; i < l; i++) {
+ p[i] = Frama_C_entropy_source;
+ }
+}
int Frama_C_nondet(int a, int b)
{
@@ -57,6 +66,19 @@ int Frama_C_interval(int min, int max)
return r;
}
+char Frama_C_char_interval(char min, char max)
+{
+ int r;
+ char aux;
+ Frama_C_update_entropy();
+ aux = Frama_C_entropy_source;
+ if ((aux>=min) && (aux <=max))
+ r = aux;
+ else
+ r = min;
+ return r;
+}
+
float Frama_C_float_interval(float min, float max)
{
Frama_C_update_entropy();
@@ -69,4 +91,12 @@ double Frama_C_double_interval(double min, double max)
return Frama_C_entropy_source ? min : max;
}
+extern void __builtin_abort(void) __attribute__((noreturn)); // GCC builtin
+
+void Frama_C_abort(void)
+{
+ __builtin_abort();
+}
+
+
__POP_FC_STDLIB
diff --git a/share/libc/__fc_define_fd_set_t.h b/share/libc/__fc_define_fd_set_t.h
index 993cba5b5176794c71b1b3c62febc5879a323fc9..6839f5bd47db9a767b8336f00e7ff7b2760b0099 100644
--- a/share/libc/__fc_define_fd_set_t.h
+++ b/share/libc/__fc_define_fd_set_t.h
@@ -27,7 +27,7 @@ __PUSH_FC_STDLIB
#define FD_SETSIZE 1024
#define NFDBITS (8 * sizeof(long))
__BEGIN_DECLS
-typedef struct { long __fc_fd_set[FD_SETSIZE / NFDBITS]; } fd_set;
+typedef struct __fc_fd_set { long __fc_fd_set[FD_SETSIZE / NFDBITS]; } fd_set;
/*@
requires valid_fdset: \valid(fdset);
diff --git a/share/libc/__fc_define_pthread_types.h b/share/libc/__fc_define_pthread_types.h
index bd9a591bc55c194098716a5e5df96e8762982a6d..4ce2bdee976a30eef04adc4e0142b8b7f014f57d 100644
--- a/share/libc/__fc_define_pthread_types.h
+++ b/share/libc/__fc_define_pthread_types.h
@@ -29,22 +29,22 @@ __BEGIN_DECLS
// stronger typing constraints
#ifndef __have_pthread_attr_t
-typedef struct { int _fc; } pthread_attr_t;
+typedef struct __fc_pthread_attr_t { int _fc; } pthread_attr_t;
#define __have_pthread_attr_t
#endif
-typedef struct { int _fc; } pthread_barrier_t;
-typedef struct { int _fc; } pthread_barrierattr_t;
-typedef struct { int _fc; } pthread_cond_t;
-typedef struct { int _fc; } pthread_condattr_t;
-typedef struct { int _fc; } pthread_key_t;
-typedef struct { int _fc; } pthread_mutex_t;
-typedef struct { int _fc; } pthread_mutexattr_t;
-typedef struct { int _fc; } pthread_once_t;
-typedef struct { int _fc; } pthread_rwlock_t;
-typedef struct { int _fc; } pthread_rwlockattr_t;
-typedef struct { int _fc; } pthread_spinlock_t;
-typedef struct { int _fc; } pthread_t;
+typedef struct __fc_pthread_barrier_t { int _fc; } pthread_barrier_t;
+typedef struct __fc_pthread_barrierattr_t { int _fc; } pthread_barrierattr_t;
+typedef struct __fc_pthread_cond_t { int _fc; } pthread_cond_t;
+typedef struct __fc_pthread_condattr_t { int _fc; } pthread_condattr_t;
+typedef struct __fc_pthread_key_t { int _fc; } pthread_key_t;
+typedef struct __fc_pthread_mutex_t { int _fc; } pthread_mutex_t;
+typedef struct __fc_pthread_mutexattr_t { int _fc; } pthread_mutexattr_t;
+typedef struct __fc_pthread_once_t { int _fc; } pthread_once_t;
+typedef struct __fc_pthread_rwlock_t { int _fc; } pthread_rwlock_t;
+typedef struct __fc_pthread_rwlockattr_t { int _fc; } pthread_rwlockattr_t;
+typedef struct __fc_pthread_spinlock_t { int _fc; } pthread_spinlock_t;
+typedef struct __fc_pthread_t { int _fc; } pthread_t;
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/__fc_inet.h b/share/libc/__fc_inet.h
index 07fe52fccc6a481e7c45fb47d0beec7133313464..5c94db3ffab24a54dd434cacf7cc2f63a6977397 100644
--- a/share/libc/__fc_inet.h
+++ b/share/libc/__fc_inet.h
@@ -103,7 +103,7 @@ struct in6_pktinfo
/* Standard well-defined IP protocols. */
-enum
+enum __fc_ipproto
{
IPPROTO_IP = 0, /* Dummy protocol for TCP. */
#define IPPROTO_IP IPPROTO_IP
diff --git a/share/libc/fc_runtime.c b/share/libc/__fc_runtime.c
similarity index 98%
rename from share/libc/fc_runtime.c
rename to share/libc/__fc_runtime.c
index 8890a09a7516cfb88c464a992ea4df1caaa8e2f0..b51db45b40c6342f0691db2e818aceb2489009cf 100644
--- a/share/libc/fc_runtime.c
+++ b/share/libc/__fc_runtime.c
@@ -20,7 +20,7 @@
/* */
/**************************************************************************/
-#include "__fc_builtin.h"
+#include "__fc_builtin.c"
#include "assert.c"
#include "ctype.c"
#include "errno.c"
@@ -31,8 +31,8 @@
#include "locale.c"
#include "math.c"
#include "netdb.c"
+#include "signal.c"
#include "stdio.c"
#include "stdlib.c"
#include "string.c"
#include "wchar.c"
-#include "__fc_builtin.c"
diff --git a/share/libc/assert.c b/share/libc/assert.c
index cfbf8e50d00e44e765d42afb4648582082e65f7f..b25057e0ed7a7384d888975a78a6e669a51fc1e4 100644
--- a/share/libc/assert.c
+++ b/share/libc/assert.c
@@ -29,7 +29,9 @@ extern void Frama_C_show_each_warning();
void __FC_assert(int c,const char* file,int line,const char*expr) {
if (!c) {
+#ifdef __FRAMAC__
Frama_C_show_each_warning("Assertion may fail",file,line,expr);
+#endif
Frama_C_abort ();
}
}
diff --git a/share/libc/fenv.c b/share/libc/fenv.c
index 9f34644e7d4580b57837e26ab3e064ea2895341c..1a4717be7f74c6f4ac2a43a945d7ff66565889f8 100644
--- a/share/libc/fenv.c
+++ b/share/libc/fenv.c
@@ -50,7 +50,7 @@ volatile fenv_t __fc_fenv_state __attribute__((FRAMA_C_MODEL));
*/
int feholdexcept( fenv_t *envp )
{
- *envp = (fenv_t)__fc_fenv_state; /* store the current FPU environment */
+ *envp = __fc_fenv_state; /* store the current FPU environment */
return 0;
}
@@ -63,9 +63,10 @@ int feholdexcept( fenv_t *envp )
* exceptions: If envp contains a raised exception flag and at the same time
* unmasks that exception type, then this will cause an interrupt.
*/
-void fesetenv( const fenv_t *envp )
+int fesetenv( const fenv_t *envp )
{
__fc_fenv_state = *envp;
+ return 0;
}
__POP_FC_STDLIB
diff --git a/share/libc/fenv.h b/share/libc/fenv.h
index 4fb6dacdd2967c3ef7b9fccd6b7f438bf8742c1e..a99347bfc3175c16c01a6dcb0095802cb00c43a7 100644
--- a/share/libc/fenv.h
+++ b/share/libc/fenv.h
@@ -30,7 +30,7 @@ __BEGIN_DECLS
/* Define bits representing the exception. We use the bit positions
of the appropriate bits in the FPU control word. */
-enum
+enum __fc_fe_error
{
FE_INVALID = 0x01,
#define FE_INVALID FE_INVALID
@@ -52,7 +52,7 @@ enum
corresponds to the layout of the block written by the `fstenv'
instruction and has additional fields for the contents of the MXCSR
register as written by the `stmxcsr' instruction. */
-typedef struct
+typedef struct __fc_fenv_t
{
unsigned short int __control_word;
unsigned short int __unused1;
@@ -97,11 +97,11 @@ extern int feholdexcept( fenv_t *envp );
* exceptions: If envp contains a raised exception flag and at the same time
* unmasks that exception type, then this will cause an interrupt.
*/
-extern void fesetenv( const fenv_t *envp );
+extern int fesetenv( const fenv_t *envp );
/** Clears the supported floating-point exceptions represented by argument.
*/
-extern void feclearexcept( int excepts );
+extern int feclearexcept( int excepts );
__END_DECLS
diff --git a/share/libc/glob.c b/share/libc/glob.c
index 05377dfe093fc51e631ca28032e44e21fb8beb80..c3907485b415840a875e63663ffeec2b07d83f4b 100644
--- a/share/libc/glob.c
+++ b/share/libc/glob.c
@@ -20,8 +20,8 @@
/* */
/**************************************************************************/
-#include <glob.h>
-#include <stdlib.h>
+#include "glob.h"
+#include "stdlib.h"
#include "__fc_builtin.h"
__PUSH_FC_STDLIB
@@ -41,7 +41,7 @@ int glob(const char *pattern, int flags,
while (pglob->gl_pathv[reserve_offs+prev_len]) prev_len++;
// path points to pglob->gl_pathv if GLOB_APPEND, or NULL otherwise
- char **path = flags & GLOB_APPEND ? &pglob->gl_pathv : NULL;
+ char **path = flags & GLOB_APPEND ? pglob->gl_pathv : NULL;
if (pglob->gl_pathc == 0) { // no results found
if (flags & GLOB_NOCHECK) {
// allocate 1 slot per reserved offset, + previous length,
@@ -52,7 +52,7 @@ int glob(const char *pattern, int flags,
if (!pglob->gl_pathv) return GLOB_NOSPACE;
// 0-init reserved offsets
for (size_t i = 0; i < reserve_offs; i++) pglob->gl_pathv[i] = 0;
- pglob->gl_pathv[reserve_offs + prev_len] = pattern;
+ pglob->gl_pathv[reserve_offs + prev_len] = (char*)pattern;
pglob->gl_pathv[reserve_offs + prev_len + 1] = 0; // terminator
return 0;
} else {
diff --git a/share/libc/glob.h b/share/libc/glob.h
index cafe8f453c4ac9ccda0b2c42609189c45e3608e6..be325cd6cb2c26b847cdbca598e810e2559cc8d7 100644
--- a/share/libc/glob.h
+++ b/share/libc/glob.h
@@ -43,7 +43,7 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
-typedef struct {
+typedef struct __fc_glob_t {
__SIZE_T gl_pathc; /* Count of paths matched by the pattern. */
char **gl_pathv; /* List of matched pathnames. */
__SIZE_T gl_offs; /* Slots to reserve in `gl_pathv'. */
diff --git a/share/libc/inttypes.c b/share/libc/inttypes.c
index a12156da2f0bed308499fc7e679a49766b99f4f2..f110cfdbcafd80ff94573e8db5cfc69b492ddd95 100644
--- a/share/libc/inttypes.c
+++ b/share/libc/inttypes.c
@@ -33,6 +33,6 @@ imaxdiv_t imaxdiv(intmax_t numer, intmax_t denom){
r.quot=numer/denom;
r.rem=numer%denom;
return r;
-};
+}
__POP_FC_STDLIB
diff --git a/share/libc/inttypes.h b/share/libc/inttypes.h
index 7a5a4f1396bf9c74803a3b48e2883e1166e17d98..be311683106349b8bcc75dbcdcd7067991c1e917 100644
--- a/share/libc/inttypes.h
+++ b/share/libc/inttypes.h
@@ -246,7 +246,7 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
-typedef struct
+typedef struct __fc_imaxdiv_t
{
intmax_t quot; /* Quotient. */
intmax_t rem; /* Remainder. */
diff --git a/share/libc/math.c b/share/libc/math.c
index dbe443de13f2e5d6973e77226aa14c34f80cd18e..95182ad6225ffc651ff1ff6d271c4610aae32405 100644
--- a/share/libc/math.c
+++ b/share/libc/math.c
@@ -44,7 +44,7 @@ float fabsf(float x)
int __finitef(float f)
{
- union { float f ; unsigned short w[2] ; } u ;
+ union __fc_u_finitef { float f ; unsigned short w[2] ; } u ;
unsigned short usExp ;
u.f = f ; /* Initilize for word access */
@@ -57,7 +57,7 @@ int __finitef(float f)
int __finite(double d)
{
- union { double d ; unsigned short w[4] ; } u ;
+ union __fc_u_finite { double d ; unsigned short w[4] ; } u ;
unsigned short usExp ;
u.d = d ; /* Initilize for word access */
diff --git a/share/libc/math.h b/share/libc/math.h
index f8d414b78b556b749ff9e4c74e78479764c2ab06..ff121459534bd3d364ed3040fdf1fd591e60cf11 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -65,7 +65,7 @@ typedef double double_t;
#define FP_SUBNORMAL 3
#define FP_NORMAL 4
-#include <float.h> // for DBL_MIN and FLT_MIN
+#include "float.h" // for DBL_MIN and FLT_MIN
/*@
assigns \result \from x;
diff --git a/share/libc/signal.c b/share/libc/signal.c
new file mode 100644
index 0000000000000000000000000000000000000000..ad8a67724a2f5b7e75dfda62c3dbdc743a338f79
--- /dev/null
+++ b/share/libc/signal.c
@@ -0,0 +1,28 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2019 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include "signal.h"
+__PUSH_FC_STDLIB
+
+struct sigaction __fc_sigaction[SIGRTMAX+1];
+
+__POP_FC_STDLIB
diff --git a/share/libc/signal.h b/share/libc/signal.h
index 458175c0aef5c02d33692115211af148407e4fac..2605e2cea27bb152bf471e3748e2e73ec201ac61 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -198,7 +198,7 @@ extern int sigdelset(sigset_t *set, int signum);
extern int sigismember(const sigset_t *set, int signum);
extern struct sigaction __fc_sigaction[SIGRTMAX+1];
-extern struct sigaction *__fc_p_sigaction = __fc_sigaction;
+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;
diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index d9c40ce3983b2ad6ee27c15da26fba50d6889453..d779e8707e28b316771656686b7b4a0566843607 100644
--- a/share/libc/stdlib.c
+++ b/share/libc/stdlib.c
@@ -182,10 +182,9 @@ int unsetenv(const char *name)
return 0;
}
-#ifndef __FRAMAC__
-// declar __fc_strerror to ensure GCC can compile this file (for debugging and tests)
-char __fc_strerror[64];
-#endif
+
+unsigned short __fc_random48_counter[3];
+
// Note: this implementation does not check the alignment, since it cannot
// currently be specified in the memory model of most plug-ins
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 98a172ccdb0cdc17eab4112275724b0984f870b1..5d8864feeae2dba6e6195a2693e776f046b597a7 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -271,23 +271,9 @@ const unsigned long __fc_rand_max = __FC_RAND_MAX;
*/
extern int rand(void);
-#ifdef _POSIX_C_SOURCE
-# if _POSIX_C_SOURCE >= 200112L
-/*@ assigns \result \from __fc_random_counter ;
- @ assigns __fc_random_counter \from __fc_random_counter ;
- @ ensures result_range: 0 <= \result < 2147483648 ;
-*/
-extern long int lrand48 (void);
-
-/*@ assigns __fc_random_counter \from seed ; */
-extern void srand48 (long int seed);
-# endif
-#endif
-
/*@ assigns __fc_random_counter \from seed ; */
extern void srand(unsigned int seed);
-#if _XOPEN_SOURCE >= 500
/*@
assigns \result \from __fc_random_counter;
ensures result_range: 0 <= \result <= __fc_rand_max;
@@ -296,7 +282,84 @@ extern long int random(void);
/*@ assigns __fc_random_counter \from seed; */
extern void srandom(unsigned int seed);
-#endif
+
+// used to check if some *48() functions have called the seed initializer
+int __fc_random48_init __attribute__((FRAMA_C_MODEL));
+
+extern unsigned short __fc_random48_counter[3] __attribute__((FRAMA_C_MODEL));
+unsigned short *__fc_p_random48_counter = __fc_random48_counter;
+
+/*@
+ assigns __fc_random48_counter[0..2] \from seed;
+ assigns __fc_random48_init \from \nothing;
+ ensures random48_initialized: __fc_random48_init == 1;
+*/
+extern void srand48 (long int seed);
+
+/*@
+ requires initialization:initialized_seed16v: \initialized(seed16v+(0..2));
+ assigns __fc_random48_counter[0..2] \from indirect:seed16v[0..2];
+ assigns __fc_random48_init \from \nothing;
+ assigns \result \from __fc_p_random48_counter;
+ ensures random48_initialized: __fc_random48_init == 1;
+ ensures result_counter: \result == __fc_p_random48_counter;
+*/
+extern unsigned short *seed48(unsigned short seed16v[3]);
+
+/*@
+ assigns __fc_random48_counter[0..2] \from param[0..5];
+ assigns __fc_random48_init \from \nothing;
+ ensures random48_initialized: __fc_random48_init == 1;
+*/
+extern void lcong48(unsigned short param[7]);
+
+/*@
+ requires random48_initialized: __fc_random48_init == 1;
+ assigns __fc_random48_counter[0..2] \from __fc_random48_counter[0..2];
+ assigns \result \from __fc_random48_counter[0..2];
+ ensures result_range: \is_finite(\result) && 0.0 <= \result < 1.0;
+*/
+extern double drand48(void);
+
+/*@
+ requires initialization:initialized_xsubi: \initialized(xsubi+(0..2));
+ assigns __fc_random48_counter[0..2] \from __fc_random48_counter[0..2];
+ assigns \result \from __fc_random48_counter[0..2];
+ ensures result_range: \is_finite(\result) && 0.0 <= \result < 1.0;
+*/
+extern double erand48(unsigned short xsubi[3]);
+
+/*@
+ requires random48_initialized: __fc_random48_init == 1;
+ assigns __fc_random48_counter[0..2] \from __fc_random48_counter[0..2];
+ assigns \result \from __fc_random48_counter[0..2];
+ ensures result_range: 0 <= \result < 2147483648;
+*/
+extern long int lrand48 (void);
+
+/*@
+ requires initialization:initialized_xsubi: \initialized(xsubi+(0..2));
+ assigns __fc_random48_counter[0..2] \from __fc_random48_counter[0..2];
+ assigns \result \from __fc_random48_counter[0..2];
+ ensures result_range: 0 <= \result < 2147483648;
+*/
+extern long int nrand48 (unsigned short xsubi[3]);
+
+/*@
+ requires random48_initialized: __fc_random48_init == 1;
+ assigns __fc_random48_counter[0..2] \from __fc_random48_counter[0..2];
+ assigns \result \from __fc_random48_counter[0..2];
+ ensures result_range: -2147483648 <= \result < 2147483648;
+*/
+extern long int mrand48 (void);
+
+/*@
+ requires initialization:initialized_xsubi: \initialized(xsubi+(0..2));
+ assigns __fc_random48_counter[0..2] \from __fc_random48_counter[0..2];
+ assigns \result \from __fc_random48_counter[0..2];
+ ensures result_range: -2147483648 <= \result < 2147483648;
+*/
+extern long int jrand48 (unsigned short xsubi[3]);
/* ISO C: 7.20.3.1 */
/*@
diff --git a/share/libc/string.c b/share/libc/string.c
index 06662b1f297c20820c33eed85b77ad1febdcc9da..fc5a78937200d259df42f5b344fa923428738dc4 100644
--- a/share/libc/string.c
+++ b/share/libc/string.c
@@ -20,6 +20,7 @@
/* */
/**************************************************************************/
+#include "__fc_builtin.h"
#include "string.h"
#include "stdint.h" // for uintptr_t
#include "stdlib.h" // for malloc()
@@ -59,7 +60,14 @@ void* memcpy(void* restrict dest, const void* restrict src, size_t n)
complete behaviors;
disjoint behaviors;
*/
-static int memoverlap(char const *p, char const *q, size_t n);
+static int memoverlap(char const *p, char const *q, size_t n) {
+ uintptr_t
+ p1 = (uintptr_t)p, p2 = (uintptr_t)(p+n),
+ q1 = (uintptr_t)q, q2 = (uintptr_t)(q+n);
+ if (p1 <= q1 && p2 > q1) return -1;
+ else if (q1 <= p1 && q2 > p1) return 1;
+ else return 0;
+}
void* memmove(void* dest, const void* src, size_t n)
{
@@ -263,9 +271,19 @@ char *strstr(const char *haystack, const char *needle)
return NULL;
}
+char __fc_strerror[64];
+static int __fc_strerror_init;
+
char *strerror(int errnum)
{
- return "strerror message by Frama-C";
+#ifdef __FRAMAC__
+ if (!__fc_strerror_init) {
+ Frama_C_make_unknown(__fc_strerror, 63);
+ __fc_strerror[63] = 0;
+ __fc_strerror_init = 1;
+ }
+#endif
+ return __fc_strerror;
}
/* Warning: read considerations about malloc() in Frama-C */
@@ -299,4 +317,19 @@ char *strndup(const char *s, size_t n)
return p;
}
+char __fc_strsignal[64];
+static int __fc_strsignal_init;
+
+char *strsignal(int signum)
+{
+#ifdef __FRAMAC__
+ if (!__fc_strsignal_init) {
+ Frama_C_make_unknown(__fc_strsignal, 63);
+ __fc_strsignal[63] = 0;
+ __fc_strsignal_init = 1;
+ }
+#endif
+ return __fc_strsignal;
+}
+
__POP_FC_STDLIB
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
index 4758f62552e54c6fc56a0541096ffe84e2f43ae5..7de5c690d8ad85af8707b87772b3b9380bcc422a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
@@ -34,7 +34,7 @@ Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 32):
+Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 33):
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Assume {
@@ -58,7 +58,7 @@ Prove: to_uint32(1 + i) <= n.
------------------------------------------------------------
-Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 32):
+Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 33):
Assume {
Type: is_uint32(n).
(* Heap *)
@@ -73,7 +73,7 @@ Prove: 0 <= n.
------------------------------------------------------------
-Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 33):
+Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 34):
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = a_1[shift_sint8(dest_0, i) <- a_1[shift_sint8(src_0, i)]].
@@ -100,24 +100,24 @@ Prove: a_2[shift_sint8(src_0, i_1)] = a_2[shift_sint8(dest_0, i_1)].
------------------------------------------------------------
-Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 33):
+Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 34):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 34) (1/3):
+Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 35) (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 34) (2/3):
-Effect at line 37
+Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 35) (2/3):
+Effect at line 38
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 34) (3/3):
-Effect at line 38
+Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 35) (3/3):
+Effect at line 39
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(dest_0, i).
@@ -145,12 +145,12 @@ Prove: included(a_2, 1, a, n).
------------------------------------------------------------
Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 96) in 'memcpy':
-Effect at line 37
+Effect at line 38
Prove: true.
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 37):
+Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 38):
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Assume {
@@ -174,7 +174,7 @@ Prove: i < to_uint32(1 + i).
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 37):
+Goal Positivity of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 38):
Prove: true.
------------------------------------------------------------
@@ -248,7 +248,7 @@ Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 71):
+Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 79):
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
@@ -285,7 +285,7 @@ Prove: to_uint32(1 + i) <= n.
------------------------------------------------------------
-Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 71):
+Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 79):
Let a = shift_sint8(d, 0).
Let a_1 = shift_sint8(s, 0).
Assume {
@@ -311,7 +311,7 @@ Prove: 0 <= n.
------------------------------------------------------------
-Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 72):
+Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 80):
Let a = shift_sint8(d, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(s, 0).
@@ -351,12 +351,12 @@ Prove: a_1[shift_sint8(d, i) <- a_1[shift_sint8(s, i)]][shift_sint8(d, i_1)] =
------------------------------------------------------------
-Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 72):
+Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 80):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 73):
+Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 81):
Let a = shift_sint8(d, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(s, 0).
@@ -396,12 +396,12 @@ Prove: a_1[shift_sint8(d, i) <- a_1[shift_sint8(s, i)]][a_3] = Mchar_0[a_3].
------------------------------------------------------------
-Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 73):
+Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 81):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 83):
+Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 91):
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
@@ -438,7 +438,7 @@ Prove: to_uint32(i - 1) < n.
------------------------------------------------------------
-Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 83):
+Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 91):
Let a = shift_sint8(d, 0).
Let a_1 = shift_sint8(s, 0).
Assume {
@@ -464,7 +464,7 @@ Prove: to_uint32(n - 1) < n.
------------------------------------------------------------
-Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 84):
+Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 92):
Let a = shift_sint8(d, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(s, 0).
@@ -504,7 +504,7 @@ Prove: a_1[shift_sint8(d, i) <- a_1[shift_sint8(s, i)]][shift_sint8(d, i_1)] =
------------------------------------------------------------
-Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 84):
+Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 92):
Let a = shift_sint8(dest_0, 0).
Let a_1 = shift_sint8(src_0, 0).
Assume {
@@ -532,7 +532,7 @@ Prove: Mchar_0[shift_sint8(src_0, i)] = Mchar_0[shift_sint8(dest_0, i)].
------------------------------------------------------------
-Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 85):
+Goal Preservation of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 93):
Let a = shift_sint8(d, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(s, 0).
@@ -572,24 +572,24 @@ Prove: a_1[shift_sint8(d, i) <- a_1[shift_sint8(s, i)]][a_3] = Mchar_0[a_3].
------------------------------------------------------------
-Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 85):
+Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 93):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 74) (1/3):
+Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 82) (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 74) (2/3):
-Effect at line 77
+Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 82) (2/3):
+Effect at line 85
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 74) (3/3):
-Effect at line 78
+Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 82) (3/3):
+Effect at line 86
Let a = shift_sint8(d, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
@@ -629,19 +629,19 @@ Prove: included(a_3, 1, a, n).
------------------------------------------------------------
-Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 86) (1/3):
+Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 94) (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 86) (2/3):
-Effect at line 89
+Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 94) (2/3):
+Effect at line 97
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 86) (3/3):
-Effect at line 90
+Goal Loop assigns (file FRAMAC_SHARE/libc/string.c, line 94) (3/3):
+Effect at line 98
Let a = shift_sint8(d, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
@@ -692,31 +692,31 @@ Prove: true.
------------------------------------------------------------
Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (2/7):
-Effect at line 66
+Effect at line 74
Prove: true.
------------------------------------------------------------
Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (3/7):
-Call Result at line 69
+Call Result at line 77
Prove: true.
------------------------------------------------------------
Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (4/7):
-Effect at line 77
+Effect at line 85
Prove: true.
------------------------------------------------------------
Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (5/7):
-Effect at line 89
+Effect at line 97
Prove: true.
------------------------------------------------------------
Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (6/7):
-Effect at line 91
+Effect at line 99
Let a = shift_sint8(d, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
@@ -756,12 +756,12 @@ Prove: 0 < n.
------------------------------------------------------------
Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (7/7):
-Effect at line 93
+Effect at line 101
Prove: true.
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 77):
+Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 85):
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
@@ -798,12 +798,12 @@ Prove: i < to_uint32(1 + i).
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 77):
+Goal Positivity of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 85):
Prove: true.
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 89):
+Goal Decreasing of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 97):
Let a = shift_sint8(dest_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
Let a_2 = shift_sint8(src_0, 0).
@@ -840,7 +840,7 @@ Prove: to_uint32(i - 1) < i.
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 89):
+Goal Positivity of Loop variant at loop (file FRAMAC_SHARE/libc/string.c, line 97):
Prove: true.
------------------------------------------------------------
diff --git a/tests/builtins/oracle/Longinit_sequencer.res.oracle b/tests/builtins/oracle/Longinit_sequencer.res.oracle
index 6813be1ec3eab0ce308b848cf24d36084f14d290..6deb10c4aea0a67d5036bafc38745c7f19bd3406 100644
--- a/tests/builtins/oracle/Longinit_sequencer.res.oracle
+++ b/tests/builtins/oracle/Longinit_sequencer.res.oracle
@@ -95,6 +95,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -331,6 +334,9 @@ Values at end of function main:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -562,6 +568,9 @@ Values at end of function main:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/builtins/oracle/free.res.oracle b/tests/builtins/oracle/free.res.oracle
index 530cf9b1670ade122a3bd6b2c73d80b4dffdfa14..c3f99748ef4e105b4ac514f33fb35fa4d2fd4b42 100644
--- a/tests/builtins/oracle/free.res.oracle
+++ b/tests/builtins/oracle/free.res.oracle
@@ -18,6 +18,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/builtins/oracle/linked_list.0.res.oracle b/tests/builtins/oracle/linked_list.0.res.oracle
index c802214c1feacc1769aac9e3e60da444bcdba705..a720cea4364ad8be5ec34cc894fc4c0c6c6b63a0 100644
--- a/tests/builtins/oracle/linked_list.0.res.oracle
+++ b/tests/builtins/oracle/linked_list.0.res.oracle
@@ -18,6 +18,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -38,7 +41,7 @@
==END OF DUMP==
[eva] computing for function malloc <- main.
Called from tests/builtins/linked_list.c:41.
-[eva:alarm] share/libc/stdlib.h:331: Warning:
+[eva:alarm] share/libc/stdlib.h:394: Warning:
function malloc, behavior allocation: postcondition 'allocation' got status unknown.
[eva] Recording results for malloc
[eva] Done for function malloc
@@ -55,6 +58,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -88,6 +94,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -124,6 +133,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -159,6 +171,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -198,6 +213,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -235,6 +253,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -276,6 +297,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -315,6 +339,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -358,6 +385,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -399,6 +429,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -444,6 +477,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -732,6 +768,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -1022,6 +1061,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index ecd278086d238f8c27853ff9484cb92d8f834ed3..67b3d10651f9e9d8f7d950db2f0cc401ee64c0bf 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -18,6 +18,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -38,7 +41,7 @@
==END OF DUMP==
[eva] computing for function malloc <- main.
Called from tests/builtins/linked_list.c:41.
-[eva:alarm] share/libc/stdlib.h:331: Warning:
+[eva:alarm] share/libc/stdlib.h:394: Warning:
function malloc, behavior allocation: postcondition 'allocation' got status unknown.
[eva] Recording results for malloc
[eva] Done for function malloc
@@ -55,6 +58,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -88,6 +94,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -124,6 +133,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -159,6 +171,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -198,6 +213,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -235,6 +253,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -276,6 +297,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -315,6 +339,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -358,6 +385,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -400,6 +430,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -446,6 +479,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -486,6 +522,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -524,6 +563,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/builtins/oracle/linked_list.2.res.oracle b/tests/builtins/oracle/linked_list.2.res.oracle
index aff1af029cc355973010dd10b08d96f50201cd5b..4687366532f8f130442769db11f45930b3d4ec6e 100644
--- a/tests/builtins/oracle/linked_list.2.res.oracle
+++ b/tests/builtins/oracle/linked_list.2.res.oracle
@@ -18,6 +18,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -38,7 +41,7 @@
==END OF DUMP==
[eva] computing for function malloc <- main.
Called from tests/builtins/linked_list.c:41.
-[eva:alarm] share/libc/stdlib.h:331: Warning:
+[eva:alarm] share/libc/stdlib.h:394: Warning:
function malloc, behavior allocation: postcondition 'allocation' got status unknown.
[eva] Recording results for malloc
[eva] Done for function malloc
@@ -55,6 +58,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -87,6 +93,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -123,6 +132,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -158,6 +170,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -197,6 +212,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -234,6 +252,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -275,6 +296,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -314,6 +338,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -357,6 +384,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -398,6 +428,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -443,6 +476,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -486,6 +522,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -533,6 +572,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -578,6 +620,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -627,6 +672,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -674,6 +722,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -725,6 +776,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -774,6 +828,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -827,6 +884,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/builtins/oracle/malloc-size-zero.0.res.oracle b/tests/builtins/oracle/malloc-size-zero.0.res.oracle
index 500a3e8e4ca5c38ee8bb80b8f4dec4f9721712eb..bc2ae68d215be83bbcf34bd7361593e22743b2e1 100644
--- a/tests/builtins/oracle/malloc-size-zero.0.res.oracle
+++ b/tests/builtins/oracle/malloc-size-zero.0.res.oracle
@@ -56,6 +56,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/builtins/oracle/malloc-size-zero.1.res.oracle b/tests/builtins/oracle/malloc-size-zero.1.res.oracle
index 51aa2e2500e0e3f3cb5a6540781cced57f4e5abc..7de8421d47ebffba67d4c480b3b735a7a90e2b23 100644
--- a/tests/builtins/oracle/malloc-size-zero.1.res.oracle
+++ b/tests/builtins/oracle/malloc-size-zero.1.res.oracle
@@ -35,6 +35,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/builtins/oracle/realloc.res.oracle b/tests/builtins/oracle/realloc.res.oracle
index 934055588511af821835ed8c8a2890b94ee2b635..9555b2ee2355ad999ed6d8af372676fe1b6171f4 100644
--- a/tests/builtins/oracle/realloc.res.oracle
+++ b/tests/builtins/oracle/realloc.res.oracle
@@ -15,6 +15,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -42,6 +45,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -91,6 +97,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -134,6 +143,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -164,6 +176,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -236,6 +251,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -291,6 +309,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -355,6 +376,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -383,6 +407,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -456,6 +483,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -480,6 +510,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -520,6 +553,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -559,6 +595,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -599,6 +638,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -627,6 +669,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/builtins/oracle/realloc_multiple.0.res.oracle b/tests/builtins/oracle/realloc_multiple.0.res.oracle
index 2999729e2e1fed6229f37b08c755028689da2928..9e00330021274a3cba7e16899bce6fa1d0937cc8 100644
--- a/tests/builtins/oracle/realloc_multiple.0.res.oracle
+++ b/tests/builtins/oracle/realloc_multiple.0.res.oracle
@@ -25,6 +25,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -60,6 +63,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -110,6 +116,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -148,6 +157,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -203,6 +215,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -246,6 +261,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -285,6 +303,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/builtins/oracle/realloc_multiple.1.res.oracle b/tests/builtins/oracle/realloc_multiple.1.res.oracle
index 6d0bc83f7e6d44aead79f735f2ff2a4800786cad..7f2845785857295d82991f7f7c3606adf573ba0f 100644
--- a/tests/builtins/oracle/realloc_multiple.1.res.oracle
+++ b/tests/builtins/oracle/realloc_multiple.1.res.oracle
@@ -33,6 +33,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -68,6 +71,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -92,6 +98,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -152,6 +161,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -190,6 +202,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -214,6 +229,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -283,6 +301,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -330,6 +351,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -370,6 +394,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/builtins/oracle/strnlen.res.oracle b/tests/builtins/oracle/strnlen.res.oracle
index 097bcf8ac85f81bbc49e03b7b0a16135a388faf8..93b9252b5320d5985fd6b26dc08bffb83bb40c9e 100644
--- a/tests/builtins/oracle/strnlen.res.oracle
+++ b/tests/builtins/oracle/strnlen.res.oracle
@@ -38,6 +38,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
diff --git a/tests/libc/check_full_libc.sh b/tests/libc/check_full_libc.sh
index c20a68fd43c2ce1f458b489815299f85edf2c877..ebfc06b481cff211a34b3a2988902444058bc48e 100755
--- a/tests/libc/check_full_libc.sh
+++ b/tests/libc/check_full_libc.sh
@@ -11,7 +11,7 @@ done;
for A in `ls *.c`;
do
- if ! grep -q $A fc_runtime.c ../../tests/libc/fc_libc.c ;
+ if ! grep -q $A __fc_runtime.c ../../tests/libc/fc_libc.c ;
then echo Not included implementation \'$A\';
fi ;
done;
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 5688d0e6e4f9e8c9ab57ab0ce3c62c2b9fdbdbd0..7f27becef31786b70e483b2adeda229886900278 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -18,7 +18,7 @@
#define _POSIX_C_SOURCE 200112L
#define _GNU_SOURCE 1
-#include "share/libc/fc_runtime.c"
+#include "share/libc/__fc_runtime.c"
#include "alloca.h"
#include "arpa/inet.h"
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index 6e7f751bf3ca6d1d5a1eeefee38a7b5424392b83..420792611b3362b3a757d44b3f9aaed2938edbb8 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 82)
+ Syntactically reachable functions = 2 (out of 112)
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 ea255ba62786f4d021615c2829e5b32294780c15..eab1d99264c45d6300692246cc0ac9ef6fca48d0 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -13,14 +13,16 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
-[metrics] Defined functions (76)
+[metrics] Defined functions (82)
======================
+ Frama_C_abort (1 call); Frama_C_char_interval (1 call);
Frama_C_double_interval (0 call); Frama_C_float_interval (0 call);
- Frama_C_interval (14 calls); Frama_C_nondet (12 calls);
- Frama_C_nondet_ptr (0 call); __FC_assert (0 call); __fc_initenv (4 calls);
- __finite (0 call); __finitef (0 call); abs (0 call); atoi (0 call);
- calloc (0 call); char_equal_ignore_case (1 call); fabs (0 call);
- fabsf (0 call); feholdexcept (0 call); fesetenv (0 call);
+ Frama_C_interval (14 calls); Frama_C_make_unknown (4 calls);
+ Frama_C_nondet (12 calls); Frama_C_nondet_ptr (0 call);
+ Frama_C_update_entropy (7 calls); __FC_assert (0 call);
+ __fc_initenv (4 calls); __finite (0 call); __finitef (0 call); abs (0 call);
+ atoi (0 call); calloc (0 call); char_equal_ignore_case (1 call);
+ fabs (0 call); fabsf (0 call); feholdexcept (0 call); fesetenv (0 call);
fetestexcept (0 call); getaddrinfo (0 call); getenv (0 call);
gethostbyname (0 call); getline (0 call); glob (0 call); globfree (0 call);
imaxabs (0 call); imaxdiv (0 call); isalnum (0 call); isalpha (0 call);
@@ -28,29 +30,28 @@
islower (0 call); isprint (0 call); ispunct (0 call); isspace (1 call);
isupper (0 call); isxdigit (0 call); localeconv (0 call); main (0 call);
memchr (0 call); memcmp (0 call); memcpy (4 calls); memmove (0 call);
- memrchr (0 call); memset (1 call); posix_memalign (0 call); putenv (0 call);
- res_search (1 call); setenv (0 call); setlocale (0 call);
- strcasecmp (0 call); strcat (0 call); strchr (3 calls); strcmp (0 call);
- strcpy (0 call); strdup (0 call); strerror (0 call); strlen (6 calls);
- strncat (0 call); strncmp (0 call); strncpy (2 calls); strndup (0 call);
- strnlen (0 call); strrchr (0 call); strstr (0 call); tolower (0 call);
- toupper (0 call); unsetenv (0 call); wcscat (0 call); wcscpy (0 call);
- wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call);
- wmemset (0 call);
+ memoverlap (1 call); memrchr (0 call); memset (1 call);
+ posix_memalign (0 call); putenv (0 call); res_search (1 call);
+ setenv (0 call); setlocale (0 call); strcasecmp (0 call); strcat (0 call);
+ strchr (3 calls); strcmp (0 call); strcpy (0 call); strdup (0 call);
+ strerror (0 call); strlen (6 calls); strncat (0 call); strncmp (0 call);
+ strncpy (2 calls); strndup (0 call); strnlen (0 call); strrchr (0 call);
+ strsignal (0 call); strstr (0 call); tolower (0 call); toupper (0 call);
+ unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
+ wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
- Undefined functions (377)
+ Undefined functions (379)
=========================
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);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
- Frama_C_long_long_interval (0 call); Frama_C_make_unknown (2 calls);
+ Frama_C_long_long_interval (0 call);
Frama_C_real_interval_as_double (0 call); Frama_C_short_interval (0 call);
Frama_C_size_t_interval (0 call); Frama_C_unsigned_char_interval (0 call);
Frama_C_unsigned_int_interval (0 call);
Frama_C_unsigned_long_interval (0 call);
Frama_C_unsigned_long_long_interval (0 call);
- Frama_C_unsigned_short_interval (0 call); Frama_C_update_entropy (5 calls);
- _Exit (0 call); __builtin_sadd_overflow (0 call);
+ Frama_C_unsigned_short_interval (0 call); _Exit (0 call);
+ __builtin_abort (1 call); __builtin_sadd_overflow (0 call);
__builtin_saddl_overflow (0 call); __builtin_saddll_overflow (0 call);
__builtin_smul_overflow (0 call); __builtin_smull_overflow (0 call);
__builtin_smulll_overflow (0 call); __builtin_ssub_overflow (0 call);
@@ -77,42 +78,43 @@
clock_nanosleep (0 call); close (0 call); closedir (0 call);
closelog (0 call); connect (0 call); cos (0 call); cosf (0 call);
cosl (0 call); creat (0 call); ctime (0 call); difftime (0 call);
- dirname (0 call); div (0 call); dup (0 call); dup2 (0 call); execl (0 call);
- execle (0 call); execlp (0 call); execv (0 call); execve (0 call);
- execvp (0 call); exit (0 call); exp (0 call); expf (0 call); fabsl (0 call);
- fclose (0 call); fcntl (0 call); fdopen (0 call); feof (2 calls);
- feof_unlocked (0 call); ferror (2 calls); ferror_unlocked (0 call);
- fflush (0 call); fgetc (1 call); fgetpos (0 call); fgets (0 call);
- fgetws (0 call); fileno (0 call); fileno_unlocked (0 call); flock (0 call);
- flockfile (0 call); floor (0 call); floorf (0 call); floorl (0 call);
- fmod (0 call); fmodf (0 call); fopen (0 call); fork (0 call);
- fputc (0 call); fputs (0 call); fread (0 call); free (1 call);
- freeaddrinfo (0 call); freopen (0 call); fseek (0 call); fsetpos (0 call);
- ftell (0 call); ftrylockfile (0 call); funlockfile (0 call);
- fwrite (0 call); gai_strerror (0 call); getc (0 call);
- getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
- getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
- gethostname (0 call); getitimer (0 call); getopt (0 call);
- getopt_long (0 call); getopt_long_only (0 call); 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);
+ dirname (0 call); div (0 call); drand48 (0 call); dup (0 call);
+ dup2 (0 call); erand48 (0 call); execl (0 call); execle (0 call);
+ execlp (0 call); execv (0 call); execve (0 call); execvp (0 call);
+ exit (0 call); exp (0 call); expf (0 call); fabsl (0 call); fclose (0 call);
+ fcntl (0 call); fdopen (0 call); feof (2 calls); feof_unlocked (0 call);
+ ferror (2 calls); ferror_unlocked (0 call); fflush (0 call); fgetc (1 call);
+ fgetpos (0 call); fgets (0 call); fgetws (0 call); fileno (0 call);
+ fileno_unlocked (0 call); flock (0 call); flockfile (0 call);
+ floor (0 call); floorf (0 call); floorl (0 call); fmod (0 call);
+ fmodf (0 call); fopen (0 call); fork (0 call); fputc (0 call);
+ fputs (0 call); fread (0 call); free (1 call); freeaddrinfo (0 call);
+ freopen (0 call); fseek (0 call); fsetpos (0 call); ftell (0 call);
+ ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call);
+ gai_strerror (0 call); getc (0 call); getc_unlocked (0 call);
+ getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
+ getegid (0 call); geteuid (0 call); getgid (0 call); gethostname (0 call);
+ getitimer (0 call); getopt (0 call); getopt_long (0 call);
+ getopt_long_only (0 call); 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); jrand48 (0 call); kill (0 call);
+ killpg (0 call); labs (0 call); lcong48 (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);
+ mbstowcs (0 call); mbtowc (0 call); mkdir (0 call); mkstemp (0 call);
+ mktime (0 call); mrand48 (0 call); nan (0 call); nanf (0 call);
+ nanl (0 call); nanosleep (0 call); nrand48 (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);
@@ -123,9 +125,9 @@
rand (0 call); random (0 call); read (0 call); readdir (0 call);
readv (0 call); realloc (3 calls); recv (0 call); recvmsg (0 call);
remove (0 call); rename (0 call); rewind (0 call); round (0 call);
- 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);
+ roundf (0 call); roundl (0 call); seed48 (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); 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);
@@ -138,29 +140,28 @@
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);
+ strsep (0 call); strspn (0 call); strtod (0 call); strtof (0 call);
+ strtoimax (0 call); strtok (0 call); strtok_r (0 call); strtol (0 call);
+ strtold (0 call); strtoll (0 call); strtoul (0 call); strtoull (0 call);
+ strxfrm (0 call); sync (0 call); sysconf (0 call); syslog (0 call);
+ system (0 call); tcgetattr (0 call); tcsetattr (0 call); time (0 call);
+ times (0 call); tmpfile (0 call); tmpnam (0 call); trunc (0 call);
+ truncf (0 call); truncl (0 call); ttyname (0 call); tzset (0 call);
+ umask (0 call); ungetc (0 call); 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)
+ 'Extern' global variables (17)
==============================
__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_sigaction; __fc_strerror; __fc_strsignal; __fc_ttyname;
- __fc_wctomb_state; optarg; opterr; optopt; tzname
+ __fc_ttyname; __fc_wctomb_state; optarg; opterr; optopt; tzname
Potential entry points (1)
==========================
@@ -168,18 +169,18 @@
Global metrics
==============
- Sloc = 1026
- Decision point = 195
- Global variables = 65
- If = 186
- Loop = 42
- Goto = 84
- Assignment = 415
- Exit point = 76
- Function = 453
- Function call = 84
- Pointer dereferencing = 157
- Cyclomatic complexity = 271
+ Sloc = 1083
+ Decision point = 204
+ Global variables = 68
+ If = 195
+ Loop = 43
+ Goto = 89
+ Assignment = 438
+ Exit point = 82
+ Function = 461
+ Function call = 89
+ Pointer dereferencing = 158
+ Cyclomatic complexity = 286
/* Generated by Frama-C */
#include "__fc_builtin.c"
#include "__fc_builtin.h"
@@ -216,6 +217,7 @@
#include "pthread.h"
#include "pwd.h"
#include "setjmp.h"
+#include "signal.c"
#include "signal.h"
#include "stdarg.h"
#include "stdint.h"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index aecfd20abf26a67bc0a99da4ee9d7f8dc15b3c52..a0d63cf77b129c701a89d1e3da29808ad515ff32 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
/* Generated by Frama-C */
typedef unsigned int size_t;
-struct __anonstruct_fenv_t_2 {
+struct __fc_fenv_t {
unsigned short __control_word ;
unsigned short __unused1 ;
unsigned short __status_word ;
@@ -16,14 +16,14 @@ struct __anonstruct_fenv_t_2 {
unsigned short __data_selector ;
unsigned short __unused5 ;
};
-typedef struct __anonstruct_fenv_t_2 fenv_t;
+typedef struct __fc_fenv_t fenv_t;
struct option {
char const *name ;
int has_arg ;
int *flag ;
int val ;
};
-struct __anonstruct_glob_t_3 {
+struct __fc_glob_t {
unsigned int gl_pathc ;
char **gl_pathv ;
unsigned int gl_offs ;
@@ -34,7 +34,7 @@ struct __anonstruct_glob_t_3 {
int (*gl_lstat)(char const * __restrict , void * __restrict ) ;
int (*gl_stat)(char const * __restrict , void * __restrict ) ;
};
-typedef struct __anonstruct_glob_t_3 glob_t;
+typedef struct __fc_glob_t glob_t;
typedef int wchar_t;
struct __fc_div_t {
int quot ;
@@ -54,12 +54,13 @@ typedef struct __fc_lldiv_t lldiv_t;
typedef unsigned char uint8_t;
typedef unsigned short uint16_t;
typedef unsigned int uint32_t;
+typedef unsigned int uintptr_t;
typedef long long intmax_t;
-struct __anonstruct_imaxdiv_t_4 {
+struct __fc_imaxdiv_t {
intmax_t quot ;
intmax_t rem ;
};
-typedef struct __anonstruct_imaxdiv_t_4 imaxdiv_t;
+typedef struct __fc_imaxdiv_t imaxdiv_t;
struct lconv {
char *decimal_point ;
char *thousands_sep ;
@@ -86,38 +87,38 @@ struct lconv {
char int_p_sign_posn ;
char int_n_sign_posn ;
};
-union __anonunion_u_5 {
+union __fc_u_finitef {
float f ;
unsigned short w[2] ;
};
-union __anonunion_u_6 {
+union __fc_u_finite {
double d ;
unsigned short w[4] ;
};
-struct __anonstruct_pthread_attr_t_7 {
+struct __fc_pthread_attr_t {
int _fc ;
};
-typedef struct __anonstruct_pthread_attr_t_7 pthread_attr_t;
-struct __anonstruct_pthread_cond_t_10 {
+typedef struct __fc_pthread_attr_t pthread_attr_t;
+struct __fc_pthread_cond_t {
int _fc ;
};
-typedef struct __anonstruct_pthread_cond_t_10 pthread_cond_t;
-struct __anonstruct_pthread_condattr_t_11 {
+typedef struct __fc_pthread_cond_t pthread_cond_t;
+struct __fc_pthread_condattr_t {
int _fc ;
};
-typedef struct __anonstruct_pthread_condattr_t_11 pthread_condattr_t;
-struct __anonstruct_pthread_mutex_t_13 {
+typedef struct __fc_pthread_condattr_t pthread_condattr_t;
+struct __fc_pthread_mutex_t {
int _fc ;
};
-typedef struct __anonstruct_pthread_mutex_t_13 pthread_mutex_t;
-struct __anonstruct_pthread_mutexattr_t_14 {
+typedef struct __fc_pthread_mutex_t pthread_mutex_t;
+struct __fc_pthread_mutexattr_t {
int _fc ;
};
-typedef struct __anonstruct_pthread_mutexattr_t_14 pthread_mutexattr_t;
-struct __anonstruct_pthread_t_19 {
+typedef struct __fc_pthread_mutexattr_t pthread_mutexattr_t;
+struct __fc_pthread_t {
int _fc ;
};
-typedef struct __anonstruct_pthread_t_19 pthread_t;
+typedef struct __fc_pthread_t pthread_t;
typedef int pid_t;
typedef unsigned int gid_t;
typedef unsigned int uid_t;
@@ -126,7 +127,7 @@ union sigval {
int sival_int ;
void *sival_ptr ;
};
-struct __anonstruct_siginfo_t_20 {
+struct __anonstruct_siginfo_t_1 {
int si_signo ;
int si_code ;
union sigval si_value ;
@@ -137,7 +138,7 @@ struct __anonstruct_siginfo_t_20 {
int si_status ;
int si_band ;
};
-typedef struct __anonstruct_siginfo_t_20 siginfo_t;
+typedef struct __anonstruct_siginfo_t_1 siginfo_t;
struct sigaction {
void (*sa_handler)(int ) ;
void (*sa_sigaction)(int , siginfo_t *, void *) ;
@@ -174,7 +175,7 @@ struct in_addr {
struct in6_addr {
uint8_t s6_addr[16] ;
};
-enum __anonenum_22 {
+enum __fc_ipproto {
IPPROTO_IP = 0,
IPPROTO_HOPOPTS = 0,
IPPROTO_ICMP = 1,
@@ -296,10 +297,10 @@ struct DIR {
struct dirent **__fc_dir_entries ;
};
typedef struct DIR DIR;
-struct __anonstruct_fd_set_25 {
+struct __fc_fd_set {
long __fc_fd_set[(unsigned int)1024 / ((unsigned int)8 * sizeof(long))] ;
};
-typedef struct __anonstruct_fd_set_25 fd_set;
+typedef struct __fc_fd_set fd_set;
typedef unsigned int useconds_t;
struct flock {
short l_type ;
@@ -337,11 +338,11 @@ struct passwd {
char *pw_shell ;
};
typedef int ( jmp_buf)[5];
-struct __anonstruct_sigjmp_buf_43 {
+struct __anonstruct_sigjmp_buf_22 {
jmp_buf buf ;
sigset_t sigs ;
};
-typedef struct __anonstruct_sigjmp_buf_43 sigjmp_buf;
+typedef struct __anonstruct_sigjmp_buf_22 sigjmp_buf;
struct _code {
char const *c_name ;
int c_val ;
@@ -373,13 +374,7 @@ struct termios {
};
int volatile Frama_C_entropy_source __attribute__((__unused__,
__FRAMA_C_MODEL__));
-/*@ requires valid_p: \valid(p + (0 .. l - 1));
- ensures initialization: \initialized(\old(p) + (0 .. \old(l) - 1));
- assigns *(p + (0 .. l - 1)), Frama_C_entropy_source;
- assigns *(p + (0 .. l - 1)) \from Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern void Frama_C_make_unknown(char *p, size_t l);
+void Frama_C_make_unknown(char *p, size_t l);
int Frama_C_nondet(int a, int b);
@@ -404,13 +399,7 @@ extern int Frama_C_interval_split(int min, int max);
extern unsigned char Frama_C_unsigned_char_interval(unsigned char min,
unsigned char max);
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern char Frama_C_char_interval(char min, char max);
+char Frama_C_char_interval(char min, char max);
/*@ requires order: min ≤ max;
ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
@@ -503,10 +492,7 @@ double Frama_C_double_interval(double min, double max);
*/
extern double Frama_C_real_interval_as_double(double min, double max);
-/*@ terminates \false;
- ensures never_terminates: \false;
- assigns \nothing; */
-extern __attribute__((__noreturn__)) void Frama_C_abort(void);
+ __attribute__((__noreturn__)) void Frama_C_abort(void);
/*@ assigns \result;
assigns \result \from p; */
@@ -524,6 +510,144 @@ extern long long Frama_C_abstract_max(long long i);
assigns \result \from i; */
extern long long Frama_C_abstract_min(long long i);
+/*@ assigns Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+void Frama_C_update_entropy(void)
+{
+ Frama_C_entropy_source = Frama_C_entropy_source;
+ return;
+}
+
+/*@ requires valid_p: \valid(p + (0 .. l - 1));
+ ensures initialization: \initialized(\old(p) + (0 .. \old(l) - 1));
+ assigns *(p + (0 .. l - 1)), Frama_C_entropy_source;
+ assigns *(p + (0 .. l - 1)) \from Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+void Frama_C_make_unknown(char *p, size_t l)
+{
+ Frama_C_update_entropy();
+ {
+ size_t i = (unsigned int)0;
+ while (i < l) {
+ *(p + i) = (char)Frama_C_entropy_source;
+ i += (size_t)1;
+ }
+ }
+ return;
+}
+
+/*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from a, b, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+int Frama_C_nondet(int a, int b)
+{
+ int tmp;
+ Frama_C_update_entropy();
+ if (Frama_C_entropy_source) tmp = a; else tmp = b;
+ return tmp;
+}
+
+/*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from a, b, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+void *Frama_C_nondet_ptr(void *a, void *b)
+{
+ void *tmp;
+ Frama_C_update_entropy();
+ if (Frama_C_entropy_source) tmp = a; else tmp = b;
+ return tmp;
+}
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+int Frama_C_interval(int min, int max)
+{
+ int r;
+ int aux;
+ Frama_C_update_entropy();
+ aux = Frama_C_entropy_source;
+ if (aux >= min)
+ if (aux <= max) r = aux; else r = min;
+ else r = min;
+ return r;
+}
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+char Frama_C_char_interval(char min, char max)
+{
+ char __retres;
+ int r;
+ char aux;
+ Frama_C_update_entropy();
+ aux = (char)Frama_C_entropy_source;
+ if ((int)aux >= (int)min)
+ if ((int)aux <= (int)max) r = (int)aux; else r = (int)min;
+ else r = (int)min;
+ __retres = (char)r;
+ return __retres;
+}
+
+/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
+ requires order: min ≤ max;
+ ensures
+ result_bounded:
+ \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+float Frama_C_float_interval(float min, float max)
+{
+ float tmp;
+ Frama_C_update_entropy();
+ if (Frama_C_entropy_source) tmp = min; else tmp = max;
+ return tmp;
+}
+
+/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
+ requires order: min ≤ max;
+ ensures
+ result_bounded:
+ \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+double Frama_C_double_interval(double min, double max)
+{
+ double tmp;
+ Frama_C_update_entropy();
+ if (Frama_C_entropy_source) tmp = min; else tmp = max;
+ return tmp;
+}
+
+extern __attribute__((__noreturn__)) void __builtin_abort(void);
+
+/*@ terminates \false;
+ ensures never_terminates: \false;
+ assigns \nothing; */
+ __attribute__((__noreturn__)) void Frama_C_abort(void);
+void Frama_C_abort(void)
+{
+ __builtin_abort();
+ return;
+}
+
void __FC_assert(int c, char const *file, int line, char const *expr);
/*@ assigns \nothing; */
@@ -995,7 +1119,7 @@ int fetestexcept(int excepts);
int feholdexcept(fenv_t *envp);
-void fesetenv(fenv_t const *envp);
+int fesetenv(fenv_t const *envp);
static int volatile fetestexcept___fc_random_fetestexcept __attribute__((
__FRAMA_C_MODEL__));
@@ -1015,10 +1139,12 @@ int feholdexcept(fenv_t *envp)
return __retres;
}
-void fesetenv(fenv_t const *envp)
+int fesetenv(fenv_t const *envp)
{
+ int __retres;
__fc_fenv_state = *envp;
- return;
+ __retres = 0;
+ return __retres;
}
extern char *optarg;
@@ -1662,17 +1788,6 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
*/
extern int rand(void);
-/*@ ensures result_range: 0 ≤ \result < 2147483648;
- assigns \result, __fc_random_counter;
- assigns \result \from __fc_random_counter;
- assigns __fc_random_counter \from __fc_random_counter;
- */
-extern long lrand48(void);
-
-/*@ assigns __fc_random_counter;
- assigns __fc_random_counter \from seed; */
-extern void srand48(long seed);
-
/*@ assigns __fc_random_counter;
assigns __fc_random_counter \from seed; */
extern void srand(unsigned int seed);
@@ -1687,6 +1802,92 @@ extern long random(void);
assigns __fc_random_counter \from seed; */
extern void srandom(unsigned int seed);
+int __fc_random48_init __attribute__((__FRAMA_C_MODEL__));
+unsigned short __fc_random48_counter[3] __attribute__((__FRAMA_C_MODEL__));
+unsigned short *__fc_p_random48_counter = __fc_random48_counter;
+/*@ ensures random48_initialized: __fc_random48_init ≡ 1;
+ assigns __fc_random48_counter[0 .. 2], __fc_random48_init;
+ assigns __fc_random48_counter[0 .. 2] \from seed;
+ assigns __fc_random48_init \from \nothing;
+ */
+extern void srand48(long seed);
+
+/*@ requires
+ initialization: initialized_seed16v: \initialized(seed16v + (0 .. 2));
+ ensures random48_initialized: __fc_random48_init ≡ 1;
+ ensures result_counter: \result ≡ __fc_p_random48_counter;
+ assigns __fc_random48_counter[0 .. 2], __fc_random48_init, \result;
+ assigns __fc_random48_counter[0 .. 2]
+ \from (indirect: *(seed16v + (0 .. 2)));
+ assigns __fc_random48_init \from \nothing;
+ assigns \result \from __fc_p_random48_counter;
+ */
+extern unsigned short *seed48(unsigned short * /*[3]*/ seed16v);
+
+/*@ ensures random48_initialized: __fc_random48_init ≡ 1;
+ assigns __fc_random48_counter[0 .. 2], __fc_random48_init;
+ assigns __fc_random48_counter[0 .. 2] \from *(param + (0 .. 5));
+ assigns __fc_random48_init \from \nothing;
+ */
+extern void lcong48(unsigned short * /*[7]*/ param);
+
+/*@ requires random48_initialized: __fc_random48_init ≡ 1;
+ ensures result_range: \is_finite(\result) ∧ 0.0 ≤ \result < 1.0;
+ assigns __fc_random48_counter[0 .. 2], \result;
+ assigns __fc_random48_counter[0 .. 2]
+ \from __fc_random48_counter[0 .. 2];
+ assigns \result \from __fc_random48_counter[0 .. 2];
+ */
+extern double drand48(void);
+
+/*@ requires
+ initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
+ ensures result_range: \is_finite(\result) ∧ 0.0 ≤ \result < 1.0;
+ assigns __fc_random48_counter[0 .. 2], \result;
+ assigns __fc_random48_counter[0 .. 2]
+ \from __fc_random48_counter[0 .. 2];
+ assigns \result \from __fc_random48_counter[0 .. 2];
+ */
+extern double erand48(unsigned short * /*[3]*/ xsubi);
+
+/*@ requires random48_initialized: __fc_random48_init ≡ 1;
+ ensures result_range: 0 ≤ \result < 2147483648;
+ assigns __fc_random48_counter[0 .. 2], \result;
+ assigns __fc_random48_counter[0 .. 2]
+ \from __fc_random48_counter[0 .. 2];
+ assigns \result \from __fc_random48_counter[0 .. 2];
+ */
+extern long lrand48(void);
+
+/*@ requires
+ initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
+ ensures result_range: 0 ≤ \result < 2147483648;
+ assigns __fc_random48_counter[0 .. 2], \result;
+ assigns __fc_random48_counter[0 .. 2]
+ \from __fc_random48_counter[0 .. 2];
+ assigns \result \from __fc_random48_counter[0 .. 2];
+ */
+extern long nrand48(unsigned short * /*[3]*/ xsubi);
+
+/*@ requires random48_initialized: __fc_random48_init ≡ 1;
+ ensures result_range: -2147483648 ≤ \result < 2147483648;
+ assigns __fc_random48_counter[0 .. 2], \result;
+ assigns __fc_random48_counter[0 .. 2]
+ \from __fc_random48_counter[0 .. 2];
+ assigns \result \from __fc_random48_counter[0 .. 2];
+ */
+extern long mrand48(void);
+
+/*@ requires
+ initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2));
+ ensures result_range: -2147483648 ≤ \result < 2147483648;
+ assigns __fc_random48_counter[0 .. 2], \result;
+ assigns __fc_random48_counter[0 .. 2]
+ \from __fc_random48_counter[0 .. 2];
+ assigns \result \from __fc_random48_counter[0 .. 2];
+ */
+extern long jrand48(unsigned short * /*[3]*/ xsubi);
+
void *calloc(size_t nmemb, size_t size);
/*@ assigns __fc_heap_status, \result;
@@ -1960,7 +2161,7 @@ int glob(char const *pattern, int flags,
int __retres;
int tmp;
unsigned int tmp_0;
- char ***tmp_1;
+ char **tmp_1;
int tmp_4;
tmp = Frama_C_interval(0,10);
pglob->gl_pathc = (unsigned int)tmp;
@@ -1969,8 +2170,8 @@ int glob(char const *pattern, int flags,
size_t prev_len = (unsigned int)0;
if (flags & (1 << 5))
while (*(pglob->gl_pathv + (reserve_offs + prev_len))) prev_len += (size_t)1;
- if (flags & (1 << 5)) tmp_1 = & pglob->gl_pathv; else tmp_1 = (char ***)0;
- char **path = (char **)tmp_1;
+ if (flags & (1 << 5)) tmp_1 = pglob->gl_pathv; else tmp_1 = (char **)0;
+ char **path = tmp_1;
if (pglob->gl_pathc == (unsigned int)0)
if (flags & (1 << 4)) {
pglob->gl_pathv = (char **)realloc((void *)path,
@@ -2855,7 +3056,7 @@ float fabsf(float x)
int __finitef(float f)
{
int __retres;
- union __anonunion_u_5 u;
+ union __fc_u_finitef u;
unsigned short usExp;
u.f = f;
usExp = (unsigned short)((int)u.w[1] & 0x7F80);
@@ -2867,7 +3068,7 @@ int __finitef(float f)
int __finite(double d)
{
int __retres;
- union __anonunion_u_6 u;
+ union __fc_u_finite u;
unsigned short usExp;
u.d = d;
usExp = (unsigned short)((int)u.w[3] & 0x7F80);
@@ -2929,8 +3130,7 @@ 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_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);
@@ -3542,8 +3742,7 @@ extern char *strtok_r(char * __restrict s, char const * __restrict delim,
*/
extern char *strsep(char **stringp, char const *delim);
-extern char __fc_strerror[64];
-
+char __fc_strerror[64];
char * const __fc_p_strerror = __fc_strerror;
char *strerror(int errnum);
@@ -3615,16 +3814,9 @@ char *strdup(char const *s);
char *strndup(char const *s, size_t n);
-extern char __fc_strsignal[64];
-
+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);
+char *strsignal(int signum);
/*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
ensures
@@ -4699,7 +4891,38 @@ void *memcpy(void * __restrict dest, void const * __restrict src, size_t n)
complete behaviors not_separated_gt, not_separated_lt, separated;
disjoint behaviors not_separated_gt, not_separated_lt, separated;
*/
-static int memoverlap(char const *p, char const *q, size_t n);
+static int memoverlap(char const *p, char const *q, size_t n)
+{
+ int __retres;
+ uintptr_t p1 = (unsigned int)p;
+ uintptr_t p2 = (unsigned int)(p + n);
+ uintptr_t q1 = (unsigned int)q;
+ uintptr_t q2 = (unsigned int)(q + n);
+ if (p1 <= q1) {
+ if (p2 > q1) {
+ __retres = -1;
+ goto return_label;
+ }
+ else goto _LAND;
+ }
+ else {
+ _LAND: ;
+ if (q1 <= p1)
+ if (q2 > p1) {
+ __retres = 1;
+ goto return_label;
+ }
+ else {
+ __retres = 0;
+ goto return_label;
+ }
+ else {
+ __retres = 0;
+ goto return_label;
+ }
+ }
+ return_label: return __retres;
+}
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
@@ -5315,6 +5538,7 @@ char *strstr(char const *haystack, char const *needle)
return_label: return __retres;
}
+static int __fc_strerror_init;
/*@ ensures result_internal_str: \result ≡ __fc_p_strerror;
ensures result_nul_terminated: *(\result + 63) ≡ 0;
ensures result_valid_string: valid_read_string(\result);
@@ -5324,7 +5548,12 @@ char *strstr(char const *haystack, char const *needle)
char *strerror(int errnum)
{
char *__retres;
- __retres = (char *)"strerror message by Frama-C";
+ if (! __fc_strerror_init) {
+ Frama_C_make_unknown(__fc_strerror,(unsigned int)63);
+ __fc_strerror[63] = (char)0;
+ __fc_strerror_init = 1;
+ }
+ __retres = __fc_strerror;
return __retres;
}
@@ -5421,6 +5650,25 @@ char *strndup(char const *s, size_t n)
return_label: return __retres;
}
+static int __fc_strsignal_init;
+/*@ 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);
+ */
+char *strsignal(int signum)
+{
+ char *__retres;
+ if (! __fc_strsignal_init) {
+ Frama_C_make_unknown(__fc_strsignal,(unsigned int)63);
+ __fc_strsignal[63] = (char)0;
+ __fc_strsignal_init = 1;
+ }
+ __retres = __fc_strsignal;
+ return __retres;
+}
+
/*@ ghost unsigned int volatile __fc_time __attribute__((__FRAMA_C_MODEL__));
*/
/*@ assigns \result;
@@ -5953,89 +6201,6 @@ wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n)
return dest;
}
-/*@ assigns Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern void Frama_C_update_entropy(void);
-
-/*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from a, b, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-int Frama_C_nondet(int a, int b)
-{
- int tmp;
- Frama_C_update_entropy();
- if (Frama_C_entropy_source) tmp = a; else tmp = b;
- return tmp;
-}
-
-/*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from a, b, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-void *Frama_C_nondet_ptr(void *a, void *b)
-{
- void *tmp;
- Frama_C_update_entropy();
- if (Frama_C_entropy_source) tmp = a; else tmp = b;
- return tmp;
-}
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-int Frama_C_interval(int min, int max)
-{
- int r;
- int aux;
- Frama_C_update_entropy();
- aux = Frama_C_entropy_source;
- if (aux >= min)
- if (aux <= max) r = aux; else r = min;
- else r = min;
- return r;
-}
-
-/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
- requires order: min ≤ max;
- ensures
- result_bounded:
- \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-float Frama_C_float_interval(float min, float max)
-{
- float tmp;
- Frama_C_update_entropy();
- if (Frama_C_entropy_source) tmp = min; else tmp = max;
- return tmp;
-}
-
-/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
- requires order: min ≤ max;
- ensures
- result_bounded:
- \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-double Frama_C_double_interval(double min, double max)
-{
- double tmp;
- Frama_C_update_entropy();
- if (Frama_C_entropy_source) tmp = min; else tmp = max;
- return tmp;
-}
-
/*@ ghost extern int __fc_stack_status __attribute__((__FRAMA_C_MODEL__)); */
/*@ ensures allocation: \fresh{Old, Here}(\result,\old(size));
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 419fd8ae3f596924cb1de2e8e4a64b6ebe139bf0..93b9bdbbe40ccc606dcc5036e9f45a7a50c22751 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -8,6 +8,7 @@
\return(fgets) == 0 (auto)
\return(gets) == 0 (auto)
\return(popen) == 0 (auto)
+ \return(seed48) == 0 (auto)
\return(calloc) == 0 (auto)
\return(malloc) == 0 (auto)
\return(realloc) == 0 (auto)
diff --git a/tests/libc/oracle/runtime.res.oracle b/tests/libc/oracle/runtime.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle
index 1a7d60180779c859e8ad53b009b2d574aa0ec047..c6859df65a9866ee566f9514128b1249f697875a 100644
--- a/tests/libc/oracle/stdlib_c.0.res.oracle
+++ b/tests/libc/oracle/stdlib_c.0.res.oracle
@@ -78,10 +78,10 @@
(0..31/34359738367) to fit 0..63/34359738367
[eva] computing for function posix_memalign <- main.
Called from tests/libc/stdlib_c.c:37.
-[eva] share/libc/stdlib.c:197:
+[eva] share/libc/stdlib.c:196:
assertion 'alignment_is_a_suitable_power_of_two' got status valid.
-[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
-[eva] share/libc/stdlib.c:200: allocating variable __malloc_posix_memalign_l200
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199: allocating variable __malloc_posix_memalign_l199
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
[eva] computing for function free <- main.
@@ -93,9 +93,9 @@
[eva] Done for function free
[eva] computing for function posix_memalign <- main.
Called from tests/libc/stdlib_c.c:39.
-[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
-[eva] share/libc/stdlib.c:200:
- allocating variable __malloc_posix_memalign_l200_0
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199:
+ allocating variable __malloc_posix_memalign_l199_0
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
[eva] computing for function free <- main.
@@ -109,8 +109,8 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function posix_memalign:
__fc_heap_status ∈ [--..--]
- p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
- p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }} or UNINITIALIZED
+ p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l199[0] }}
+ p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l199_0[0] }} or UNINITIALIZED
__retres ∈ {0; 12}
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
@@ -120,8 +120,8 @@
q ∈ {{ NULL ; &__calloc_main_l21[0] }}
r ∈ {0}
s ∈ {{ NULL ; &__calloc_w_main_l32[0] }}
- p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
- p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }}
+ p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l199[0] }}
+ p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l199_0[0] }}
p_memal_res ∈ {0; 12}
p_memal_res2 ∈ {0; 12}
__retres ∈ {0}
diff --git a/tests/libc/oracle/stdlib_c.1.res.oracle b/tests/libc/oracle/stdlib_c.1.res.oracle
index 9021fc4d9d1690f4816abb040418148419280ab1..b87733adc52dff64e5e3c6b23eb532c56cd2a6c0 100644
--- a/tests/libc/oracle/stdlib_c.1.res.oracle
+++ b/tests/libc/oracle/stdlib_c.1.res.oracle
@@ -97,10 +97,10 @@
(0..31/34359738367) to fit 0..191/34359738367
[eva] computing for function posix_memalign <- main.
Called from tests/libc/stdlib_c.c:37.
-[eva] share/libc/stdlib.c:197:
+[eva] share/libc/stdlib.c:196:
assertion 'alignment_is_a_suitable_power_of_two' got status valid.
-[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
-[eva] share/libc/stdlib.c:200: allocating variable __malloc_posix_memalign_l200
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199: allocating variable __malloc_posix_memalign_l199
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
[eva] computing for function free <- main.
@@ -112,9 +112,9 @@
[eva] Done for function free
[eva] computing for function posix_memalign <- main.
Called from tests/libc/stdlib_c.c:39.
-[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
-[eva] share/libc/stdlib.c:200:
- allocating variable __malloc_posix_memalign_l200_0
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199:
+ allocating variable __malloc_posix_memalign_l199_0
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
[eva] computing for function free <- main.
@@ -128,8 +128,8 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function posix_memalign:
__fc_heap_status ∈ [--..--]
- p_al0 ∈ {{ &__malloc_posix_memalign_l200[0] }}
- p_al1 ∈ {{ &__malloc_posix_memalign_l200_0[0] }} or UNINITIALIZED
+ p_al0 ∈ {{ &__malloc_posix_memalign_l199[0] }}
+ p_al1 ∈ {{ &__malloc_posix_memalign_l199_0[0] }} or UNINITIALIZED
__retres ∈ {0}
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
@@ -139,8 +139,8 @@
q ∈ {{ NULL ; &__calloc_main_l21[0] }}
r ∈ {0}
s ∈ {{ NULL ; &__calloc_w_main_l32[0] }}
- p_al0 ∈ {{ &__malloc_posix_memalign_l200[0] }}
- p_al1 ∈ {{ &__malloc_posix_memalign_l200_0[0] }}
+ p_al0 ∈ {{ &__malloc_posix_memalign_l199[0] }}
+ p_al1 ∈ {{ &__malloc_posix_memalign_l199_0[0] }}
p_memal_res ∈ {0}
p_memal_res2 ∈ {0}
__retres ∈ {0}
diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle
index c70cca5c9ec4c02a371d875dd9c5978ed6f15c83..fbcbc924edbd2afa3d722765d61531a826a64d72 100644
--- a/tests/libc/oracle/stdlib_c.2.res.oracle
+++ b/tests/libc/oracle/stdlib_c.2.res.oracle
@@ -96,10 +96,10 @@
[eva] Done for function calloc
[eva] computing for function posix_memalign <- main.
Called from tests/libc/stdlib_c.c:37.
-[eva] share/libc/stdlib.c:197:
+[eva] share/libc/stdlib.c:196:
assertion 'alignment_is_a_suitable_power_of_two' got status valid.
-[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
-[eva] share/libc/stdlib.c:200: allocating variable __malloc_posix_memalign_l200
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199: allocating variable __malloc_posix_memalign_l199
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
[eva] computing for function free <- main.
@@ -111,9 +111,9 @@
[eva] Done for function free
[eva] computing for function posix_memalign <- main.
Called from tests/libc/stdlib_c.c:39.
-[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
-[eva] share/libc/stdlib.c:200:
- allocating variable __malloc_posix_memalign_l200_0
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199:
+ allocating variable __malloc_posix_memalign_l199_0
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
[eva] computing for function free <- main.
@@ -140,8 +140,8 @@
__malloc_w_calloc_l72_1[0..4294967291] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function posix_memalign:
__fc_heap_status ∈ [--..--]
- p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
- p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }} or UNINITIALIZED
+ p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l199[0] }}
+ p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l199_0[0] }} or UNINITIALIZED
__retres ∈ {0; 12}
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
@@ -151,8 +151,8 @@
q ∈ {{ NULL ; (int *)&__malloc_calloc_l72_0 }}
r ∈ {0}
s ∈ {{ NULL ; (int *)&__malloc_w_calloc_l72_1 }} or UNINITIALIZED
- p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
- p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }}
+ p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l199[0] }}
+ p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l199_0[0] }}
p_memal_res ∈ {0; 12}
p_memal_res2 ∈ {0; 12}
__retres ∈ {0}
diff --git a/tests/libc/oracle/stdlib_h.res.oracle b/tests/libc/oracle/stdlib_h.res.oracle
index f5a2bec1be1185a580dea18a6847f0b06bcaa48f..86789f173287f9d753f9e63b15b3dc140094ddfd 100644
--- a/tests/libc/oracle/stdlib_h.res.oracle
+++ b/tests/libc/oracle/stdlib_h.res.oracle
@@ -238,16 +238,94 @@
[eva] tests/libc/stdlib_h.c:82:
function mkstemp: precondition 'valid_template' got status valid.
[eva] Done for function mkstemp
+[eva] computing for function drand48 <- main.
+ Called from tests/libc/stdlib_h.c:86.
+[eva] using specification for function drand48
+[eva:alarm] tests/libc/stdlib_h.c:86: Warning:
+ function drand48: precondition 'random48_initialized' got status invalid.
+[eva] Done for function drand48
+[eva] computing for function lrand48 <- main.
+ Called from tests/libc/stdlib_h.c:90.
+[eva] using specification for function lrand48
+[eva:alarm] tests/libc/stdlib_h.c:90: Warning:
+ function lrand48: precondition 'random48_initialized' got status invalid.
+[eva] Done for function lrand48
+[eva] computing for function mrand48 <- main.
+ Called from tests/libc/stdlib_h.c:94.
+[eva] using specification for function mrand48
+[eva:alarm] tests/libc/stdlib_h.c:94: Warning:
+ function mrand48: precondition 'random48_initialized' got status invalid.
+[eva] Done for function mrand48
+[eva] computing for function erand48 <- main.
+ Called from tests/libc/stdlib_h.c:99.
+[eva] using specification for function erand48
+[eva:alarm] tests/libc/stdlib_h.c:99: Warning:
+ function erand48: precondition 'initialization,initialized_xsubi' got status invalid.
+[eva] Done for function erand48
+[eva] computing for function erand48 <- main.
+ Called from tests/libc/stdlib_h.c:104.
+[eva] tests/libc/stdlib_h.c:104:
+ function erand48: precondition 'initialization,initialized_xsubi' got status valid.
+[eva] Done for function erand48
+[eva] tests/libc/stdlib_h.c:105: assertion got status valid.
+[eva] computing for function jrand48 <- main.
+ Called from tests/libc/stdlib_h.c:106.
+[eva] using specification for function jrand48
+[eva] tests/libc/stdlib_h.c:106:
+ function jrand48: precondition 'initialization,initialized_xsubi' got status valid.
+[eva] Done for function jrand48
+[eva] tests/libc/stdlib_h.c:107: assertion got status valid.
+[eva] computing for function nrand48 <- main.
+ Called from tests/libc/stdlib_h.c:108.
+[eva] using specification for function nrand48
+[eva] tests/libc/stdlib_h.c:108:
+ function nrand48: precondition 'initialization,initialized_xsubi' got status valid.
+[eva] Done for function nrand48
+[eva] tests/libc/stdlib_h.c:109: assertion got status valid.
+[eva] computing for function srand48 <- main.
+ Called from tests/libc/stdlib_h.c:111.
+[eva] using specification for function srand48
+[eva] Done for function srand48
+[eva] computing for function seed48 <- main.
+ Called from tests/libc/stdlib_h.c:113.
+[eva] using specification for function seed48
+[eva] tests/libc/stdlib_h.c:113:
+ function seed48: precondition 'initialization,initialized_seed16v' got status valid.
+[eva] Done for function seed48
+[eva] computing for function lcong48 <- main.
+ Called from tests/libc/stdlib_h.c:115.
+[eva] using specification for function lcong48
+[eva] Done for function lcong48
+[eva] computing for function drand48 <- main.
+ Called from tests/libc/stdlib_h.c:117.
+[eva] tests/libc/stdlib_h.c:117:
+ function drand48: precondition 'random48_initialized' got status valid.
+[eva] Done for function drand48
+[eva] tests/libc/stdlib_h.c:118: assertion got status valid.
+[eva] computing for function mrand48 <- main.
+ Called from tests/libc/stdlib_h.c:119.
+[eva] tests/libc/stdlib_h.c:119:
+ function mrand48: precondition 'random48_initialized' got status valid.
+[eva] Done for function mrand48
+[eva] tests/libc/stdlib_h.c:120: assertion got status valid.
+[eva] computing for function lrand48 <- main.
+ Called from tests/libc/stdlib_h.c:121.
+[eva] tests/libc/stdlib_h.c:121:
+ function lrand48: precondition 'random48_initialized' got status valid.
+[eva] Done for function lrand48
+[eva] tests/libc/stdlib_h.c:122: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_random48_init ∈ {1}
+ __fc_random48_counter[0..2] ∈ [--..--]
base ∈ {0; 2; 36}
sl ∈ {{ "12 34 -56" }}
s ∈ {{ " 3.14 0x1.2p2" }}
pl ∈ {{ "12 34 -56" + [0..--] }}
q ∈ {{ " 3.14 0x1.2p2" + [0..--] }}
- l ∈ [--..--]
+ l ∈ [0..2147483647]
pll ∈ {{ "12 34 -56" + [0..--] }}
ll ∈ [--..--]
pul ∈ {{ "12 34 -56" + [0..--] }}
@@ -256,7 +334,7 @@
ull ∈ [--..--]
sd ∈ {{ " 3.14 0x1.2p2" }}
pd ∈ {{ " 3.14 0x1.2p2" + [0..--] }}
- d ∈ [-inf .. inf] ∪ {NaN}
+ d ∈ [-0. .. 1.]
pld ∈ {{ " 3.14 0x1.2p2" + [0..--] }}
ld ∈ [-inf .. inf] ∪ {NaN}
pf ∈ {{ " 3.14 0x1.2p2" + [0..--] }}
@@ -269,4 +347,16 @@
p ∈ {{ &ai[1] }}
tempFilename[0..9] ∈ [--..--]
r ∈ [-1..19]
+ xsubi[0..2] ∈ {42}
+ seed48v[0] ∈ {0}
+ [1] ∈ {4}
+ [2] ∈ {2}
+ res ∈ {{ &__fc_random48_counter[0] }}
+ param[0] ∈ {0}
+ [1] ∈ {4}
+ [2] ∈ {2}
+ [3] ∈ {0}
+ [4] ∈ {4}
+ [5] ∈ {2}
+ [6] ∈ {0}
__retres ∈ {0}
diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index d4cb7a56f166e0c86f7e6014fb885161748ef0e9..01a4e906ea181e9a16394341b6a59aff9005809a 100644
--- a/tests/libc/oracle/string_c.res.oracle
+++ b/tests/libc/oracle/string_c.res.oracle
@@ -90,8 +90,10 @@
[eva] tests/libc/string_c.c:42:
function memmove: precondition 'valid_src' got status valid.
[eva] computing for function memoverlap <- memmove <- test_memmove <- main.
- Called from share/libc/string.c:69.
-[eva] using specification for function memoverlap
+ Called from share/libc/string.c:77.
+[eva] share/libc/string.c:59:
+ function memoverlap, behavior not_separated_gt: postcondition 'result_p_after_q' got status valid.
+[eva] Recording results for memoverlap
[eva] Done for function memoverlap
[eva] share/libc/string.h:108:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
@@ -110,7 +112,10 @@
[eva] tests/libc/string_c.c:49:
function memmove: precondition 'valid_src' got status valid.
[eva] computing for function memoverlap <- memmove <- test_memmove <- main.
- Called from share/libc/string.c:69.
+ Called from share/libc/string.c:77.
+[eva] share/libc/string.c:55:
+ function memoverlap, behavior not_separated_lt: postcondition 'result_p_before_q' got status valid.
+[eva] Recording results for memoverlap
[eva] Done for function memoverlap
[eva] Recording results for memmove
[eva] Done for function memmove
@@ -122,7 +127,8 @@
[eva] tests/libc/string_c.c:52:
function memmove: precondition 'valid_src' got status valid.
[eva] computing for function memoverlap <- memmove <- test_memmove <- main.
- Called from share/libc/string.c:69.
+ Called from share/libc/string.c:77.
+[eva] Recording results for memoverlap
[eva] Done for function memoverlap
[eva] Recording results for memmove
[eva] Done for function memmove
@@ -134,7 +140,10 @@
[eva] tests/libc/string_c.c:56:
function memmove: precondition 'valid_src' got status valid.
[eva] computing for function memoverlap <- memmove <- test_memmove <- main.
- Called from share/libc/string.c:69.
+ Called from share/libc/string.c:77.
+[eva] share/libc/string.c:51:
+ function memoverlap, behavior separated: postcondition 'result_no_overlap' got status valid.
+[eva] Recording results for memoverlap
[eva] Done for function memoverlap
[eva] Recording results for memmove
[eva] Done for function memmove
@@ -480,8 +489,8 @@
[eva] tests/libc/string_c.c:124:
function strcat: precondition 'room_string' got status valid.
[eva] computing for function strlen <- strcat <- test_strcat <- main.
- Called from share/libc/string.c:174.
-[eva] share/libc/string.c:174:
+ Called from share/libc/string.c:182.
+[eva] share/libc/string.c:182:
function strlen: precondition 'valid_string_s' got status valid.
[eva] Recording results for strlen
[eva] Done for function strlen
@@ -506,7 +515,7 @@
[eva] tests/libc/string_c.c:132:
function strcat: precondition 'room_string' got status valid.
[eva] computing for function strlen <- strcat <- test_strcat <- main.
- Called from share/libc/string.c:174.
+ Called from share/libc/string.c:182.
[eva] Recording results for strlen
[eva] Done for function strlen
[eva] Recording results for strcat
@@ -521,7 +530,7 @@
[eva] tests/libc/string_c.c:134:
function strcat: precondition 'room_string' got status valid.
[eva] computing for function strlen <- strcat <- test_strcat <- main.
- Called from share/libc/string.c:174.
+ Called from share/libc/string.c:182.
[eva] Recording results for strlen
[eva] Done for function strlen
[eva] Recording results for strcat
@@ -534,7 +543,7 @@
function strcat: precondition 'valid_string_dest' got status valid.
[eva] tests/libc/string_c.c:135:
function strcat: precondition 'room_string' got status valid.
-[eva] share/libc/string.c:174: Reusing old results for call to strlen
+[eva] share/libc/string.c:182: Reusing old results for call to strlen
[eva] Recording results for strcat
[eva] Done for function strcat
[eva] tests/libc/string_c.c:136: assertion got status valid.
@@ -698,8 +707,8 @@
[eva] tests/libc/string_c.c:214:
function strrchr: precondition 'valid_string_s' got status valid.
[eva] computing for function strlen <- strrchr <- test_strrchr <- main.
- Called from share/libc/string.c:229.
-[eva] share/libc/string.c:229:
+ Called from share/libc/string.c:237.
+[eva] share/libc/string.c:237:
function strlen: precondition 'valid_string_s' got status valid.
[eva] Recording results for strlen
[eva] Done for function strlen
@@ -718,7 +727,7 @@
Called from tests/libc/string_c.c:216.
[eva] tests/libc/string_c.c:216:
function strrchr: precondition 'valid_string_s' got status valid.
-[eva] share/libc/string.c:229: Reusing old results for call to strlen
+[eva] share/libc/string.c:237: Reusing old results for call to strlen
[eva] share/libc/string.h:184:
function strrchr, behavior not_found: postcondition 'result_null' got status valid.
[eva] Recording results for strrchr
@@ -728,7 +737,7 @@
Called from tests/libc/string_c.c:218.
[eva] tests/libc/string_c.c:218:
function strrchr: precondition 'valid_string_s' got status valid.
-[eva] share/libc/string.c:229: Reusing old results for call to strlen
+[eva] share/libc/string.c:237: Reusing old results for call to strlen
[eva] Recording results for strrchr
[eva] Done for function strrchr
[eva] tests/libc/string_c.c:219: assertion got status valid.
@@ -736,7 +745,7 @@
Called from tests/libc/string_c.c:220.
[eva] tests/libc/string_c.c:220:
function strrchr: precondition 'valid_string_s' got status valid.
-[eva] share/libc/string.c:229: Reusing old results for call to strlen
+[eva] share/libc/string.c:237: Reusing old results for call to strlen
[eva] Recording results for strrchr
[eva] Done for function strrchr
[eva] tests/libc/string_c.c:221: assertion got status valid.
@@ -964,6 +973,12 @@
[3] ∈ {0; 18; 108}
[4] ∈ {0; 111}
[5] ∈ {0}
+[eva:final-states] Values at end of function memoverlap:
+ p1 ∈ {{ (unsigned int)&buf{[0], [2], [3]} }}
+ p2 ∈ {{ (unsigned int)&buf{[4], [6]} }}
+ q1 ∈ {{ (unsigned int)&buf{[0], [2]} }}
+ q2 ∈ {{ (unsigned int)&buf{[3], [4], [6]} }}
+ __retres ∈ {-1; 0; 1}
[eva:final-states] Values at end of function memmove:
s ∈ {{ &buf{[0], [2]} }}
d ∈ {{ &buf{[0], [2], [3]} }}
diff --git a/tests/libc/oracle/string_c_generic.res.oracle b/tests/libc/oracle/string_c_generic.res.oracle
index 79cc74ecd4c8d7931621e3703168d0584d862705..23daf7cb9257fd1bdee878600fe317860cfafaaa 100644
--- a/tests/libc/oracle/string_c_generic.res.oracle
+++ b/tests/libc/oracle/string_c_generic.res.oracle
@@ -160,7 +160,7 @@
function strncpy: precondition 'room_nstring' got status valid.
[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.c:220: starting to merge loop iterations
[eva] share/libc/string.h:363:
function strncpy: postcondition 'result_ptr' got status valid.
[eva] share/libc/string.h:364:
@@ -211,7 +211,7 @@
function strncmp: precondition 'valid_string_s1' got status valid.
[eva] tests/libc/string_c_generic.c:82:
function strncmp: precondition 'valid_string_s2' got status valid.
-[eva] share/libc/string.c:130: starting to merge loop iterations
+[eva] share/libc/string.c:138: starting to merge loop iterations
[eva] share/libc/string.h:147:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strncmp
[eva:alarm] share/libc/string.h:147: Warning:
@@ -245,8 +245,8 @@
[eva] tests/libc/string_c_generic.c:86:
function strncat, behavior partial: precondition 'room_string' got status valid.
[eva] computing for function strlen <- strncat <- main.
- Called from share/libc/string.c:185.
-[eva] share/libc/string.c:185:
+ Called from share/libc/string.c:193.
+[eva] share/libc/string.c:193:
function strlen: precondition 'valid_string_s' got status valid.
[eva] share/libc/string.h:127:
function strlen: postcondition 'acsl_c_equiv' got status valid.
@@ -307,8 +307,8 @@
[eva] tests/libc/string_c_generic.c:93:
function strrchr: precondition 'valid_string_s' got status valid.
[eva] computing for function strlen <- strrchr <- main.
- Called from share/libc/string.c:229.
-[eva] share/libc/string.c:229:
+ Called from share/libc/string.c:237.
+[eva] share/libc/string.c:237:
function strlen: precondition 'valid_string_s' got status valid.
[eva] Recording results for strlen
[eva] Done for function strlen
@@ -326,8 +326,8 @@
Called from tests/libc/string_c_generic.c:94.
[eva] tests/libc/string_c_generic.c:94:
function strrchr: precondition 'valid_string_s' got status valid.
-[eva] share/libc/string.c:229: Reusing old results for call to strlen
-[eva] share/libc/string.c:229: starting to merge loop iterations
+[eva] share/libc/string.c:237: Reusing old results for call to strlen
+[eva] share/libc/string.c:237: starting to merge loop iterations
[eva] share/libc/string.h:184:
function strrchr, behavior not_found: postcondition 'result_null' got status valid.
[eva] Recording results for strrchr
diff --git a/tests/libc/oracle/string_c_strstr.res.oracle b/tests/libc/oracle/string_c_strstr.res.oracle
index f9d41091bb490290c1d7a23223a429da21ede466..6009523b88343d2be3364eb0953243acb941f53a 100644
--- a/tests/libc/oracle/string_c_strstr.res.oracle
+++ b/tests/libc/oracle/string_c_strstr.res.oracle
@@ -68,7 +68,7 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_c_strstr.c:59:
function strstr: precondition 'valid_string_needle' got status valid.
-[eva] share/libc/string.c:258: starting to merge loop iterations
+[eva] share/libc/string.c:266: starting to merge loop iterations
[eva] Recording results for strstr
[eva] Done for function strstr
[eva] computing for function strstr <- main.
diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c
new file mode 100644
index 0000000000000000000000000000000000000000..6fd7bf646ade2d79c3e247e9a0910ae63d0b253f
--- /dev/null
+++ b/tests/libc/runtime.c
@@ -0,0 +1,9 @@
+/* run.config*
+ COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
+ CMD: gcc -D__FC_MACHDEP_X86_64 share/libc/__fc_runtime.c -Wno-attributes
+ OPT:
+ */
+
+int main() {
+ return 0;
+}
diff --git a/tests/libc/stdlib_h.c b/tests/libc/stdlib_h.c
index dec6260f59fd24e6aed419f1af823ab1527d2fd6..ea1b69046d2c3e6452c948df14cccd81439d8ac2 100644
--- a/tests/libc/stdlib_h.c
+++ b/tests/libc/stdlib_h.c
@@ -81,5 +81,45 @@ int main() {
char tempFilename[] = "blaXXXXXX";
int r = mkstemp(tempFilename);
+ if (nondet) {
+ // should fail: seed not initialized
+ drand48();
+ }
+ if (nondet) {
+ // should fail: seed not initialized
+ lrand48();
+ }
+ if (nondet) {
+ // should fail: seed not initialized
+ mrand48();
+ }
+ unsigned short xsubi[3];
+ if (nondet) {
+ // should fail: xsubi
+ erand48(xsubi);
+ }
+ xsubi[0] = 42;
+ xsubi[1] = 42;
+ xsubi[2] = 42;
+ d = erand48(xsubi);
+ //@ assert 0.0 <= d < 1.0;
+ l = jrand48(xsubi);
+ //@ assert -2147483648 <= l < 2147483648;
+ l = nrand48(xsubi);
+ //@ assert 0 <= l < 2147483648;
+
+ srand48(42);
+ unsigned short seed48v[3] = {0, 4, 2};
+ unsigned short *res = seed48(seed48v);
+ unsigned short param[7] = {0, 4, 2, 0, 4, 2, 0};
+ lcong48(param);
+
+ d = drand48();
+ //@ assert 0.0 <= d < 1.0;
+ l = mrand48();
+ //@ assert -2147483648 <= l < 2147483648;
+ l = lrand48();
+ //@ assert 0 <= l < 2147483648;
+
return 0;
}
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index 289e246d8ac73d48cb1a4111f42a59e03092aa8b..18dd8eea6bdd67932e7fc01d51851c6e6edc9444 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/tests/value/oracle/gauges.res.oracle
@@ -364,6 +364,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -421,6 +424,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -477,6 +483,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -533,6 +542,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -595,6 +607,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
@@ -653,6 +668,9 @@
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
__fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
[1] ∈ {{ NULL ; &S_1___fc_env[0] }}
[2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}