From 1b013a8bed7866a82ed0a0a676288e6285422895 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 11 Oct 2021 17:28:15 +0200
Subject: [PATCH] [Libc] add semi-spec and stub for non-POSIX asprintf
---
share/libc/stdio.c | 20 ++
share/libc/stdio.h | 16 ++
.../instrumentation_model/e_acsl_contract.h | 2 +-
.../e_acsl_observation_model.h | 2 +-
.../e-acsl/tests/arith/oracle/gen_arith.c | 1 +
.../e-acsl/tests/arith/oracle/gen_array.c | 1 +
.../e-acsl/tests/arith/oracle/gen_at.c | 1 +
.../oracle/gen_at_on-purely-logic-variables.c | 1 +
.../e-acsl/tests/arith/oracle/gen_bitwise.c | 1 +
.../e-acsl/tests/arith/oracle/gen_cast.c | 1 +
.../tests/arith/oracle/gen_comparison.c | 1 +
.../arith/oracle/gen_extended_quantifiers.c | 1 +
.../e-acsl/tests/arith/oracle/gen_functions.c | 1 +
.../tests/arith/oracle/gen_functions_rec.c | 1 +
.../tests/arith/oracle/gen_integer_constant.c | 1 +
.../e-acsl/tests/arith/oracle/gen_let.c | 1 +
.../e-acsl/tests/arith/oracle/gen_longlong.c | 1 +
.../e-acsl/tests/arith/oracle/gen_not.c | 1 +
.../e-acsl/tests/arith/oracle/gen_quantif.c | 1 +
.../e-acsl/tests/arith/oracle/gen_rationals.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1304.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1324.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1326.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1395.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1478.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1700.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1717.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1718.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1740.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1837.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts2191.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts2231.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts2305.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts2386.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts2406.c | 1 +
.../tests/bts/oracle/gen_issue-eacsl-105.c | 1 +
.../tests/bts/oracle/gen_issue-eacsl-139.c | 1 +
.../tests/bts/oracle/gen_issue-eacsl-145.c | 1 +
.../tests/bts/oracle/gen_issue-eacsl-149.c | 1 +
.../tests/bts/oracle/gen_issue-eacsl-172.c | 1 +
.../tests/bts/oracle/gen_issue-eacsl-177.c | 1 +
.../tests/bts/oracle/gen_issue-eacsl-91.c | 1 +
.../e-acsl/tests/bts/oracle/gen_issue69.c | 1 +
.../bts/oracle/issue-eacsl-145.res.oracle | 1 -
.../tests/constructs/oracle/gen_decrease.c | 1 +
.../tests/constructs/oracle/gen_false.c | 1 +
.../constructs/oracle/gen_function_contract.c | 1 +
.../tests/constructs/oracle/gen_ghost.c | 1 +
.../tests/constructs/oracle/gen_invariant.c | 1 +
.../constructs/oracle/gen_labeled_stmt.c | 1 +
.../e-acsl/tests/constructs/oracle/gen_lazy.c | 1 +
.../e-acsl/tests/constructs/oracle/gen_loop.c | 1 +
.../constructs/oracle/gen_nested_code_annot.c | 1 +
.../tests/constructs/oracle/gen_result.c | 1 +
.../e-acsl/tests/constructs/oracle/gen_rte.c | 1 +
.../constructs/oracle/gen_stmt_contract.c | 1 +
.../e-acsl/tests/constructs/oracle/gen_true.c | 1 +
.../tests/constructs/oracle/gen_typedef.c | 1 +
.../tests/examples/oracle/gen_linear_search.c | 1 +
.../tests/full-mtracking/oracle/gen_addrOf.c | 1 +
.../e-acsl/tests/gmp-only/oracle/gen_arith.c | 1 +
.../tests/gmp-only/oracle/gen_functions.c | 1 +
.../e-acsl/tests/memory/oracle/gen_addrOf.c | 1 +
.../e-acsl/tests/memory/oracle/gen_alias.c | 1 +
.../tests/memory/oracle/gen_bypassed_var.c | 1 +
.../memory/oracle/gen_compound_initializers.c | 1 +
.../tests/memory/oracle/gen_ctype_macros.c | 1 +
.../tests/memory/oracle/gen_decl_in_switch.c | 1 +
.../tests/memory/oracle/gen_early_exit.c | 1 +
.../memory/oracle/gen_ghost_parameters.c | 1 +
.../e-acsl/tests/memory/oracle/gen_goto.c | 1 +
.../e-acsl/tests/memory/oracle/gen_init.c | 1 +
.../tests/memory/oracle/gen_literal_string.c | 1 +
.../tests/memory/oracle/gen_local_init.c | 1 +
.../e-acsl/tests/memory/oracle/gen_null.c | 1 +
.../tests/memory/oracle/gen_other_constants.c | 1 +
.../e-acsl/tests/memory/oracle/gen_ptr.c | 1 +
.../e-acsl/tests/memory/oracle/gen_sizeof.c | 1 +
.../e-acsl/tests/memory/oracle/gen_vla.c | 1 +
.../e-acsl/tests/special/oracle/gen_builtin.c | 1 +
.../special/oracle/gen_e-acsl-bittree-model.c | 1 +
.../oracle/gen_e-acsl-compile-dlmalloc.c | 1 +
.../special/oracle/gen_e-acsl-functions.c | 1 +
.../special/oracle/gen_e-acsl-instrument.c | 1 +
.../special/oracle/gen_e-acsl-rt-debug.c | 1 +
.../special/oracle/gen_e-acsl-segment-model.c | 1 +
.../tests/temporal/oracle/gen_t_addr-by-val.c | 1 +
.../tests/temporal/oracle/gen_t_array.c | 1 +
.../e-acsl/tests/temporal/oracle/gen_t_char.c | 1 +
.../tests/temporal/oracle/gen_t_darray.c | 1 +
.../e-acsl/tests/temporal/oracle/gen_t_fptr.c | 1 +
.../tests/temporal/oracle/gen_t_global_init.c | 1 +
.../tests/temporal/oracle/gen_t_labels.c | 1 +
.../tests/temporal/oracle/gen_t_lit_string.c | 1 +
.../tests/temporal/oracle/gen_t_scope.c | 1 +
.../tests/temporal/oracle/gen_t_while.c | 1 +
src/plugins/value/utils/library_functions.ml | 3 +-
.../tests/erroneous/oracle/printf.res.oracle | 2 +
.../tests/known/oracle/printf.res.oracle | 3 +
.../oracle/printf_garbled_mix.res.oracle | 2 +
.../oracle/printf_wrong_arity.res.oracle | 3 +
.../oracle/printf_wrong_pointers.res.oracle | 2 +
.../oracle/printf_wrong_types.res.oracle | 4 +
.../tests/known/oracle/scanf.res.oracle | 2 +
.../tests/known/oracle/scanf_loop.res.oracle | 2 +
.../tests/known/oracle/scanf_wrong.res.oracle | 2 +
.../tests/known/oracle/snprintf.res.oracle | 2 +
.../tests/known/oracle/stdio_print.res.oracle | 2 +
.../tests/known/oracle/stdio_scan.res.oracle | 2 +
.../tests/known/oracle/swprintf.res.oracle | 2 +
.../tests/known/oracle/wchar.res.oracle | 2 +
.../builtins/oracle/linked_list.0.res.oracle | 18 ++
.../builtins/oracle/linked_list.1.res.oracle | 18 ++
.../builtins/oracle/linked_list.2.res.oracle | 20 ++
tests/idct/oracle/ieee_1180_1990.res.oracle | 42 ++-
tests/libc/oracle/fc_libc.0.res.oracle | 49 ++--
tests/libc/oracle/fc_libc.1.res.oracle | 32 +++
tests/libc/oracle/stdio_c.res.oracle | 255 ++++++++++--------
tests/libc/oracle/stdio_h.res.oracle | 26 +-
tests/libc/stdio_c.c | 15 +-
tests/libc/stdio_h.c | 9 +-
tests/metrics/oracle/libc.1.res.oracle | 38 +--
tests/metrics/oracle/libc.json | 6 +-
tests/rte/oracle/value_rte.res.oracle | 29 +-
125 files changed, 562 insertions(+), 163 deletions(-)
diff --git a/share/libc/stdio.c b/share/libc/stdio.c
index 0da68a57ac7..bc46eb85673 100644
--- a/share/libc/stdio.c
+++ b/share/libc/stdio.c
@@ -20,6 +20,7 @@
/* */
/**************************************************************************/
+#include "__fc_builtin.h"
#include "stdio.h"
#include "stdlib.h"
#include "stdint.h" // for SIZE_MAX
@@ -92,4 +93,23 @@ ssize_t getline(char **lineptr, size_t *n, FILE *stream) {
return -1;
}
+// Non-POSIX; arbitrarily allocates between 1 and 256 bytes.
+// This stub is unsound in the general case, but enough for
+// many test cases.
+int asprintf(char **strp, const char *fmt, ...) {
+ va_list args;
+ va_start(args, fmt);
+ size_t len = Frama_C_interval(1, 256);
+ *strp = malloc(len);
+ if (!*strp) {
+ va_end(args);
+ return -1;
+ }
+ // Emulate writing to the string
+ Frama_C_make_unknown(*strp, len - 1U);
+ (*strp)[len - 1U] = 0;
+ return len;
+}
+
+
__POP_FC_STDLIB
diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index 93a5829898c..18fa5958b7c 100644
--- a/share/libc/stdio.h
+++ b/share/libc/stdio.h
@@ -583,6 +583,22 @@ extern int pclose(FILE *stream);
ssize_t getline(char **lineptr, size_t *n, FILE *stream);
#endif
+// Non-POSIX; allocates memory, so requires 'stdio.c' to be included
+
+#include "__fc_alloc_axiomatic.h"
+
+/*@
+ requires valid_strp: \valid(strp);
+ requires valid_fmt: valid_read_string(fmt);
+ assigns __fc_heap_status \from indirect:fmt[0 ..], __fc_heap_status;
+ assigns \result \from indirect:fmt[0 ..], indirect:__fc_heap_status;
+ assigns *strp \from fmt[0 ..], indirect:__fc_heap_status;
+ //missing: variadic arguments
+ ensures result_error_or_written_byes: \result == -1 || \result >= 0;
+ allocates *strp;
+*/
+int asprintf(char **strp, const char *fmt, ...);
+
__END_DECLS
#define IOV_MAX 1024
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h
index 98fa261bf28..d39f9104217 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h
@@ -32,7 +32,7 @@
#include "../internals/e_acsl_alias.h"
-#ifdef __FC_STDLIB
+#ifdef __FC_FEATURES_H
# include <__fc_alloc_axiomatic.h>
#else
/*@ ghost extern int __fc_heap_status; */
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
index 7cabbe5457d..ce068ecad6e 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
@@ -37,7 +37,7 @@
#include "../internals/e_acsl_alias.h"
#include "e_acsl_heap.h"
-#ifdef __FC_STDLIB
+#ifdef __FC_FEATURES_H
# include <__fc_alloc_axiomatic.h>
#else
/*@ ghost extern int __fc_heap_status; */
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c
index b5265e84689..7553a951c4b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle/gen_array.c
index 347680631d6..fd738aa7b4b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_array.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
index 877b80e482c..3f1cdbd8249 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
index 7357e7cf32c..2ea404238af 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c b/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
index a421b3f34be..0f070266079 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
index c63917398ce..c90b243c08b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
index 896c9741e9e..54bd5b922db 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
index 0dc365800f3..5e13957ce56 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index 84bbc75c2b9..bd14370f572 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
index b63ae684d46..42f39839d78 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
index 096a8cd3446..bdfdae9e75e 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_let.c b/src/plugins/e-acsl/tests/arith/oracle/gen_let.c
index 48a64c6fc1f..f1d72daba9f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_let.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_let.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
index e48f67cea87..90b0651a115 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_not.c b/src/plugins/e-acsl/tests/arith/oracle/gen_not.c
index d09bb71f994..a553f45a442 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_not.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
index ae624f3a5dd..762933f8fed 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
index 00ea678bb6d..e50e4e0f0f1 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
index 56cd1905203..8c7d12a1602 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index 3728e989aae..aa6edd56fa7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index c5b6665908d..9755e8cd106 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index e4ce2b0300f..68220ac9996 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
index 506172e9b1b..e22850aba10 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index db165cf968b..f235a94655c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
index 8693ba5674d..235b00e3ce3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index 9a2a7e93911..12837b756e4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index 72cbffe72fd..248e0c5dac9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
index ad106a78c1a..71d5655e76f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 98da9b92aa8..68b811cf123 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
char *__gen_e_acsl_literal_string_3;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
index ce15aa2b174..b83815b665d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
index 4a9f3921fd8..beb8f456827 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
index eb8feac0bb5..3e6032ceff5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
index c14d3f8d10b..60838e80f00 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
index d4fccb9af3c..3005fdba28a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c
index 2c8298f36dc..5a48d337504 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
index 3afa85d098a..e5d36213c84 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-145.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-145.c
index a68b9bc741b..072539c22ae 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-145.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-145.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
index 5710f18fae1..8d33325a01f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c
index b6559e0ca88..91b232c39ba 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
index dce9ccced14..f3b0980fe60 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
index b393878b816..24396bfc82b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
index bcb111b2c7a..c5762d971de 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
index e7143f3c725..6136cebc45e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
@@ -11,7 +11,6 @@
__e_acsl_sound_verdict ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
__e_acsl_heap_allocated_blocks ∈ [--..--]
- __fc_heap_status ∈ [--..--]
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c
index 5c9168343d0..c9da90bf22f 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_false.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_false.c
index 85b76ff45a6..b6db66215dc 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_false.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
index 22a773aa6be..c29fe752eee 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_ghost.c
index 7077d948dbe..19a1e3dfd46 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_ghost.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_invariant.c
index 6fd64a10a3a..65d2e93785c 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_invariant.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c
index a41944fff18..f1091f95d9b 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_lazy.c
index 3c90b94bef5..99047ada7fc 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_lazy.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c
index 2644fbaf96f..029e81dbde9 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_nested_code_annot.c
index 075893b1811..39cb8590d19 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_nested_code_annot.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
index f0840ee5da6..55615fb2891 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
index c329fa29818..fad68a23da5 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c
index c547c88f2b3..7fbeb0f748b 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_true.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_true.c
index 8603a3791f0..4417657b807 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_true.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_typedef.c
index 37c835510d0..45bc00f2631 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_typedef.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
index ebaf959d8bc..fa774f67e47 100644
--- a/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c
index c27908a810a..a27503d98f3 100644
--- a/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c
index cccd91e3f09..8c713255a98 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
index a803622c90b..a0dfc732599 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c
index a72dcdf1649..77eb66c7343 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c b/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c
index f73fcd60c90..c056a0c0b85 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
index d653ef1b72c..3b0b106b963 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c
index f324cd6b7eb..35129325096 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
char *__gen_e_acsl_literal_string_3;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
index f9916ddbab1..45e92a3f5de 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "ctype.h"
#include "stddef.h"
#include "stdio.h"
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
index 2eb6d843174..9cb1a440568 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
index 97debe70674..123bf12d8a5 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ghost_parameters.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ghost_parameters.c
index 3a4ab987b63..ade66b89b69 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ghost_parameters.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ghost_parameters.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
index ee4f315c4e1..70c0f2aa925 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_init.c
index 2c00fe4f012..276d86a0d82 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_init.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c
index 2ae93f0e987..61622601118 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
char *__gen_e_acsl_literal_string_6;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
index 3f3eb016471..0eb3cefd4a8 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_null.c b/src/plugins/e-acsl/tests/memory/oracle/gen_null.c
index 94b5ca7fced..375f0da0129 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_null.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c
index bdb06b362ea..7de63880550 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
index 4b7d6f59edd..3aadcd229f8 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c
index 7f829ac63e5..04238dc3f42 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
index 76649cc1f80..db99b831141 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
index 40a21f890be..a80a813054c 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-bittree-model.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-bittree-model.c
index 46e4f1c6e12..72d97a54831 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-bittree-model.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-bittree-model.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-compile-dlmalloc.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-compile-dlmalloc.c
index 59f62c0c1c0..2f77399ecaa 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-compile-dlmalloc.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-compile-dlmalloc.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
index 5b7a9aa5a54..79d83f6e40d 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
index be6541fd320..2a06979d910 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-rt-debug.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-rt-debug.c
index 59f62c0c1c0..2f77399ecaa 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-rt-debug.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-rt-debug.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-segment-model.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-segment-model.c
index 46e4f1c6e12..72d97a54831 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-segment-model.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-segment-model.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
index dfc3a961e28..0324021b4b2 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdint.h"
#include "stdio.h"
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c
index d36bd641170..17349b41486 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c
index 5369d3c824b..26ac8e12f25 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c
index f7db119cba3..2dd226207fc 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c
index d17b4ca48cc..5759e6ea84b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
index f682429dec8..5206161a3d3 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
index bd0b5a8ef59..72fec76659a 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c
index fddcff05b56..55a7f643816 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
char *__gen_e_acsl_literal_string_2;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
index 54d2758b54f..d2fccd6d110 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
index 4fba571813a..8dd92ddbabe 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
#include "stddef.h"
#include "stdio.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index 7262bebbeaf..fb21a5a91f6 100644
--- a/src/plugins/value/utils/library_functions.ml
+++ b/src/plugins/value/utils/library_functions.ml
@@ -71,7 +71,8 @@ let returned_value kf =
let unsupported_specifications =
- [ "glob", "glob.c";
+ [ "asprintf", "stdio.c";
+ "glob", "glob.c";
"globfree", "glob.c";
"getaddrinfo", "netdb.c";
"getline", "stdio.c";
diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index 648e90041fe..b6d3abc6517 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/erroneous/printf.c:8: Warning: Multiple usage of flag '-'.
[variadic] tests/erroneous/printf.c:8: Warning:
Flag ' ' and conversion specififer e are not compatibles.
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index c18613a1f18..eef24bcc00f 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -26,6 +26,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/printf.c:37:
Translating call to printf to a call to the specialized version printf_va_1.
[variadic] tests/known/printf.c:38:
@@ -156,6 +158,7 @@
hashes[0..3] ∈ {35}
__retres ∈ {0}
/* Generated by Frama-C */
+#include "__fc_builtin.h"
#include "errno.h"
#include "inttypes.h"
#include "signal.h"
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index f4a8692821d..7ccc3cea381 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/printf_garbled_mix.c:7:
Translating call to printf to a call to the specialized version printf_va_1.
[eva] Analyzing a complete application starting at main
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index c20bf567f1b..6fb1d968c2e 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/printf_wrong_arity.c:8:
Translating call to printf to a call to the specialized version printf_va_1.
[variadic] tests/known/printf_wrong_arity.c:8: Warning:
@@ -38,6 +40,7 @@
.__fc_FILE_data ∈ [--..--]
__retres ∈ {0}
/* Generated by Frama-C */
+#include "__fc_builtin.h"
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
index 94e8f171ee2..60c107c9ea4 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/printf_wrong_pointers.c:14:
Translating call to printf to a call to the specialized version printf_va_1.
[variadic] tests/known/printf_wrong_pointers.c:15:
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index 96262a87b67..a235c4ff5de 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
[variadic] tests/known/printf_wrong_types.c:19:
@@ -426,6 +428,8 @@ int main(void)
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
[variadic] tests/known/printf_wrong_types.c:19:
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
index f32b5df9f60..cfb401fc439 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/scanf.c:7:
Translating call to scanf to a call to the specialized version scanf_va_1.
[eva] Analyzing a complete application starting at main
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
index 972e7931d57..5f797ff74eb 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/scanf_loop.c:6:
Translating call to scanf to a call to the specialized version scanf_va_1.
[eva] Analyzing a complete application starting at main
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
index 84a91e7152a..1eb6ee4db02 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/scanf_wrong.c:8:
Translating call to scanf to a call to the specialized version scanf_va_1.
[variadic] tests/known/scanf_wrong.c:8: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index e570fee7f28..1aa67296258 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/snprintf.c:12:
Translating call to snprintf to a call to the specialized version snprintf_va_1.
[variadic] tests/known/snprintf.c:15:
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
index 5195bdb7c25..5cded5c9814 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/stdio_print.c:9: Warning:
Call to function fprintf with non-static format argument:
no specification will be generated.
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
index d1405ef465a..933132b0680 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -14,6 +14,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/stdio_scan.c:10: Warning:
Call to function fscanf with non-static format argument:
no specification will be generated.
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index ceed1ffebc1..b86d9aef770 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -26,6 +26,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/swprintf.c:12:
Translating call to swprintf to a call to the specialized version swprintf_va_1.
[variadic] tests/known/swprintf.c:15:
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index c9a23135ec5..eb195f46475 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -26,6 +26,8 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:590:
+ Declaration of variadic function asprintf.
[variadic] tests/known/wchar.c:11:
Translating call to wprintf to a call to the specialized version wprintf_va_1.
[variadic] tests/known/wchar.c:12:
diff --git a/tests/builtins/oracle/linked_list.0.res.oracle b/tests/builtins/oracle/linked_list.0.res.oracle
index 603208eb3a1..6d87dc3d346 100644
--- a/tests/builtins/oracle/linked_list.0.res.oracle
+++ b/tests/builtins/oracle/linked_list.0.res.oracle
@@ -18,6 +18,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -60,6 +61,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -98,6 +100,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -139,6 +142,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -179,6 +183,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -223,6 +228,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -265,6 +271,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -311,6 +318,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -355,6 +363,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -403,6 +412,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -449,6 +459,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -499,6 +510,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -791,6 +803,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -1085,6 +1098,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -1375,6 +1389,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -1669,6 +1684,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -1960,6 +1976,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
@@ -2255,6 +2272,7 @@
__fc_tmpnam[0..2047] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_random48_init ∈ {0}
diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index 33e86c7f82e..2171112cc9e 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -18,6 +18,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -60,6 +61,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -98,6 +100,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -139,6 +142,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -179,6 +183,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -223,6 +228,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -265,6 +271,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -311,6 +318,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -355,6 +363,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -403,6 +412,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -450,6 +460,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -501,6 +512,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -547,6 +559,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -591,6 +604,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -631,6 +645,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -675,6 +690,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -718,6 +734,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -761,6 +778,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
diff --git a/tests/builtins/oracle/linked_list.2.res.oracle b/tests/builtins/oracle/linked_list.2.res.oracle
index ed887dca2d5..794283f4aeb 100644
--- a/tests/builtins/oracle/linked_list.2.res.oracle
+++ b/tests/builtins/oracle/linked_list.2.res.oracle
@@ -18,6 +18,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -60,6 +61,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -97,6 +99,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -138,6 +141,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -178,6 +182,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -222,6 +227,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -264,6 +270,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -310,6 +317,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -354,6 +362,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -402,6 +411,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -448,6 +458,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -498,6 +509,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -546,6 +558,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -598,6 +611,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -648,6 +662,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -702,6 +717,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -754,6 +770,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -810,6 +827,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -864,6 +882,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
@@ -922,6 +941,7 @@
__fc_tmpnam[0..0x7FF] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
__fc_random48_init ∈ {0}
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index eb9d1531fcf..8961e153e8a 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1163,6 +1163,9 @@
[ Valid ] Axiomatic 'WcsNCmp'
axiomatic WcsNCmp
by Frama-C kernel.
+[ Valid ] Axiomatic 'dynamic_allocation'
+ axiomatic dynamic_allocation
+ by Frama-C kernel.
[ Valid ] Axiomatic 'format_length'
axiomatic format_length
by Frama-C kernel.
@@ -1190,6 +1193,9 @@
[ Extern ] Axiom 'memset_def'
axiom memset_def
Unverifiable but considered Valid.
+[ Extern ] Axiom 'never_allocable'
+ axiom never_allocable
+ Unverifiable but considered Valid.
[ Extern ] Axiom 'strchr_def'
axiom strchr_def
Unverifiable but considered Valid.
@@ -2347,6 +2353,36 @@
default behavior
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function 'asprintf'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'result_error_or_written_byes'
+ ensures
+ result_error_or_written_byes: \result ≡ -1 ∨ \result ≥ 0
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 593)
+ assigns __fc_heap_status, \result, *strp;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 593)
+ assigns __fc_heap_status
+ \from (indirect: *(fmt + (0 ..))), __fc_heap_status;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 594)
+ assigns \result
+ \from (indirect: *(fmt + (0 ..))), (indirect: __fc_heap_status);
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 595)
+ assigns *strp
+ \from *(fmt + (0 ..)), (indirect: __fc_heap_status);
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+[ Extern ] Frees/Allocates nothing/(file share/libc/stdio.h, line 598)
+ allocates *\old(strp);
+ Unverifiable but considered Valid.
+
--------------------------------------------------------------------------------
--- Properties of Function '__fc_fpclassifyf'
--------------------------------------------------------------------------------
@@ -4394,9 +4430,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 191 Completely validated
+ 193 Completely validated
16 Locally validated
- 556 Considered valid
+ 563 Considered valid
56 To be validated
- 819 Total
+ 828 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 52ea02c4ae3..881040218e6 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 (99)
- ======================
+[metrics] Defined functions (100)
+ =======================
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 (16 calls); Frama_C_make_unknown (5 calls);
+ Frama_C_interval (17 calls); Frama_C_make_unknown (6 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);
@@ -25,16 +25,17 @@
argz_count (0 call); argz_create (0 call); argz_create_sep (0 call);
argz_delete (0 call); argz_extract (0 call); argz_insert (0 call);
argz_next (1 call); argz_replace (0 call); argz_stringify (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);
- isblank (0 call); iscntrl (0 call); isdigit (3 calls); isgraph (0 call);
- 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 (5 calls); memmove (3 calls);
- memoverlap (1 call); mempcpy (1 call); memrchr (0 call); memset (1 call);
+ asprintf (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); isblank (0 call);
+ iscntrl (0 call); isdigit (3 calls); isgraph (0 call); 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 (5 calls); memmove (3 calls); memoverlap (1 call);
+ mempcpy (1 call); memrchr (0 call); memset (1 call);
posix_memalign (0 call); putenv (0 call); realpath (0 call);
res_search (1 call); setenv (0 call); setlocale (0 call); stpcpy (1 call);
str_append (3 calls); strcasecmp (0 call); strcat (0 call);
@@ -122,7 +123,7 @@
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); lseek (0 call); lstat (0 call);
- makedev (0 call); malloc (12 calls); mblen (0 call); mbstowcs (0 call);
+ makedev (0 call); malloc (13 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);
@@ -195,18 +196,18 @@
Global metrics
==============
- Sloc = 1460
- Decision point = 270
+ Sloc = 1472
+ Decision point = 271
Global variables = 86
- If = 255
+ If = 256
Loop = 55
- Goto = 112
- Assignment = 618
- Exit point = 99
- Function = 526
- Function call = 141
- Pointer dereferencing = 249
- Cyclomatic complexity = 369
+ Goto = 113
+ Assignment = 625
+ Exit point = 100
+ Function = 527
+ Function call = 144
+ Pointer dereferencing = 254
+ Cyclomatic complexity = 371
[kernel] share/libc/sys/socket.h:451: Warning:
clause with '\initialized' must contain name 'initialization'
/* Generated by Frama-C */
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 1cf9de7928f..c794e4be1b1 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -5630,6 +5630,8 @@ extern int pclose(FILE *stream);
ssize_t getline(char **lineptr, size_t *n, FILE *stream);
+int asprintf(char **strp, char const *fmt, void * const *__va_params);
+
/*@ assigns \result;
assigns \result \from maj, min; */
extern dev_t makedev(int maj, int min);
@@ -5740,6 +5742,36 @@ ssize_t getline(char **lineptr, size_t *n, FILE *stream)
return_label: return __retres;
}
+/*@ requires valid_strp: \valid(strp);
+ requires valid_fmt: valid_read_string(fmt);
+ ensures result_error_or_written_byes: \result ≡ -1 ∨ \result ≥ 0;
+ assigns __fc_heap_status, \result, *strp;
+ assigns __fc_heap_status
+ \from (indirect: *(fmt + (0 ..))), __fc_heap_status;
+ assigns \result
+ \from (indirect: *(fmt + (0 ..))), (indirect: __fc_heap_status);
+ assigns *strp \from *(fmt + (0 ..)), (indirect: __fc_heap_status);
+ allocates *\old(strp);
+ */
+int asprintf(char **strp, char const *fmt, void * const *__va_params)
+{
+ int __retres;
+ va_list args;
+ int tmp;
+ args = __va_params;
+ tmp = Frama_C_interval(1,256);
+ size_t len = (unsigned int)tmp;
+ *strp = (char *)malloc(len);
+ if (! *strp) {
+ __retres = -1;
+ goto return_label;
+ }
+ Frama_C_make_unknown(*strp,len - 1U);
+ *(*strp + (len - 1U)) = (char)0;
+ __retres = (int)len;
+ return_label: return __retres;
+}
+
/*@ requires abs_representable: i > -2147483647 - 1;
assigns \result;
assigns \result \from i;
diff --git a/tests/libc/oracle/stdio_c.res.oracle b/tests/libc/oracle/stdio_c.res.oracle
index 06ba2405258..97998c985f7 100644
--- a/tests/libc/oracle/stdio_c.res.oracle
+++ b/tests/libc/oracle/stdio_c.res.oracle
@@ -3,277 +3,322 @@
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-
+ nondet ∈ [--..--]
[eva] computing for function fopen <- main.
- Called from tests/libc/stdio_c.c:11.
+ Called from tests/libc/stdio_c.c:12.
[eva] using specification for function fopen
-[eva] tests/libc/stdio_c.c:11:
+[eva] tests/libc/stdio_c.c:12:
function fopen: precondition 'valid_filename' got status valid.
-[eva] tests/libc/stdio_c.c:11:
+[eva] tests/libc/stdio_c.c:12:
function fopen: precondition 'valid_mode' got status valid.
[eva] Done for function fopen
[eva] computing for function getline <- main.
- Called from tests/libc/stdio_c.c:13.
+ Called from tests/libc/stdio_c.c:14.
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:46.
+ Called from share/libc/stdio.c:47.
[eva] using specification for function ferror
-[eva] share/libc/stdio.c:46:
+[eva] share/libc/stdio.c:47:
function ferror: precondition 'valid_stream' got status valid.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:46.
+ Called from share/libc/stdio.c:47.
[eva] using specification for function feof
-[eva] share/libc/stdio.c:46:
+[eva] share/libc/stdio.c:47:
function feof: precondition 'valid_stream' got status valid.
[eva] Done for function feof
-[eva] share/libc/stdio.c:51: Call to builtin malloc
-[eva] share/libc/stdio.c:51: allocating variable __malloc_getline_l51
+[eva] share/libc/stdio.c:52: Call to builtin malloc
+[eva] share/libc/stdio.c:52: allocating variable __malloc_getline_l52
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
-[eva] share/libc/stdio.c:60:
+ Called from share/libc/stdio.c:61.
+[eva] share/libc/stdio.c:61:
function ferror: precondition 'valid_stream' got status valid.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
-[eva] share/libc/stdio.c:60:
+ Called from share/libc/stdio.c:61.
+[eva] share/libc/stdio.c:61:
function feof: precondition 'valid_stream' got status valid.
[eva] Done for function feof
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] using specification for function fgetc
-[eva] share/libc/stdio.c:62:
+[eva] share/libc/stdio.c:63:
function fgetc: precondition 'valid_stream' got status valid.
[eva] Done for function fgetc
-[eva:alarm] share/libc/stdio.c:68: Warning:
+[eva:alarm] share/libc/stdio.c:69: Warning:
out of bounds write. assert \valid(*lineptr + tmp_2);
(tmp_2 from cur++)
-[eva] share/libc/stdio.c:61: starting to merge loop iterations
+[eva] share/libc/stdio.c:62: starting to merge loop iterations
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
-[eva] share/libc/stdio.c:82: Call to builtin realloc
-[eva] share/libc/stdio.c:82:
+[eva] share/libc/stdio.c:83: Call to builtin realloc
+[eva] share/libc/stdio.c:83:
function realloc: precondition 'freeable' got status valid.
-[eva] share/libc/stdio.c:82: allocating variable __realloc_getline_l82
-[eva] share/libc/stdio.c:60: starting to merge loop iterations
+[eva] share/libc/stdio.c:83: allocating variable __realloc_getline_l83
+[eva] share/libc/stdio.c:61: starting to merge loop iterations
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
-[eva] share/libc/stdio.c:82: Call to builtin realloc
+[eva] share/libc/stdio.c:83: Call to builtin realloc
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
-[eva] share/libc/stdio.c:82: Call to builtin realloc
+[eva] share/libc/stdio.c:83: Call to builtin realloc
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
-[eva] share/libc/stdio.c:82: Call to builtin realloc
+[eva] share/libc/stdio.c:83: Call to builtin realloc
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
-[eva] share/libc/stdio.c:82: Call to builtin realloc
+[eva] share/libc/stdio.c:83: Call to builtin realloc
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
-[eva:alarm] share/libc/stdio.c:71: Warning:
+[eva:alarm] share/libc/stdio.c:72: Warning:
out of bounds write. assert \valid(*lineptr + cur);
[eva] Recording results for getline
[eva] Done for function getline
-[eva:alarm] tests/libc/stdio_c.c:14: Warning:
- assertion 'read_ok' got status unknown.
-[eva] tests/libc/stdio_c.c:15: Call to builtin strlen
[eva:alarm] tests/libc/stdio_c.c:15: Warning:
- function strlen: precondition 'valid_string_s' got status unknown.
+ assertion 'read_ok' got status unknown.
+[eva] tests/libc/stdio_c.c:16: Call to builtin strlen
[eva:alarm] tests/libc/stdio_c.c:16: Warning:
- assertion 'read_bytes' got status unknown.
+ function strlen: precondition 'valid_string_s' got status unknown.
[eva:alarm] tests/libc/stdio_c.c:17: Warning:
+ assertion 'read_bytes' got status unknown.
+[eva:alarm] tests/libc/stdio_c.c:18: Warning:
assertion 'allocated_enough' got status unknown.
-[eva] tests/libc/stdio_c.c:13: starting to merge loop iterations
+[eva] tests/libc/stdio_c.c:14: starting to merge loop iterations
[eva] computing for function getline <- main.
- Called from tests/libc/stdio_c.c:13.
+ Called from tests/libc/stdio_c.c:14.
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:46.
+ Called from share/libc/stdio.c:47.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:46.
+ Called from share/libc/stdio.c:47.
[eva] Done for function feof
-[eva] share/libc/stdio.c:51: Call to builtin malloc
+[eva] share/libc/stdio.c:52: Call to builtin malloc
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
-[eva] share/libc/stdio.c:82: Call to builtin realloc
+[eva] share/libc/stdio.c:83: Call to builtin realloc
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
[eva] Recording results for getline
[eva] Done for function getline
-[eva] tests/libc/stdio_c.c:15: Call to builtin strlen
+[eva] tests/libc/stdio_c.c:16: Call to builtin strlen
[eva] computing for function getline <- main.
- Called from tests/libc/stdio_c.c:13.
+ Called from tests/libc/stdio_c.c:14.
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:46.
+ Called from share/libc/stdio.c:47.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:46.
+ Called from share/libc/stdio.c:47.
[eva] Done for function feof
-[eva] share/libc/stdio.c:51: Call to builtin malloc
+[eva] share/libc/stdio.c:52: Call to builtin malloc
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
-[eva] share/libc/stdio.c:82: Call to builtin realloc
+[eva] share/libc/stdio.c:83: Call to builtin realloc
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
[eva] Recording results for getline
[eva] Done for function getline
-[eva] tests/libc/stdio_c.c:15: Call to builtin strlen
+[eva] tests/libc/stdio_c.c:16: Call to builtin strlen
[eva] computing for function getline <- main.
- Called from tests/libc/stdio_c.c:13.
+ Called from tests/libc/stdio_c.c:14.
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:46.
+ Called from share/libc/stdio.c:47.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:46.
+ Called from share/libc/stdio.c:47.
[eva] Done for function feof
-[eva] share/libc/stdio.c:51: Call to builtin malloc
+[eva] share/libc/stdio.c:52: Call to builtin malloc
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
[eva] computing for function fgetc <- getline <- main.
- Called from share/libc/stdio.c:62.
+ Called from share/libc/stdio.c:63.
[eva] Done for function fgetc
-[eva] share/libc/stdio.c:82: Call to builtin realloc
+[eva] share/libc/stdio.c:83: Call to builtin realloc
[eva] computing for function ferror <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
- Called from share/libc/stdio.c:60.
+ Called from share/libc/stdio.c:61.
[eva] Done for function feof
[eva] Recording results for getline
[eva] Done for function getline
-[eva] tests/libc/stdio_c.c:15: Call to builtin strlen
-[eva] tests/libc/stdio_c.c:19: Call to builtin free
-[eva] tests/libc/stdio_c.c:19:
+[eva] tests/libc/stdio_c.c:16: Call to builtin strlen
+[eva] tests/libc/stdio_c.c:20: Call to builtin free
+[eva] tests/libc/stdio_c.c:20:
function free: precondition 'freeable' got status valid.
[eva] computing for function fclose <- main.
- Called from tests/libc/stdio_c.c:20.
+ Called from tests/libc/stdio_c.c:21.
[eva] using specification for function fclose
-[eva] tests/libc/stdio_c.c:20:
+[eva] tests/libc/stdio_c.c:21:
function fclose: precondition 'valid_stream' got status valid.
[eva] Done for function fclose
+[eva] computing for function asprintf <- main.
+ Called from tests/libc/stdio_c.c:28.
+[eva] computing for function Frama_C_interval <- asprintf <- main.
+ Called from share/libc/stdio.c:102.
+[eva] using specification for function Frama_C_interval
+[eva] share/libc/stdio.c:102:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] share/libc/stdio.c:103: Call to builtin malloc
+[eva] share/libc/stdio.c:103: allocating variable __malloc_asprintf_l103
+[eva] computing for function Frama_C_make_unknown <- asprintf <- main.
+ Called from share/libc/stdio.c:109.
+[eva] using specification for function Frama_C_make_unknown
+[eva:alarm] share/libc/stdio.c:109: Warning:
+ function Frama_C_make_unknown: precondition 'valid_p' got status unknown.
+[eva] Done for function Frama_C_make_unknown
+[eva:alarm] share/libc/stdio.c:110: Warning:
+ out of bounds write. assert \valid(*strp + (unsigned int)(len - 1U));
+[eva] Recording results for asprintf
+[eva] Done for function asprintf
+[eva] computing for function printf_va_1 <- main.
+ Called from tests/libc/stdio_c.c:30.
+[eva] using specification for function printf_va_1
+[eva:alarm] tests/libc/stdio_c.c:30: Warning:
+ function printf_va_1: precondition valid_read_string(param0) got status unknown.
+[eva] tests/libc/stdio_c.c:30:
+ function printf_va_1: precondition valid_read_string(format) got status valid.
+[eva] Done for function printf_va_1
+[eva] tests/libc/stdio_c.c:31: Call to builtin free
+[eva] tests/libc/stdio_c.c:31:
+ function free: precondition 'freeable' got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function asprintf:
+ __fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
+ args ∈ {{ &__va_args[0] }}
+ len ∈ [1..256]
+ s ∈ {{ NULL ; &__malloc_asprintf_l103[0] }}
+ __retres ∈ [-1..256]
+ __malloc_asprintf_l103[0..254] ∈ [--..--] or UNINITIALIZED
+ [255] ∈ {0} or UNINITIALIZED
[eva:final-states] Values at end of function getline:
__fc_heap_status ∈ [--..--]
__fc_errno ∈ [--..--]
__fc_fopen[0..15] ∈ [--..--]
cur ∈ [0..2147483647]
line ∈
- {{ NULL ; &__malloc_w_getline_l51[0] ; &__realloc_w_getline_l82[0] }}
+ {{ NULL ; &__malloc_w_getline_l52[0] ; &__realloc_w_getline_l83[0] }}
len ∈ [0..2147483647]
__retres ∈ [-1..2147483646]
- __malloc_w_getline_l51[0..1] ∈ [--..--] or UNINITIALIZED
- __realloc_w_getline_l82[0..2147483645] ∈ [--..--] or UNINITIALIZED
+ __malloc_w_getline_l52[0..1] ∈ [--..--] or UNINITIALIZED
+ __realloc_w_getline_l83[0..2147483645] ∈ [--..--] or UNINITIALIZED
[2147483646] ∈ {0} or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
__fc_errno ∈ [--..--]
__fc_fopen[0..15] ∈ [--..--]
+ __fc_initial_stdout.__fc_FILE_id ∈ {1}
+ .__fc_FILE_data ∈ [--..--]
stream ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
line ∈
- {{ NULL ; &__malloc_w_getline_l51[0] ; &__realloc_w_getline_l82[0] }} or ESCAPINGADDR
+ {{ NULL ; &__malloc_w_getline_l52[0] ; &__realloc_w_getline_l83[0] }} or ESCAPINGADDR
len ∈ [0..2147483647]
total_len ∈ [--..--]
read ∈ {-1} or UNINITIALIZED
__retres ∈ {0; 1}
- __malloc_w_getline_l51[0..1] ∈ [--..--] or UNINITIALIZED
- __realloc_w_getline_l82[0..2147483645] ∈ [--..--] or UNINITIALIZED
+ __malloc_w_getline_l52[0..1] ∈ [--..--] or UNINITIALIZED
+ __realloc_w_getline_l83[0..2147483645] ∈ [--..--] or UNINITIALIZED
[2147483646] ∈ {0} or UNINITIALIZED
+ __malloc_asprintf_l103[0..254] ∈ [--..--] or UNINITIALIZED
+ [255] ∈ {0} or UNINITIALIZED
diff --git a/tests/libc/oracle/stdio_h.res.oracle b/tests/libc/oracle/stdio_h.res.oracle
index 3a64229e0e6..9029d4fbc09 100644
--- a/tests/libc/oracle/stdio_h.res.oracle
+++ b/tests/libc/oracle/stdio_h.res.oracle
@@ -137,12 +137,35 @@
[eva] tests/libc/stdio_h.c:49:
function fclose: precondition 'valid_stream' got status valid.
[eva] Done for function fclose
+[eva] computing for function asprintf <- main.
+ Called from tests/libc/stdio_h.c:52.
+[eva] using specification for function asprintf
+[eva:libc:unsupported-spec] tests/libc/stdio_h.c:52: Warning:
+ The specification of function 'asprintf' is currently not supported by Eva.
+ Consider adding 'share/libc/stdio.c' to the analyzed source files.
+[eva] tests/libc/stdio_h.c:52: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdio_h.c:52:
+ function asprintf: precondition 'valid_strp' got status valid.
+[eva] tests/libc/stdio_h.c:52:
+ function asprintf: precondition 'valid_fmt' got status valid.
+[eva] Done for function asprintf
+[eva:alarm] tests/libc/stdio_h.c:54: Warning:
+ accessing uninitialized left-value. assert \initialized(&s);
+[eva] computing for function printf_va_2 <- main.
+ Called from tests/libc/stdio_h.c:54.
+[eva] using specification for function printf_va_2
+[eva:alarm] tests/libc/stdio_h.c:54: Warning:
+ function printf_va_2: precondition valid_read_string(param0) got status invalid.
+[eva] tests/libc/stdio_h.c:54:
+ function printf_va_2: no state left, precondition valid_read_string(format) got status valid.
+[eva] Done for function printf_va_2
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__fc_errno ∈ [--..--]
__fc_fopen[0..15] ∈ [--..--]
+ __fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
f ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
r ∈ [--..--]
@@ -154,5 +177,6 @@
fgets_res ∈ {{ NULL ; &fgets_buf0[0] }}
pos ∈ [--..--] or UNINITIALIZED
res_fclose ∈ {-1; 0}
- __retres ∈ {0; 1; 2; 3}
+ s ∈ [--..--] or UNINITIALIZED
+ __retres ∈ {1; 2; 3}
S___fc_stdout[0..1] ∈ [--..--]
diff --git a/tests/libc/stdio_c.c b/tests/libc/stdio_c.c
index 1459a645ab9..29374afba20 100644
--- a/tests/libc/stdio_c.c
+++ b/tests/libc/stdio_c.c
@@ -1,7 +1,8 @@
#include <stdlib.h>
#include <string.h>
#include "stdio.c"
-
+#include "__fc_builtin.h"
+volatile int nondet;
int main() {
FILE *stream;
char *line = NULL;
@@ -18,5 +19,17 @@ int main() {
}
free(line);
fclose(stream);
+
+ if (nondet) {
+ // Test asprintf without a C stub; the specification
+ // uses an unsupported 'allocates' clause, so 's' will
+ // point to invalid memory.
+ char *s;
+ int r = asprintf(&s, "bla %s", 42);
+ if (r == -1) return 1;
+ printf("%s", s);
+ free(s);
+ }
+
return 0;
}
diff --git a/tests/libc/stdio_h.c b/tests/libc/stdio_h.c
index 19531ca2e40..0ee459dfb20 100644
--- a/tests/libc/stdio_h.c
+++ b/tests/libc/stdio_h.c
@@ -1,6 +1,6 @@
#include <stdio.h>
+#include <stdlib.h>
#include "__fc_builtin.h"
-
volatile int nondet;
int main() {
FILE *f = fopen("/dev/urandom", "r");
@@ -47,5 +47,12 @@ int main() {
fsetpos(f, &pos);
int res_fclose = fclose(f);
+
+ char *s;
+ r = asprintf(&s, "bla %s", 42);
+ if (r == -1) return 1;
+ printf("%s", s);
+ free(s);
+
return 0;
}
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index 81dff3785c2..a57305d1570 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -4,20 +4,20 @@
bar (1 call); f (0 call); foo (1 call); g (address taken) (0 call);
getopt (1 call); h (1 call); main (0 call);
- Specified-only functions (123)
+ Specified-only functions (124)
==============================
- _exit (0 call); access (0 call); chdir (0 call); chown (0 call);
- chroot (0 call); clearerr (0 call); clearerr_unlocked (0 call);
- close (0 call); dup (0 call); dup2 (0 call); execl (0 call);
- execle (0 call); execlp (0 call); execv (0 call); execve (0 call);
- execvp (0 call); fclose (0 call); fdopen (0 call); feof (0 call);
- feof_unlocked (0 call); ferror (0 call); ferror_unlocked (0 call);
- fflush (0 call); fgetc (0 call); fgetpos (0 call); fgets (0 call);
- fileno (0 call); fileno_unlocked (0 call); flockfile (0 call);
- fopen (0 call); fork (0 call); fputc (0 call); fputs (0 call);
- fread (0 call); freopen (0 call); fseek (0 call); fseeko (0 call);
- fsetpos (0 call); ftell (0 call); ftello (0 call); ftrylockfile (0 call);
- funlockfile (0 call); fwrite (0 call); getc (0 call);
+ _exit (0 call); access (0 call); asprintf (0 call); chdir (0 call);
+ chown (0 call); chroot (0 call); clearerr (0 call);
+ clearerr_unlocked (0 call); close (0 call); dup (0 call); dup2 (0 call);
+ execl (0 call); execle (0 call); execlp (0 call); execv (0 call);
+ execve (0 call); execvp (0 call); fclose (0 call); fdopen (0 call);
+ feof (0 call); feof_unlocked (0 call); ferror (0 call);
+ ferror_unlocked (0 call); fflush (0 call); fgetc (0 call); fgetpos (0 call);
+ fgets (0 call); fileno (0 call); fileno_unlocked (0 call);
+ flockfile (0 call); fopen (0 call); fork (0 call); fputc (0 call);
+ fputs (0 call); fread (0 call); freopen (0 call); fseek (0 call);
+ fseeko (0 call); fsetpos (0 call); ftell (0 call); ftello (0 call);
+ ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call); getc (0 call);
getc_unlocked (0 call); getchar (1 call); getchar_unlocked (0 call);
getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
gethostname (0 call); getopt_long (0 call); getopt_long_only (0 call);
@@ -44,10 +44,10 @@
=======================================
- 'Extern' global variables (10)
+ 'Extern' global variables (11)
==============================
- Frama_C_entropy_source; __fc_errno; __fc_hostname; __fc_stdin; __fc_stdout;
- __fc_ttyname; optarg; opterr; optind; optopt
+ Frama_C_entropy_source; __fc_errno; __fc_heap_status; __fc_hostname;
+ __fc_stdin; __fc_stdout; __fc_ttyname; optarg; opterr; optind; optopt
Potential entry points (2)
==========================
@@ -57,13 +57,13 @@
==============
Sloc = 20
Decision point = 0
- Global variables = 17
+ Global variables = 18
If = 0
Loop = 0
Goto = 0
Assignment = 9
Exit point = 7
- Function = 130
+ Function = 131
Function call = 8
Pointer dereferencing = 1
Cyclomatic complexity = 7
@@ -91,7 +91,7 @@
----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
- Syntactically reachable functions = 8 (out of 130)
+ Syntactically reachable functions = 8 (out of 131)
Semantically reached functions = 8
Coverage estimation = 100.0%
[metrics] References to non-analyzed functions
diff --git a/tests/metrics/oracle/libc.json b/tests/metrics/oracle/libc.json
index a6de1ef4b08..afe73bccdad 100644
--- a/tests/metrics/oracle/libc.json
+++ b/tests/metrics/oracle/libc.json
@@ -11,6 +11,7 @@
"specified-only-functions": [
{ "_exit": { "calls": 0, "address_taken": false } },
{ "access": { "calls": 0, "address_taken": false } },
+ { "asprintf": { "calls": 0, "address_taken": false } },
{ "chdir": { "calls": 0, "address_taken": false } },
{ "chown": { "calls": 0, "address_taken": false } },
{ "chroot": { "calls": 0, "address_taken": false } },
@@ -135,8 +136,9 @@
],
"undefined-functions": [],
"extern-global-vars": [
- "Frama_C_entropy_source", "__fc_errno", "__fc_hostname", "__fc_stdin",
- "__fc_stdout", "__fc_ttyname", "optarg", "opterr", "optind", "optopt"
+ "Frama_C_entropy_source", "__fc_errno", "__fc_heap_status",
+ "__fc_hostname", "__fc_stdin", "__fc_stdout", "__fc_ttyname", "optarg",
+ "opterr", "optind", "optopt"
],
"entry-points": [ "f", "main" ]
}
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index 83a5a5c7b21..537f8de5cf7 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -75,6 +75,8 @@
by Frama-C kernel.
[ Valid ] Axiomatic 'WcsNCmp'
by Frama-C kernel.
+[ Valid ] Axiomatic 'dynamic_allocation'
+ by Frama-C kernel.
[ Valid ] Axiomatic 'format_length'
by Frama-C kernel.
[ Valid ] Axiomatic 'pipe_streams'
@@ -93,6 +95,8 @@
Unverifiable but considered Valid.
[ Extern ] Axiom 'memset_def'
Unverifiable but considered Valid.
+[ Extern ] Axiom 'never_allocable'
+ Unverifiable but considered Valid.
[ Extern ] Axiom 'strchr_def'
Unverifiable but considered Valid.
[ Extern ] Axiom 'strcmp_zero'
@@ -897,6 +901,25 @@
[ Valid ] Default behavior
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function 'asprintf'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'result_error_or_written_byes'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 593)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 593)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 594)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 595)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+[ Extern ] Frees/Allocates nothing/(file share/libc/stdio.h, line 598)
+ Unverifiable but considered Valid.
+
--------------------------------------------------------------------------------
--- Properties of Function 'main'
--------------------------------------------------------------------------------
@@ -911,8 +934,8 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 74 Completely validated
- 214 Considered valid
+ 76 Completely validated
+ 221 Considered valid
1 To be validated
- 289 Total
+ 298 Total
--------------------------------------------------------------------------------
--
GitLab