From 5d24aacd07e9c624ef31362c9906a51e96131524 Mon Sep 17 00:00:00 2001
From: Dario Pinto <dario.pinto@cea.fr>
Date: Mon, 29 Jun 2020 16:00:34 +0200
Subject: [PATCH] [Libc] add stub for realpath
---
share/libc/stdlib.c | 31 ++
share/libc/stdlib.h | 3 +
.../tests/arith/oracle_ci/gen_functions.c | 144 +++++-----
.../tests/arith/oracle_ci/gen_functions_rec.c | 140 ++++-----
.../tests/gmp-only/oracle_ci/gen_functions.c | 172 +++++------
.../memory/oracle_ci/gen_hidden_malloc.c | 11 +-
.../memory/oracle_ci/hidden_malloc.res.oracle | 4 +-
.../oracle_dev/hidden_malloc.res.oracle | 2 -
.../tests/temporal/oracle_ci/gen_t_fun_lib.c | 27 +-
.../temporal/oracle_ci/t_fun_lib.res.oracle | 6 -
.../temporal/oracle_dev/t_fun_lib.res.oracle | 2 -
src/plugins/value/utils/library_functions.ml | 3 +-
tests/libc/oracle/fc_libc.0.res.oracle | 43 +--
tests/libc/oracle/fc_libc.1.res.oracle | 50 ++++
tests/libc/oracle/stdlib_c.0.res.oracle | 237 +++++++++++----
tests/libc/oracle/stdlib_c.1.res.oracle | 271 +++++++++++++-----
tests/libc/oracle/stdlib_c.2.res.oracle | 119 ++++++--
tests/libc/stdlib_c.c | 14 +
18 files changed, 830 insertions(+), 449 deletions(-)
diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index c74ec8681e7..0bd44d02100 100644
--- a/share/libc/stdlib.c
+++ b/share/libc/stdlib.c
@@ -201,4 +201,35 @@ int posix_memalign(void **memptr, size_t alignment, size_t size) {
return 0;
}
+char *realpath(const char *restrict file_name, char *restrict resolved_name)
+{
+ if (!file_name) {
+ errno = EINVAL;
+ return NULL;
+ }
+ // do path search
+
+ // simulate possible errors
+ switch (Frama_C_interval(0, 6)) {
+ case 0: errno = EACCES; return NULL;
+ case 1: errno = EIO; return NULL;
+ case 2: errno = ELOOP; return NULL;
+ case 3: errno = ENAMETOOLONG; return NULL;
+ case 4: errno = ENOENT; return NULL;
+ case 5: errno = ENOTDIR; return NULL;
+ default: break;
+ }
+ int realpath_len = Frama_C_interval(1, PATH_MAX);
+ if (!resolved_name) {
+ resolved_name = malloc(PATH_MAX);
+ if (!resolved_name) {
+ errno = ENOMEM;
+ return NULL;
+ }
+ }
+ Frama_C_make_unknown(resolved_name, realpath_len);
+ resolved_name[realpath_len-1] = '\0';
+ return resolved_name;
+}
+
__POP_FC_STDLIB
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 1c52b42c4b1..e5e7a3e33e4 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -699,6 +699,9 @@ extern int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
extern int mkstemp(char *templat);
+extern char *realpath(const char *restrict file_name,
+ char *restrict resolved_name);
+
__END_DECLS
__POP_FC_STDLIB
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
index 80def032755..a1227023b92 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
@@ -232,78 +232,6 @@ void __gen_e_acsl_k(int x)
return;
}
-long __gen_e_acsl_f1(int x, int y)
-{
- long __retres = x + (long)y;
- return __retres;
-}
-
-void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
- __e_acsl_mpz_struct * y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_3;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(y));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_clear(__gen_e_acsl_x_3);
- __gmpz_clear(__gen_e_acsl_add_3);
- return;
-}
-
-void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
- __e_acsl_mpz_struct * y)
-{
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(x),
- (__e_acsl_mpz_struct const *)(y));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_clear(__gen_e_acsl_add_4);
- return;
-}
-
-int __gen_e_acsl_h_char(int c)
-{
- return c;
-}
-
-int __gen_e_acsl_h_short(int s)
-{
- return s;
-}
-
-int __gen_e_acsl_g_hidden(int x)
-{
- return x;
-}
-
-double __gen_e_acsl_f2(double x)
-{
- __e_acsl_mpq_t __gen_e_acsl__8;
- __e_acsl_mpq_t __gen_e_acsl__9;
- __e_acsl_mpq_t __gen_e_acsl_div;
- double __gen_e_acsl__10;
- __gmpq_init(__gen_e_acsl__8);
- __gmpq_set_str(__gen_e_acsl__8,"1",10);
- __gmpq_init(__gen_e_acsl__9);
- __gmpq_set_d(__gen_e_acsl__9,x);
- __gmpq_init(__gen_e_acsl_div);
- __gmpq_div(__gen_e_acsl_div,(__e_acsl_mpq_struct const *)(__gen_e_acsl__8),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__9));
- __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
- __gmpq_clear(__gen_e_acsl__8);
- __gmpq_clear(__gen_e_acsl__9);
- __gmpq_clear(__gen_e_acsl_div);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
- return __gen_e_acsl__10;
-}
-
int __gen_e_acsl_g(int x)
{
int __gen_e_acsl_g_hidden_2;
@@ -384,4 +312,76 @@ int __gen_e_acsl_k_pred(int x)
return __retres;
}
+long __gen_e_acsl_f1(int x, int y)
+{
+ long __retres = x + (long)y;
+ return __retres;
+}
+
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+ __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gmpz_clear(__gen_e_acsl_x_3);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ return;
+}
+
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(x),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_clear(__gen_e_acsl_add_4);
+ return;
+}
+
+int __gen_e_acsl_h_char(int c)
+{
+ return c;
+}
+
+int __gen_e_acsl_h_short(int s)
+{
+ return s;
+}
+
+int __gen_e_acsl_g_hidden(int x)
+{
+ return x;
+}
+
+double __gen_e_acsl_f2(double x)
+{
+ __e_acsl_mpq_t __gen_e_acsl__8;
+ __e_acsl_mpq_t __gen_e_acsl__9;
+ __e_acsl_mpq_t __gen_e_acsl_div;
+ double __gen_e_acsl__10;
+ __gmpq_init(__gen_e_acsl__8);
+ __gmpq_set_str(__gen_e_acsl__8,"1",10);
+ __gmpq_init(__gen_e_acsl__9);
+ __gmpq_set_d(__gen_e_acsl__9,x);
+ __gmpq_init(__gen_e_acsl_div);
+ __gmpq_div(__gen_e_acsl_div,(__e_acsl_mpq_struct const *)(__gen_e_acsl__8),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__9));
+ __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gmpq_clear(__gen_e_acsl__8);
+ __gmpq_clear(__gen_e_acsl__9);
+ __gmpq_clear(__gen_e_acsl_div);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
+ return __gen_e_acsl__10;
+}
+
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
index df6e9ac544b..b9015c95933 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
@@ -105,76 +105,6 @@ int main(void)
return __retres;
}
-int __gen_e_acsl_f3(int n)
-{
- int __gen_e_acsl_if_6;
- if (n > 0) {
- int __gen_e_acsl_g_2;
- int __gen_e_acsl_f3_5;
- __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
- __gen_e_acsl_f3_5 = __gen_e_acsl_f3_2(n - 1L);
- __gen_e_acsl_if_6 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
- }
- else {
- int __gen_e_acsl_g_8;
- __gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
- __gen_e_acsl_if_6 = __gen_e_acsl_g_8;
- }
- return __gen_e_acsl_if_6;
-}
-
-int __gen_e_acsl_f3_2(long n)
-{
- int __gen_e_acsl_if_5;
- if (n > 0L) {
- int __gen_e_acsl_g_4;
- int __gen_e_acsl_f3_4;
- __gen_e_acsl_g_4 = __gen_e_acsl_g((int)n);
- __gen_e_acsl_f3_4 = __gen_e_acsl_f3_2(n - 1L);
- __gen_e_acsl_if_5 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
- }
- else {
- int __gen_e_acsl_g_6;
- __gen_e_acsl_g_6 = __gen_e_acsl_g_5(n + 1L);
- __gen_e_acsl_if_5 = __gen_e_acsl_g_6;
- }
- return __gen_e_acsl_if_5;
-}
-
-unsigned long __gen_e_acsl_f4(int n)
-{
- unsigned long __gen_e_acsl_if_10;
- if (n < 100) {
- unsigned long __gen_e_acsl_f4_5;
- __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_10 = __gen_e_acsl_f4_5;
- }
- else {
- unsigned long __gen_e_acsl_if_9;
- if ((long)n < 9223372036854775807L) __gen_e_acsl_if_9 = 9223372036854775807UL;
- else __gen_e_acsl_if_9 = 6UL;
- __gen_e_acsl_if_10 = __gen_e_acsl_if_9;
- }
- return __gen_e_acsl_if_10;
-}
-
-unsigned long __gen_e_acsl_f4_2(long n)
-{
- unsigned long __gen_e_acsl_if_8;
- if (n < 100L) {
- unsigned long __gen_e_acsl_f4_4;
- __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_8 = __gen_e_acsl_f4_4;
- }
- else {
- unsigned long __gen_e_acsl_if_7;
- if (n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
- else __gen_e_acsl_if_7 = 6UL;
- __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
- }
- return __gen_e_acsl_if_8;
-}
-
void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
{
__e_acsl_mpz_t __gen_e_acsl_if_2;
@@ -317,4 +247,74 @@ int __gen_e_acsl_g_5(long n)
return __retres;
}
+int __gen_e_acsl_f3(int n)
+{
+ int __gen_e_acsl_if_6;
+ if (n > 0) {
+ int __gen_e_acsl_g_2;
+ int __gen_e_acsl_f3_5;
+ __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
+ __gen_e_acsl_f3_5 = __gen_e_acsl_f3_2(n - 1L);
+ __gen_e_acsl_if_6 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_8;
+ __gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
+ __gen_e_acsl_if_6 = __gen_e_acsl_g_8;
+ }
+ return __gen_e_acsl_if_6;
+}
+
+int __gen_e_acsl_f3_2(long n)
+{
+ int __gen_e_acsl_if_5;
+ if (n > 0L) {
+ int __gen_e_acsl_g_4;
+ int __gen_e_acsl_f3_4;
+ __gen_e_acsl_g_4 = __gen_e_acsl_g((int)n);
+ __gen_e_acsl_f3_4 = __gen_e_acsl_f3_2(n - 1L);
+ __gen_e_acsl_if_5 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_6;
+ __gen_e_acsl_g_6 = __gen_e_acsl_g_5(n + 1L);
+ __gen_e_acsl_if_5 = __gen_e_acsl_g_6;
+ }
+ return __gen_e_acsl_if_5;
+}
+
+unsigned long __gen_e_acsl_f4(int n)
+{
+ unsigned long __gen_e_acsl_if_10;
+ if (n < 100) {
+ unsigned long __gen_e_acsl_f4_5;
+ __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_10 = __gen_e_acsl_f4_5;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_9;
+ if ((long)n < 9223372036854775807L) __gen_e_acsl_if_9 = 9223372036854775807UL;
+ else __gen_e_acsl_if_9 = 6UL;
+ __gen_e_acsl_if_10 = __gen_e_acsl_if_9;
+ }
+ return __gen_e_acsl_if_10;
+}
+
+unsigned long __gen_e_acsl_f4_2(long n)
+{
+ unsigned long __gen_e_acsl_if_8;
+ if (n < 100L) {
+ unsigned long __gen_e_acsl_f4_4;
+ __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_8 = __gen_e_acsl_f4_4;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_7;
+ if (n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
+ else __gen_e_acsl_if_7 = 6UL;
+ __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
+ }
+ return __gen_e_acsl_if_8;
+}
+
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index 585642b7869..0050e6edc3b 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
@@ -288,92 +288,6 @@ void __gen_e_acsl_k(int x)
return;
}
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __e_acsl_mpz_t __gen_e_acsl_y_3;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_clear(__gen_e_acsl_x_4);
- __gmpz_clear(__gen_e_acsl_y_3);
- __gmpz_clear(__gen_e_acsl_add_4);
- return;
-}
-
-void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
- __e_acsl_mpz_struct * y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_5;
- __e_acsl_mpz_t __gen_e_acsl_add_5;
- __gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
- __gmpz_init(__gen_e_acsl_add_5);
- __gmpz_add(__gen_e_acsl_add_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
- (__e_acsl_mpz_struct const *)(y));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
- __gmpz_clear(__gen_e_acsl_x_5);
- __gmpz_clear(__gen_e_acsl_add_5);
- return;
-}
-
-void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
- __e_acsl_mpz_struct * y)
-{
- __e_acsl_mpz_t __gen_e_acsl_add_6;
- __gmpz_init(__gen_e_acsl_add_6);
- __gmpz_add(__gen_e_acsl_add_6,(__e_acsl_mpz_struct const *)(x),
- (__e_acsl_mpz_struct const *)(y));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
- __gmpz_clear(__gen_e_acsl_add_6);
- return;
-}
-
-int __gen_e_acsl_h_char(int c)
-{
- return c;
-}
-
-int __gen_e_acsl_h_short(int s)
-{
- return s;
-}
-
-int __gen_e_acsl_g_hidden(int x)
-{
- return x;
-}
-
-double __gen_e_acsl_f2(double x)
-{
- __e_acsl_mpq_t __gen_e_acsl__13;
- __e_acsl_mpq_t __gen_e_acsl__14;
- __e_acsl_mpq_t __gen_e_acsl_div;
- double __gen_e_acsl_cast;
- __gmpq_init(__gen_e_acsl__13);
- __gmpq_set_str(__gen_e_acsl__13,"1",10);
- __gmpq_init(__gen_e_acsl__14);
- __gmpq_set_d(__gen_e_acsl__14,x);
- __gmpq_init(__gen_e_acsl_div);
- __gmpq_div(__gen_e_acsl_div,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
- __gen_e_acsl_cast = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
- __gmpq_clear(__gen_e_acsl__13);
- __gmpq_clear(__gen_e_acsl__14);
- __gmpq_clear(__gen_e_acsl_div);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast); */
- return __gen_e_acsl_cast;
-}
-
int __gen_e_acsl_g(int x)
{
int __gen_e_acsl_g_hidden_2;
@@ -488,4 +402,90 @@ int __gen_e_acsl_k_pred(int x)
return __retres;
}
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __e_acsl_mpz_t __gen_e_acsl_y_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_clear(__gen_e_acsl_x_4);
+ __gmpz_clear(__gen_e_acsl_y_3);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ return;
+}
+
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+ __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_5;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
+ __gmpz_clear(__gen_e_acsl_x_5);
+ __gmpz_clear(__gen_e_acsl_add_5);
+ return;
+}
+
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,(__e_acsl_mpz_struct const *)(x),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
+ __gmpz_clear(__gen_e_acsl_add_6);
+ return;
+}
+
+int __gen_e_acsl_h_char(int c)
+{
+ return c;
+}
+
+int __gen_e_acsl_h_short(int s)
+{
+ return s;
+}
+
+int __gen_e_acsl_g_hidden(int x)
+{
+ return x;
+}
+
+double __gen_e_acsl_f2(double x)
+{
+ __e_acsl_mpq_t __gen_e_acsl__13;
+ __e_acsl_mpq_t __gen_e_acsl__14;
+ __e_acsl_mpq_t __gen_e_acsl_div;
+ double __gen_e_acsl_cast;
+ __gmpq_init(__gen_e_acsl__13);
+ __gmpq_set_str(__gen_e_acsl__13,"1",10);
+ __gmpq_init(__gen_e_acsl__14);
+ __gmpq_set_d(__gen_e_acsl__14,x);
+ __gmpq_init(__gen_e_acsl_div);
+ __gmpq_div(__gen_e_acsl_div,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
+ __gen_e_acsl_cast = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gmpq_clear(__gen_e_acsl__13);
+ __gmpq_clear(__gen_e_acsl__14);
+ __gmpq_clear(__gen_e_acsl_div);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast); */
+ return __gen_e_acsl_cast;
+}
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c
index 8fa1b3c59f4..ef47698bb6f 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c
@@ -2,13 +2,6 @@
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string;
-/*@ assigns \result, *((char *)x_1 + (0 ..));
- assigns \result \from *(x_0 + (0 ..)), *((char *)x_1 + (0 ..));
- assigns *((char *)x_1 + (0 ..))
- \from *(x_0 + (0 ..)), *((char *)x_1 + (0 ..));
- */
-extern int ( /* missing proto */ realpath)(char const *x_0, void *x_1);
-
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
@@ -25,11 +18,9 @@ void __e_acsl_globals_init(void)
int main(int argc, char const **argv)
{
int __retres;
- int tmp;
__e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
__e_acsl_globals_init();
- tmp = realpath(__gen_e_acsl_literal_string,(void *)0);
- char *cwd = (char *)tmp;
+ char *cwd = realpath(__gen_e_acsl_literal_string,(char *)0);
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
index cecec801d91..9ee3cfb6095 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
@@ -1,9 +1,7 @@
-[kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:11: Warning:
- Calling undeclared function realpath. Old style K&R code?
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/memory/hidden_malloc.c:11: Warning:
Neither code nor specification for function realpath, generating default assigns from the prototype
[eva:invalid-assigns] tests/memory/hidden_malloc.c:11:
- Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)).
+ Completely invalid destination for assigns clause *(resolved_name + (0 ..)).
Ignoring.
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle
index dd729b732a8..c1d15293253 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle
@@ -1,3 +1 @@
[kernel] Parsing tests/memory/hidden_malloc.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:11: Warning:
- Calling undeclared function realpath. Old style K&R code?
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c
index 6ec8b81a0e7..33388accb3a 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c
@@ -2,13 +2,6 @@
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string;
-/*@ assigns \result, *(x_0 + (0 ..)), *(x_1 + (0 ..));
- assigns \result \from *(x_0 + (0 ..)), *(x_1 + (0 ..));
- assigns *(x_0 + (0 ..)) \from *(x_0 + (0 ..)), *(x_1 + (0 ..));
- assigns *(x_1 + (0 ..)) \from *(x_0 + (0 ..)), *(x_1 + (0 ..));
- */
-extern int ( /* missing proto */ realpath)(char *x_0, char *x_1);
-
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
@@ -25,12 +18,8 @@ void __e_acsl_globals_init(void)
int main(void)
{
int __retres;
- int tmp_0;
- int tmp_1;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& tmp_1),(size_t)4);
- __e_acsl_store_block((void *)(& tmp_0),(size_t)4);
char *c = (char *)__gen_e_acsl_literal_string;
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
@@ -80,23 +69,19 @@ int main(void)
16);
}
/*@ assert \valid(q) ∧ \valid(p); */ ;
- __e_acsl_full_init((void *)(& tmp_0));
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(& q),1U);
- tmp_0 = realpath(c,q);
- char *path = (char *)tmp_0;
- __e_acsl_temporal_store_nblock((void *)(& path),(void *)((char *)tmp_0));
+ char *path = realpath((char const *)c,q);
+ __e_acsl_temporal_store_nblock((void *)(& path),(void *)*(& path));
__e_acsl_store_block((void *)(& path),(size_t)8);
__e_acsl_full_init((void *)(& path));
- __e_acsl_full_init((void *)(& tmp_1));
+ __e_acsl_full_init((void *)(& path));
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(& q),1U);
- tmp_1 = realpath(c,q);
- __e_acsl_full_init((void *)(& path));
- __e_acsl_temporal_store_nblock((void *)(& path),(void *)((char *)tmp_1));
- path = (char *)tmp_1;
+ path = realpath((char const *)c,q);
+ __e_acsl_temporal_store_nblock((void *)(& path),(void *)*(& path));
{
int __gen_e_acsl_initialized_3;
int __gen_e_acsl_and_4;
@@ -155,8 +140,6 @@ int main(void)
}
/*@ assert ¬\valid(p) ∧ ¬\valid(path); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(& tmp_1));
- __e_acsl_delete_block((void *)(& tmp_0));
__e_acsl_delete_block((void *)(& path));
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& p));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_lib.res.oracle
index 57c3a74f84b..9cd605d192b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_lib.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_lib.res.oracle
@@ -1,12 +1,6 @@
-[kernel:typing:implicit-function-declaration] tests/temporal/t_fun_lib.c:20: Warning:
- Calling undeclared function realpath. Old style K&R code?
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/temporal/t_fun_lib.c:20: Warning:
Neither code nor specification for function realpath, generating default assigns from the prototype
-[eva:invalid-assigns] tests/temporal/t_fun_lib.c:20:
- Completely invalid destination for assigns clause *(x_0 + (0 ..)). Ignoring.
-[eva:invalid-assigns] tests/temporal/t_fun_lib.c:21:
- Completely invalid destination for assigns clause *(x_0 + (0 ..)). Ignoring.
[eva:alarm] tests/temporal/t_fun_lib.c:23: Warning:
function __e_acsl_assert: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle
index 5d97f1e4656..1928ecb96d0 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle
@@ -1,3 +1 @@
[kernel] Parsing tests/temporal/t_fun_lib.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/temporal/t_fun_lib.c:20: Warning:
- Calling undeclared function realpath. Old style K&R code?
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index e3c5407e4b4..7e5ff93a018 100644
--- a/src/plugins/value/utils/library_functions.ml
+++ b/src/plugins/value/utils/library_functions.ml
@@ -82,7 +82,8 @@ let unsupported_specifications =
"posix_memalign", "stdlib.c";
"putenv", "stdlib.c";
"setenv", "stdlib.c";
- "unsetenv", "stdlib.c"
+ "unsetenv", "stdlib.c";
+ "realpath", "stdlib.c"
]
let unsupported_specs_tbl =
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 8ab5e9661ec..f2b765368ed 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -13,11 +13,11 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
-[metrics] Defined functions (82)
+[metrics] Defined functions (83)
======================
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_make_unknown (4 calls);
+ Frama_C_interval (16 calls); Frama_C_make_unknown (5 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);
@@ -31,14 +31,15 @@
isupper (0 call); isxdigit (0 call); localeconv (0 call); main (0 call);
memchr (0 call); memcmp (0 call); memcpy (4 calls); memmove (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);
+ posix_memalign (0 call); putenv (0 call); realpath (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 (411)
=========================
@@ -115,7 +116,7 @@
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); lseek (0 call); lstat (0 call); makedev (0 call);
- malloc (7 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+ malloc (8 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
mkdir (0 call); mkfifo (0 call); mknod (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);
@@ -178,18 +179,18 @@
Global metrics
==============
- Sloc = 1083
- Decision point = 204
+ Sloc = 1127
+ Decision point = 213
Global variables = 70
- If = 195
+ If = 198
Loop = 43
- Goto = 89
- Assignment = 438
- Exit point = 82
- Function = 493
- Function call = 89
- Pointer dereferencing = 158
- Cyclomatic complexity = 286
+ Goto = 97
+ Assignment = 459
+ Exit point = 83
+ Function = 494
+ Function call = 93
+ Pointer dereferencing = 159
+ Cyclomatic complexity = 296
/* Generated by Frama-C */
#include "__fc_builtin.c"
#include "__fc_builtin.h"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index ce58bfc1d77..f0bf4264838 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2564,6 +2564,9 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
extern int mkstemp(char *templat);
+char *realpath(char const * __restrict file_name,
+ char * __restrict resolved_name);
+
int glob(char const *pattern, int flags,
int (*errfunc)(char const *epath, int eerrno), glob_t *pglob)
{
@@ -5349,6 +5352,53 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
return_label: return __retres;
}
+char *realpath(char const * __restrict file_name,
+ char * __restrict resolved_name)
+{
+ char *__retres;
+ int tmp;
+ if (! file_name) {
+ __fc_errno = 22;
+ __retres = (char *)0;
+ goto return_label;
+ }
+ tmp = Frama_C_interval(0,6);
+ switch (tmp) {
+ case 0: __fc_errno = 13;
+ __retres = (char *)0;
+ goto return_label;
+ case 1: __fc_errno = 5;
+ __retres = (char *)0;
+ goto return_label;
+ case 2: __fc_errno = 40;
+ __retres = (char *)0;
+ goto return_label;
+ case 3: __fc_errno = 36;
+ __retres = (char *)0;
+ goto return_label;
+ case 4: __fc_errno = 2;
+ __retres = (char *)0;
+ goto return_label;
+ case 5: __fc_errno = 20;
+ __retres = (char *)0;
+ goto return_label;
+ default: break;
+ }
+ int realpath_len = Frama_C_interval(1,256);
+ if (! resolved_name) {
+ resolved_name = (char *)malloc((unsigned int)256);
+ if (! resolved_name) {
+ __fc_errno = 12;
+ __retres = (char *)0;
+ goto return_label;
+ }
+ }
+ Frama_C_make_unknown(resolved_name,(unsigned int)realpath_len);
+ *(resolved_name + (realpath_len - 1)) = (char)'\000';
+ __retres = resolved_name;
+ return_label: return __retres;
+}
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle
index 37622a4661e..d091a47903a 100644
--- a/tests/libc/oracle/stdlib_c.0.res.oracle
+++ b/tests/libc/oracle/stdlib_c.0.res.oracle
@@ -4,80 +4,80 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/libc/stdlib_c.c:14:
+[eva] tests/libc/stdlib_c.c:15:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:14: allocating variable __calloc_main_l14
-[eva] tests/libc/stdlib_c.c:16: assertion got status valid.
+[eva] tests/libc/stdlib_c.c:15: allocating variable __calloc_main_l15
+[eva] tests/libc/stdlib_c.c:17: assertion got status valid.
[eva] computing for function Frama_C_size_t_interval <- main.
- Called from tests/libc/stdlib_c.c:20.
+ Called from tests/libc/stdlib_c.c:21.
[eva] using specification for function Frama_C_size_t_interval
-[eva] tests/libc/stdlib_c.c:20:
+[eva] tests/libc/stdlib_c.c:21:
function Frama_C_size_t_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_size_t_interval
[eva] computing for function Frama_C_size_t_interval <- main.
- Called from tests/libc/stdlib_c.c:20.
+ Called from tests/libc/stdlib_c.c:21.
[eva] Done for function Frama_C_size_t_interval
-[eva] tests/libc/stdlib_c.c:21:
+[eva] tests/libc/stdlib_c.c:22:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:21: Warning:
+[eva] tests/libc/stdlib_c.c:22: Warning:
calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
-[eva] tests/libc/stdlib_c.c:21: allocating variable __calloc_main_l21
-[eva] tests/libc/stdlib_c.c:21:
+[eva] tests/libc/stdlib_c.c:22: allocating variable __calloc_main_l22
+[eva] tests/libc/stdlib_c.c:22:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:23: assertion got status valid.
-[eva] tests/libc/stdlib_c.c:27:
+[eva] tests/libc/stdlib_c.c:24: assertion got status valid.
+[eva] tests/libc/stdlib_c.c:28:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:27: Warning:
+[eva] tests/libc/stdlib_c.c:28: Warning:
calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
-[eva] tests/libc/stdlib_c.c:27:
+[eva] tests/libc/stdlib_c.c:28:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:27:
+[eva] tests/libc/stdlib_c.c:28:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:27:
+[eva] tests/libc/stdlib_c.c:28:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:28: assertion got status valid.
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:29: assertion got status valid.
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:32: allocating variable __calloc_main_l32
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:33: allocating variable __calloc_main_l33
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31) to fit 0..63
-[eva:alarm] tests/libc/stdlib_c.c:33: Warning:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31) to fit 0..63
+[eva:alarm] tests/libc/stdlib_c.c:34: Warning:
out of bounds write. assert \valid(s + (unsigned int)(i - 1));
-[eva] tests/libc/stdlib_c.c:31: starting to merge loop iterations
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:32: starting to merge loop iterations
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/63) to fit 0..63/95
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/63) to fit 0..63/95
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/95) to fit 0..63/127
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/95) to fit 0..63/127
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:32: Warning:
+[eva] tests/libc/stdlib_c.c:33: Warning:
calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/127) to fit 0..63/34359738367
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/127) to fit 0..63/34359738367
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32'
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33'
(0..31/34359738367) to fit 0..63/34359738367
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32'
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33'
(0..31/34359738367) to fit 0..63/34359738367
[eva] computing for function posix_memalign <- main.
- Called from tests/libc/stdlib_c.c:37.
+ Called from tests/libc/stdlib_c.c:38.
[eva] share/libc/stdlib.c:196:
assertion 'alignment_is_a_suitable_power_of_two' got status valid.
[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
@@ -85,25 +85,131 @@
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
[eva] computing for function free <- main.
- Called from tests/libc/stdlib_c.c:38.
+ Called from tests/libc/stdlib_c.c:39.
[eva] using specification for function free
-[eva] tests/libc/stdlib_c.c:38: Warning: ignoring unsupported \allocates clause
-[eva] tests/libc/stdlib_c.c:38:
+[eva] tests/libc/stdlib_c.c:39: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:39:
function free: precondition 'freeable' got status valid.
[eva] Done for function free
[eva] computing for function posix_memalign <- main.
- Called from tests/libc/stdlib_c.c:39.
+ Called from tests/libc/stdlib_c.c:40.
[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
[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.
- Called from tests/libc/stdlib_c.c:40.
-[eva] tests/libc/stdlib_c.c:40: Warning: ignoring unsupported \allocates clause
-[eva] tests/libc/stdlib_c.c:40:
+ Called from tests/libc/stdlib_c.c:41.
+[eva] tests/libc/stdlib_c.c:41: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:41:
+ function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] tests/libc/stdlib_c.c:44: Call to builtin Frama_C_malloc
+[eva] tests/libc/stdlib_c.c:44: allocating variable __malloc_main_l44
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:46.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] using specification for function Frama_C_interval
+[eva] share/libc/stdlib.c:213:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] share/libc/stdlib.c:222:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] using specification for function Frama_C_make_unknown
+[eva] share/libc/stdlib.c:230:
+ function Frama_C_make_unknown: precondition 'valid_p' got status valid.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva:alarm] tests/libc/stdlib_c.c:48: Warning:
+ assertion 'valid_if_exact' got status unknown.
+[eva] computing for function Frama_C_nondet <- main.
+ Called from tests/libc/stdlib_c.c:50.
+[eva] using specification for function Frama_C_nondet
+[eva] Done for function Frama_C_nondet
+[eva] computing for function Frama_C_nondet <- main.
+ Called from tests/libc/stdlib_c.c:50.
+[eva] Done for function Frama_C_nondet
+[eva:alarm] tests/libc/stdlib_c.c:51: Warning:
+ assertion 'maybe_uninitialized' got status unknown.
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:53.
+[eva] tests/libc/stdlib_c.c:53: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:53:
function free: precondition 'freeable' got status valid.
[eva] Done for function free
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:53.
+[eva] Done for function free
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:53.
+[eva] Done for function free
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:53.
+[eva] Done for function free
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:54.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] share/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] share/libc/stdlib.c:224: allocating variable __malloc_realpath_l224
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:54.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] share/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:54.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] share/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:54.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] share/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -112,17 +218,36 @@
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 realpath:
+ __fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
+ __fc_errno ∈ [--..--]
+ resolved_name ∈
+ {{ NULL ; &__malloc_main_l44[0] ;
+ &__malloc_realpath_l224[0] }}
+ realpath_len ∈ [1..256]
+ __retres ∈
+ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] }}
+ __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224[0] ∈ [--..--]
+ [1..255] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
- p ∈ {{ NULL ; &__calloc_main_l14 }}
+ __fc_errno ∈ [--..--]
+ p ∈ {{ NULL ; &__calloc_main_l15 }}
nmemb ∈ [1..4294967295]
- q ∈ {{ NULL ; &__calloc_main_l21[0] }}
+ q ∈ {{ NULL ; &__calloc_main_l22[0] }}
r ∈ {0}
- s ∈ {{ NULL ; &__calloc_w_main_l32[0] }}
+ s ∈ {{ NULL ; &__calloc_w_main_l33[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}
- __calloc_w_main_l32[0..1073741823] ∈ {0; 42}
+ resolved_name ∈ {{ NULL ; &__malloc_main_l44[0] }}
+ realpath_res ∈ {{ NULL ; &__malloc_realpath_l224[0] }}
+ __retres ∈ {0; 1}
+ __calloc_w_main_l33[0..1073741823] ∈ {0; 42}
+ __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224[0] ∈ [--..--]
+ [1..255] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/stdlib_c.1.res.oracle b/tests/libc/oracle/stdlib_c.1.res.oracle
index 430cfeea5d9..348bcec67f0 100644
--- a/tests/libc/oracle/stdlib_c.1.res.oracle
+++ b/tests/libc/oracle/stdlib_c.1.res.oracle
@@ -4,99 +4,99 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/libc/stdlib_c.c:14:
+[eva] tests/libc/stdlib_c.c:15:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:14: allocating variable __calloc_main_l14
-[eva] tests/libc/stdlib_c.c:16: assertion got status valid.
+[eva] tests/libc/stdlib_c.c:15: allocating variable __calloc_main_l15
+[eva] tests/libc/stdlib_c.c:17: assertion got status valid.
[eva] computing for function Frama_C_size_t_interval <- main.
- Called from tests/libc/stdlib_c.c:20.
+ Called from tests/libc/stdlib_c.c:21.
[eva] using specification for function Frama_C_size_t_interval
-[eva] tests/libc/stdlib_c.c:20:
+[eva] tests/libc/stdlib_c.c:21:
function Frama_C_size_t_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_size_t_interval
-[eva] tests/libc/stdlib_c.c:21:
+[eva] tests/libc/stdlib_c.c:22:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:21: Warning:
+[eva] tests/libc/stdlib_c.c:22: Warning:
calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
-[eva] tests/libc/stdlib_c.c:21: allocating variable __calloc_main_l21
-[eva] tests/libc/stdlib_c.c:23: assertion got status valid.
-[eva] tests/libc/stdlib_c.c:27:
+[eva] tests/libc/stdlib_c.c:22: allocating variable __calloc_main_l22
+[eva] tests/libc/stdlib_c.c:24: assertion got status valid.
+[eva] tests/libc/stdlib_c.c:28:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:27: Warning:
+[eva] tests/libc/stdlib_c.c:28: Warning:
calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
-[eva] tests/libc/stdlib_c.c:27:
+[eva] tests/libc/stdlib_c.c:28:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:28: assertion got status valid.
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:29: assertion got status valid.
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:32: allocating variable __calloc_main_l32
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:33: allocating variable __calloc_main_l33
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31) to fit 0..63
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31) to fit 0..63
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/63) to fit 0..63
-[eva:alarm] tests/libc/stdlib_c.c:33: Warning:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/63) to fit 0..63
+[eva:alarm] tests/libc/stdlib_c.c:34: Warning:
out of bounds write. assert \valid(s + (unsigned int)(i - 1));
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/63) to fit 0..95
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/63) to fit 0..95
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/95) to fit 0..95
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/95) to fit 0..95
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/95) to fit 0..127
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/95) to fit 0..127
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/127) to fit 0..127
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/127) to fit 0..127
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/127) to fit 0..159
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/127) to fit 0..159
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/159) to fit 0..159
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/159) to fit 0..159
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/159) to fit 0..191
-[eva] tests/libc/stdlib_c.c:31: starting to merge loop iterations
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/159) to fit 0..191
+[eva] tests/libc/stdlib_c.c:32: starting to merge loop iterations
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/191) to fit 0..191/223
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/191) to fit 0..191/223
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/223) to fit 0..191/255
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/223) to fit 0..191/255
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva] tests/libc/stdlib_c.c:32: Warning:
+[eva] tests/libc/stdlib_c.c:33: Warning:
calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32' (0..31/255) to fit 0..191/34359738367
-[eva] tests/libc/stdlib_c.c:32:
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33' (0..31/255) to fit 0..191/34359738367
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32'
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33'
(0..31/34359738367) to fit 0..191/34359738367
-[eva] tests/libc/stdlib_c.c:32:
+[eva] tests/libc/stdlib_c.c:33:
Call to builtin Frama_C_calloc for function calloc
-[eva:malloc] tests/libc/stdlib_c.c:32:
- resizing variable `__calloc_w_main_l32'
+[eva:malloc] tests/libc/stdlib_c.c:33:
+ resizing variable `__calloc_w_main_l33'
(0..31/34359738367) to fit 0..191/34359738367
[eva] computing for function posix_memalign <- main.
- Called from tests/libc/stdlib_c.c:37.
+ Called from tests/libc/stdlib_c.c:38.
[eva] share/libc/stdlib.c:196:
assertion 'alignment_is_a_suitable_power_of_two' got status valid.
[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
@@ -104,25 +104,131 @@
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
[eva] computing for function free <- main.
- Called from tests/libc/stdlib_c.c:38.
+ Called from tests/libc/stdlib_c.c:39.
[eva] using specification for function free
-[eva] tests/libc/stdlib_c.c:38: Warning: ignoring unsupported \allocates clause
-[eva] tests/libc/stdlib_c.c:38:
+[eva] tests/libc/stdlib_c.c:39: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:39:
function free: precondition 'freeable' got status valid.
[eva] Done for function free
[eva] computing for function posix_memalign <- main.
- Called from tests/libc/stdlib_c.c:39.
+ Called from tests/libc/stdlib_c.c:40.
[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
[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.
- Called from tests/libc/stdlib_c.c:40.
-[eva] tests/libc/stdlib_c.c:40: Warning: ignoring unsupported \allocates clause
-[eva] tests/libc/stdlib_c.c:40:
+ Called from tests/libc/stdlib_c.c:41.
+[eva] tests/libc/stdlib_c.c:41: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:41:
function free: precondition 'freeable' got status valid.
[eva] Done for function free
+[eva] tests/libc/stdlib_c.c:44: Call to builtin Frama_C_malloc
+[eva] tests/libc/stdlib_c.c:44: allocating variable __malloc_main_l44
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:46.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] using specification for function Frama_C_interval
+[eva] share/libc/stdlib.c:213:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] share/libc/stdlib.c:222:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] using specification for function Frama_C_make_unknown
+[eva] share/libc/stdlib.c:230:
+ function Frama_C_make_unknown: precondition 'valid_p' got status valid.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva:alarm] tests/libc/stdlib_c.c:48: Warning:
+ assertion 'valid_if_exact' got status unknown.
+[eva] computing for function Frama_C_nondet <- main.
+ Called from tests/libc/stdlib_c.c:50.
+[eva] using specification for function Frama_C_nondet
+[eva] Done for function Frama_C_nondet
+[eva] computing for function Frama_C_nondet <- main.
+ Called from tests/libc/stdlib_c.c:50.
+[eva] Done for function Frama_C_nondet
+[eva:alarm] tests/libc/stdlib_c.c:51: Warning:
+ assertion 'maybe_uninitialized' got status unknown.
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:53.
+[eva] tests/libc/stdlib_c.c:53: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:53:
+ function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:53.
+[eva] Done for function free
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:53.
+[eva] Done for function free
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:53.
+[eva] Done for function free
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:54.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] share/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] share/libc/stdlib.c:224: allocating variable __malloc_realpath_l224
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:54.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] share/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:54.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] share/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:54.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] share/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -131,17 +237,36 @@
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 realpath:
+ __fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
+ __fc_errno ∈ [--..--]
+ resolved_name ∈
+ {{ NULL ; &__malloc_main_l44[0] ;
+ &__malloc_realpath_l224[0] }}
+ realpath_len ∈ [1..256]
+ __retres ∈
+ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] }}
+ __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224[0] ∈ [--..--]
+ [1..255] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
- p ∈ {{ &__calloc_main_l14 }}
+ __fc_errno ∈ [--..--]
+ p ∈ {{ &__calloc_main_l15 }}
nmemb ∈ [1..4294967295]
- q ∈ {{ NULL ; &__calloc_main_l21[0] }}
+ q ∈ {{ NULL ; &__calloc_main_l22[0] }}
r ∈ {0}
- s ∈ {{ NULL ; &__calloc_w_main_l32[0] }}
+ s ∈ {{ NULL ; &__calloc_w_main_l33[0] }}
p_al0 ∈ {{ &__malloc_posix_memalign_l199[0] }}
p_al1 ∈ {{ &__malloc_posix_memalign_l199_0[0] }}
p_memal_res ∈ {0}
p_memal_res2 ∈ {0}
+ resolved_name ∈ {{ &__malloc_main_l44[0] }}
+ realpath_res ∈ {{ NULL ; &__malloc_realpath_l224[0] }}
__retres ∈ {0}
- __calloc_w_main_l32[0..1073741823] ∈ {0; 42}
+ __calloc_w_main_l33[0..1073741823] ∈ {0; 42}
+ __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224[0] ∈ [--..--]
+ [1..255] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle
index 70c7ee08e99..37236106c30 100644
--- a/tests/libc/oracle/stdlib_c.2.res.oracle
+++ b/tests/libc/oracle/stdlib_c.2.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
[eva] computing for function calloc <- main.
- Called from tests/libc/stdlib_c.c:14.
+ Called from tests/libc/stdlib_c.c:15.
[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
[eva] share/libc/stdlib.c:72: allocating variable __malloc_calloc_l72
[eva] computing for function memset <- calloc <- main.
@@ -18,15 +18,15 @@
[eva] Done for function memset
[eva] Recording results for calloc
[eva] Done for function calloc
-[eva] tests/libc/stdlib_c.c:16: assertion got status valid.
+[eva] tests/libc/stdlib_c.c:17: assertion got status valid.
[eva] computing for function Frama_C_size_t_interval <- main.
- Called from tests/libc/stdlib_c.c:20.
+ Called from tests/libc/stdlib_c.c:21.
[eva] using specification for function Frama_C_size_t_interval
-[eva] tests/libc/stdlib_c.c:20:
+[eva] tests/libc/stdlib_c.c:21:
function Frama_C_size_t_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_size_t_interval
[eva] computing for function calloc <- main.
- Called from tests/libc/stdlib_c.c:21.
+ Called from tests/libc/stdlib_c.c:22.
[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
[eva] share/libc/stdlib.c:72: allocating variable __malloc_calloc_l72_0
[eva] computing for function memset <- calloc <- main.
@@ -36,14 +36,14 @@
[eva] Done for function memset
[eva] Recording results for calloc
[eva] Done for function calloc
-[eva:alarm] tests/libc/stdlib_c.c:23: Warning: assertion got status unknown.
+[eva:alarm] tests/libc/stdlib_c.c:24: Warning: assertion got status unknown.
[eva] computing for function calloc <- main.
- Called from tests/libc/stdlib_c.c:27.
+ Called from tests/libc/stdlib_c.c:28.
[eva] Recording results for calloc
[eva] Done for function calloc
-[eva] tests/libc/stdlib_c.c:28: assertion got status valid.
+[eva] tests/libc/stdlib_c.c:29: assertion got status valid.
[eva] computing for function calloc <- main.
- Called from tests/libc/stdlib_c.c:32.
+ Called from tests/libc/stdlib_c.c:33.
[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
[eva] share/libc/stdlib.c:72: allocating variable __malloc_calloc_l72_1
[eva] computing for function memset <- calloc <- main.
@@ -51,19 +51,19 @@
[eva] Done for function memset
[eva] Recording results for calloc
[eva] Done for function calloc
-[eva] tests/libc/stdlib_c.c:31: starting to merge loop iterations
+[eva] tests/libc/stdlib_c.c:32: starting to merge loop iterations
[eva] computing for function calloc <- main.
- Called from tests/libc/stdlib_c.c:32.
+ Called from tests/libc/stdlib_c.c:33.
[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
[eva] computing for function memset <- calloc <- main.
Called from share/libc/stdlib.c:73.
[eva] Done for function memset
[eva] Recording results for calloc
[eva] Done for function calloc
-[eva:alarm] tests/libc/stdlib_c.c:33: Warning:
+[eva:alarm] tests/libc/stdlib_c.c:34: Warning:
out of bounds write. assert \valid(s + (unsigned int)(i - 1));
[eva] computing for function calloc <- main.
- Called from tests/libc/stdlib_c.c:32.
+ Called from tests/libc/stdlib_c.c:33.
[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
[eva] computing for function memset <- calloc <- main.
Called from share/libc/stdlib.c:73.
@@ -71,7 +71,7 @@
[eva] Recording results for calloc
[eva] Done for function calloc
[eva] computing for function calloc <- main.
- Called from tests/libc/stdlib_c.c:32.
+ Called from tests/libc/stdlib_c.c:33.
[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
[eva] computing for function memset <- calloc <- main.
Called from share/libc/stdlib.c:73.
@@ -79,7 +79,7 @@
[eva] Recording results for calloc
[eva] Done for function calloc
[eva] computing for function calloc <- main.
- Called from tests/libc/stdlib_c.c:32.
+ Called from tests/libc/stdlib_c.c:33.
[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
[eva] computing for function memset <- calloc <- main.
Called from share/libc/stdlib.c:73.
@@ -87,7 +87,7 @@
[eva] Recording results for calloc
[eva] Done for function calloc
[eva] computing for function calloc <- main.
- Called from tests/libc/stdlib_c.c:32.
+ Called from tests/libc/stdlib_c.c:33.
[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
[eva] computing for function memset <- calloc <- main.
Called from share/libc/stdlib.c:73.
@@ -95,7 +95,7 @@
[eva] Recording results for calloc
[eva] Done for function calloc
[eva] computing for function posix_memalign <- main.
- Called from tests/libc/stdlib_c.c:37.
+ Called from tests/libc/stdlib_c.c:38.
[eva] share/libc/stdlib.c:196:
assertion 'alignment_is_a_suitable_power_of_two' got status valid.
[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
@@ -103,25 +103,77 @@
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
[eva] computing for function free <- main.
- Called from tests/libc/stdlib_c.c:38.
+ Called from tests/libc/stdlib_c.c:39.
[eva] using specification for function free
-[eva] tests/libc/stdlib_c.c:38: Warning: ignoring unsupported \allocates clause
-[eva] tests/libc/stdlib_c.c:38:
+[eva] tests/libc/stdlib_c.c:39: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:39:
function free: precondition 'freeable' got status valid.
[eva] Done for function free
[eva] computing for function posix_memalign <- main.
- Called from tests/libc/stdlib_c.c:39.
+ Called from tests/libc/stdlib_c.c:40.
[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
[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.
- Called from tests/libc/stdlib_c.c:40.
-[eva] tests/libc/stdlib_c.c:40: Warning: ignoring unsupported \allocates clause
-[eva] tests/libc/stdlib_c.c:40:
+ Called from tests/libc/stdlib_c.c:41.
+[eva] tests/libc/stdlib_c.c:41: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:41:
+ function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] tests/libc/stdlib_c.c:44: Call to builtin Frama_C_malloc
+[eva] tests/libc/stdlib_c.c:44: allocating variable __malloc_main_l44
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:46.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] using specification for function Frama_C_interval
+[eva] share/libc/stdlib.c:213:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] share/libc/stdlib.c:222:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] using specification for function Frama_C_make_unknown
+[eva] share/libc/stdlib.c:230:
+ function Frama_C_make_unknown: precondition 'valid_p' got status valid.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
+[eva:alarm] tests/libc/stdlib_c.c:48: Warning:
+ assertion 'valid_if_exact' got status unknown.
+[eva] computing for function Frama_C_nondet <- main.
+ Called from tests/libc/stdlib_c.c:50.
+[eva] using specification for function Frama_C_nondet
+[eva] Done for function Frama_C_nondet
+[eva:alarm] tests/libc/stdlib_c.c:51: Warning:
+ assertion 'maybe_uninitialized' got status unknown.
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:53.
+[eva] tests/libc/stdlib_c.c:53: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:53:
function free: precondition 'freeable' got status valid.
[eva] Done for function free
+[eva] computing for function realpath <- main.
+ Called from tests/libc/stdlib_c.c:54.
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:213.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- realpath <- main.
+ Called from share/libc/stdlib.c:222.
+[eva] Done for function Frama_C_interval
+[eva] share/libc/stdlib.c:224: Call to builtin Frama_C_malloc
+[eva] share/libc/stdlib.c:224: allocating variable __malloc_realpath_l224
+[eva] computing for function Frama_C_make_unknown <- realpath <- main.
+ Called from share/libc/stdlib.c:230.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for realpath
+[eva] Done for function realpath
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -143,9 +195,22 @@
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 realpath:
+ __fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
+ __fc_errno ∈ [--..--]
+ resolved_name ∈
+ {{ NULL ; &__malloc_main_l44[0] ;
+ &__malloc_realpath_l224[0] }}
+ realpath_len ∈ [1..256]
+ __retres ∈
+ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] }}
+ __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224[0..255] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
+ __fc_errno ∈ [--..--]
p ∈ {{ NULL ; (int *)&__malloc_calloc_l72 }}
nmemb ∈ [1..4294967295]
q ∈ {{ NULL ; (int *)&__malloc_calloc_l72_0 }}
@@ -155,7 +220,11 @@
p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l199_0[0] }}
p_memal_res ∈ {0; 12}
p_memal_res2 ∈ {0; 12}
- __retres ∈ {0}
+ resolved_name ∈ {{ NULL ; &__malloc_main_l44[0] }}
+ realpath_res ∈ {{ NULL ; &__malloc_realpath_l224[0] }}
+ __retres ∈ {0; 1}
__malloc_calloc_l72[0..3] ∈ [--..--] or UNINITIALIZED
__malloc_calloc_l72_0[0..4294967291] ∈ [--..--] or UNINITIALIZED
__malloc_w_calloc_l72_1[0..4294967291] ∈ [--..--] or UNINITIALIZED
+ __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224[0..255] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/stdlib_c.c b/tests/libc/stdlib_c.c
index f021a7551c1..d1dbd85a5a3 100644
--- a/tests/libc/stdlib_c.c
+++ b/tests/libc/stdlib_c.c
@@ -8,6 +8,7 @@
#include "stdlib.c"
#include "__fc_builtin.h"
#include <stdint.h>
+#include <limits.h>
int main() {
// always succeeds if -eva-no-alloc-returns-null, otherwise may succeed
@@ -39,5 +40,18 @@ int main() {
int p_memal_res2 = posix_memalign((void**)&p_al1, 32, 42);
free(p_al1);
+ //__fc_realpath test
+ char *resolved_name = malloc(PATH_MAX);
+ if (!resolved_name) return 1;
+ char *realpath_res = realpath("/bin/ls", resolved_name);
+ if (realpath_res) {
+ //@ assert valid_if_exact: valid_read_string(realpath_res);
+ }
+ if (Frama_C_nondet(0, 1)) {
+ //@ assert maybe_uninitialized: \initialized(resolved_name + PATH_MAX-1);
+ }
+ free(resolved_name);
+ realpath_res = realpath("/bin/ls", NULL);
+
return 0;
}
--
GitLab