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/string.c b/share/libc/string.c
index 06662b1f297c20820c33eed85b77ad1febdcc9da..99e54e162ad796fc903922f4068d0556d1996e82 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)
{
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/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 b43c270eb5cf1b69247d75e24bb7b757a5ae5007..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 93)
+ 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 609d7872065b726dbf020b1d6312daebcd238e14..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 (384)
+ 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);
@@ -108,15 +109,15 @@
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); 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);
+ 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);
pthread_mutex_destroy (0 call); pthread_mutex_init (0 call);
pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call); putc (0 call);
putc_unlocked (0 call); putchar (0 call); putchar_unlocked (0 call);
@@ -139,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)
==========================
@@ -169,18 +169,18 @@
Global metrics
==============
- Sloc = 1026
- Decision point = 195
- Global variables = 66
- If = 186
- Loop = 42
- Goto = 84
- Assignment = 415
- Exit point = 76
- Function = 460
- 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"
@@ -217,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 14d31d680243c64fde8938062020691d49bade74..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;
@@ -1677,8 +1803,7 @@ extern long random(void);
extern void srandom(unsigned int seed);
int __fc_random48_init __attribute__((__FRAMA_C_MODEL__));
-extern unsigned short __fc_random48_counter[3] __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;
@@ -2036,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;
@@ -2045,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,
@@ -2931,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);
@@ -2943,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);
@@ -3005,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);
@@ -3618,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);
@@ -3691,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
@@ -4775,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);
@@ -5391,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);
@@ -5400,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;
}
@@ -5497,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;
@@ -6029,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/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/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;
+}