diff --git a/share/libc/stdio.c b/share/libc/stdio.c
index 0da68a57ac73d70d2a47d102566a06265092dd14..bc46eb85673495caf49b0dba4e3594f8545a3318 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 93a5829898c63cfe07face63d45209f21d0fa60c..18fa5958b7c01c9fae757fdb3400d774b5be30f8 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 98fa261bf28779ec3281cb2665512daacf830a9c..d39f910421780a69e719773ae8c89af29530d051 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 7cabbe5457d673cff71272c39602a2a412fb9e0b..ce068ecad6e5e3dc9a3d90fd8deb6ad74acd3bfe 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 b5265e84689baf60970908ecedb04ac709995ca4..7553a951c4b52aaf9400d6577e9a93dd3e0e5d4a 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 347680631d643665984d1ea5c28e588ebcb70296..fd738aa7b4b03d0f062ee3a3e6d84032b9fb135e 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 877b80e482c482a7a2c1d36b722dbd24bc86764a..3f1cdbd82498918ba38a0ea29a2adb92c0169da4 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 7357e7cf32c657e690bac2196cd4806769376591..2ea404238aff80f36a69bb2a84125a597a386d27 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 a421b3f34be98f1262171bae25bb49543f502d90..0f0702660796a74f1fbd1999fcb8183ab7a63c73 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 c63917398ce804719d214b63f16611b26dde0abd..c90b243c08b820282bfe99606fabc72eac11e6ac 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 896c9741e9e3f85ef4c5b4514957d95dd66fefa9..54bd5b922db1f35431245daea4cb02c20ae03002 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 0dc365800f3a322f927c8f285959f3d817a014eb..5e13957ce560daff2d960978c5fa498bd00896b5 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 84bbc75c2b91cfd729292f295037c1e17932b0be..bd14370f572710c15132e2d91dabb069a4ff9fc3 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 b63ae684d46ef5ab3cadef73f01c492caee8fc48..42f39839d7871600dd9480a187537ec73c875f27 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 096a8cd3446a6c4be1db87566422c47b0b779115..bdfdae9e75ef7dcf2fb3e2a6e5ac1fdec59fd652 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 48a64c6fc1f12f9a9e8ff6a3ca0da7ece4f7ea23..f1d72daba9f0904a47d80254bdaf919b2a494d4e 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 e48f67cea87e6e8f109ef6f6fa0b083d176134e9..90b0651a11521588af3b3799ee98b8a02010c5a5 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 d09bb71f9945158f44c65cc538722160fff36bf2..a553f45a4423e9f96ccaef8deae944e4361dc3c3 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 ae624f3a5dd576f12551dbd56209bd9792c28713..762933f8fed7f20ae90e68b8b016ae87026769b0 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 00ea678bb6d8ce5b7a7da9d59f2d73b2d431333e..e50e4e0f0f1a4c6a8d156203d2ca0c30e8ad12c8 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 56cd19052034f1e10c443ca76f16b87fc0fcf5b5..8c7d12a1602c19079507484fd0419b37327805fd 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 3728e989aae62e7ec981e79fa5898e0524b17a2f..aa6edd56fa7dddc19ec5c7a78c4ffe0f97881415 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 c5b6665908d3ef321c781e0f937751855faea388..9755e8cd106f5a74c39689df65735c50ff024ad0 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 e4ce2b0300f7f706214481bd5aebe66730f3fdd7..68220ac9996606c8d648333cf04fb942bb7d1e31 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 506172e9b1b55c7d8dc362513d49d665fdce1319..e22850aba10b0f49c53415da9b086424d516621d 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 db165cf968b0feb27509a9dc850f350451db638a..f235a94655c43df645f7f898406274d5f66049dd 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 8693ba5674dc21b587de1116c5b1435728d596ba..235b00e3ce39f982b658a892f2b6c39bc4540062 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 9a2a7e9391158f898b1cba0ad1574b9f5c06437b..12837b756e42c9db9a7d9ec9d136bec4f93cbedb 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 72cbffe72fd40fbc12fa3e175543b6e7cb7afc47..248e0c5dac9a77836ed676ee647a64e8ba15dc1b 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 ad106a78c1acd219b8461c1b51e26c97c631c53e..71d5655e76f7283ef6b7fbb843c8725b835c3358 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 98da9b92aa86932c8548f21c13d7f5b071e1ccb9..68b811cf123a0c069ef8392ef08d26b80b9ed603 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 ce15aa2b174848339ca35b55c3edf23bd5f5b03f..b83815b665daf90d54ba40bef0923b97c7da0338 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 4a9f3921fd81ea700be58509c3bfa0b8b8d879f3..beb8f456827b957dd1ca4ea3e6612b0b11bd4349 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 eb8feac0bb5ce7b32232c4c7d5651544cf1378ee..3e6032ceff5d360da26a744d1e92abf383164fad 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 c14d3f8d10bbc266726a8691ce04c6bfa0351b7d..60838e80f0077118a75fd3c90152cd1d6a173af9 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 d4fccb9af3cf84d9d342d4e891e6c9d047425548..3005fdba28a0e7fde0476a544deb1cee8ad1c2aa 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 2c8298f36dcc6d763a4cc60d01d33974af5234ef..5a48d337504908d0c693c30fd49b517d85fb46a6 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 3afa85d098a2e38ed8d4238474cdf1b541f9240b..e5d36213c8486363a11a0192fd2b883a5b7122c2 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 a68b9bc741b31ab13eb9d5a949b3d22fdc9f8fc4..072539c22ae052daad7e7f24e6eeb21173da8bc6 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 5710f18fae1f99c0f94d96c19ee006036592be00..8d33325a01f4ce58d9de5e794582195de7b1d3f7 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 b6559e0ca88ee21fbfa019998a6a521e0d64e8c9..91b232c39ba10381933188988101853b64531d2a 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 dce9ccced14dcf95ee4f9d18d1121b4a399433fd..f3b0980fe6050cb156957fba63de14a803b15060 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 b393878b81667c3905f85884978ae39509f363f6..24396bfc82b95133eb8119e99c3557439a09461c 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 bcb111b2c7a7454321e6f8858e99600f9523ad47..c5762d971dea76d2d8ac74cdb935ff134fad1b8b 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 e7143f3c725aded195940c498f03c556c7d0d222..6136cebc45ed92fb5908b315bfd4e1c9ac6d7b2c 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 5c9168343d02d0da6625b806ee3adeff678b0d34..c9da90bf22f58c36bc929800e70643a7837c03f2 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 85b76ff45a64721d1e6e280f6ec5bba98b93658e..b6db66215dc340b85f2a80d4b0513ee6b6dde66a 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 22a773aa6be93bbf26a30a79f5001328a420f958..c29fe752eee1eb2062ee0411e5048892ab19d443 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 7077d948dbea1d2a06fa63448afb9a3a38a23086..19a1e3dfd46a540d6525445e25bfe3c1dc20d623 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 6fd64a10a3a0e8c9157213a3ac76e3f998448303..65d2e93785cd4c110da3196e18c56fa94552d3c2 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 a41944fff180adb068c69adb74532ab2a79c70de..f1091f95d9bb2e93247dfc7feeceefe4c63d93a8 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 3c90b94bef5d46b34a8e55f313501d1af4fa380a..99047ada7fce8801fa3da7a63e74f6ca77b965a4 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 2644fbaf96fa398d23a58dc7ae336b019cd6283e..029e81dbde948f4cf261e8fe0736c00e13f1fa9c 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 075893b1811697b6c34943deb8a84c1ab4fa5bf3..39cb8590d19d9d758c879547eb4b5409b448bca5 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 f0840ee5da6d4bc1b9178a8da68d46a9bd2c15e5..55615fb2891193cdd323ccc30fcafa30e54f960d 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 c329fa2981878b3f2d4ef2d0ebc0f6d680c54b56..fad68a23da5c81abb9763db0a88c4540ca598551 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 c547c88f2b3786ffc97a2844b28de2e5b0b85715..7fbeb0f748b24a2cb9280a40157a05478229cd85 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 8603a3791f0c798d405a2bb2427aab63c5dee226..4417657b8079620bf6c69cc60f6bdd9dc036687a 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 37c835510d0afd252ff79c46964fda3048a0a0f1..45bc00f263118febfab9bc1d789ef7e9e42e4b68 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 ebaf959d8bc3d5a0805104ae76e711e9049cb5b3..fa774f67e47d3a677ccb4e12762e46154c3d41a3 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 c27908a810ae4afeb3133a51443f953f0b1598e5..a27503d98f33e0ad1f9e31e6b310db1832d552b0 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 cccd91e3f09bc928795a0e758ee46b26b82f36d9..8c713255a9883ae0820182f496162daa1a888346 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 a803622c90b832f962381ee05cd470540ee4f480..a0dfc7325996cf9771b3fa9ef58887faca913c90 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 a72dcdf164931adbca303c4de06fa37ed6d65c50..77eb66c73434ef0a19ff2a79c1618a08e4cef21e 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 f73fcd60c90bc3d1f227f7343333c65872409051..c056a0c0b85eeb3ddc2fde3335ac14824a34261a 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 d653ef1b72cd342eedd3be2463fa125897925df7..3b0b106b9630d9abf94d2ffc232296da7e47f33d 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 f324cd6b7ebc5bf9e3c3fccf6cf0fed6f676683c..35129325096b543be203e72c0de69489c04968fd 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 f9916ddbab122006517ed7aa326b5f5075428cfb..45e92a3f5de25520a5d1439bf732ede4eb8b9164 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 2eb6d8431742c05ab00e309f0ab52bbd57ed3f8d..9cb1a440568a7e0ca7705ed7a03d799011c98684 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 97debe7067496c41e72d83021d6c520bfef6cc1d..123bf12d8a51831f1632b19ef1861568f048c60e 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 3a4ab987b63e5b69037c11eae9ff02bad1d2c87d..ade66b89b69aa12b1cbe00785131ad2555d32414 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 ee4f315c4e1a84ae3b1d9e380a4ecd9feece5ed5..70c0f2aa925bcdbfadf5d5a0109660312ec9ac9d 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 2c00fe4f0123d8e938d9c23e024aa61b4169cd55..276d86a0d821796532e160c41d7f467cd822b656 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 2ae93f0e98702ed7be0bdee03dbead5ad0a820e7..6162260111829a4c53f7ab287aeb99ef1ed8f4c9 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 3f3eb016471db26f2a2bd53d2d08d815b8ec1a6b..0eb3cefd4a8d80047a7020844f4ddd8d4ed066ef 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 94b5ca7fced84d99b2962d761dae2484f5fdfc81..375f0da012931441d10f4a33032c16acccb5d7a7 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 bdb06b362ea7fc1d2139e35fff28b3eb42e347fe..7de63880550589245145a85f4f5185e7d4e9deb2 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 4b7d6f59edd5e7d8248ce0cc155f8ef95f2dd407..3aadcd229f8b1c88013602b610b59b8b75255ca8 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 7f829ac63e5df4c4572c65e993be3e6e17f49838..04238dc3f425095bb6201e4823a9092509c6484e 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 76649cc1f80bb48ea6bafd00cfe0f5c5add09a48..db99b83114133ad4e8d0b79dc9dd0a944d921036 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 40a21f890be549217f97ce1769b183c1f25c6d05..a80a813054c76077f2d3027cf177897eeac77ecc 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 46e4f1c6e1263fd048fef601610db2db1befa0b8..72d97a54831c7c1dff3f9c7169b1fea2e5589388 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 59f62c0c1c0649b220ba956a3414a42bbac15bab..2f77399ecaa5a4d06eaa2187ba6d723f9cc485dc 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 5b7a9aa5a54c55c6da9021d3deb9049e90f50475..79d83f6e40dab17fa30344132cf90e4891a44645 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 be6541fd320ab55c658b6400776d7a39fc6a43fd..2a06979d910095fbf6dc6bc9d24b41cf29319230 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 59f62c0c1c0649b220ba956a3414a42bbac15bab..2f77399ecaa5a4d06eaa2187ba6d723f9cc485dc 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 46e4f1c6e1263fd048fef601610db2db1befa0b8..72d97a54831c7c1dff3f9c7169b1fea2e5589388 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 dfc3a961e287759cb75665bcf1d12a5be972ccf2..0324021b4b2ed6ab6d035ed2f388e2ba6056757d 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 d36bd64117041de0bed8f23049b35cd37b1471a2..17349b414867ebc57efc76abda167c3f1087dc35 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 5369d3c824ba8a6ca6391a0f6e0e32c453913bc3..26ac8e12f25ce50dd420654192056f455df54886 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 f7db119cba3c3dd19958d504cdf6c114d5d866fb..2dd226207fca2c2718cdea9646ee68554f5691c3 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 d17b4ca48cce23440f8ee48aa41a265dd230517b..5759e6ea84b71493b7f495f7554bd37bbb5f3edc 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 f682429dec874ab1b36025e84ebb041ea97f91c2..5206161a3d3e05c067842cd5b3d52fa7f86ca9d6 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 bd0b5a8ef59662fac86b1437bf4e4df12cdbf539..72fec76659a77a3aa1be7d0ed9597500503ccbce 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 fddcff05b56a1d384803849ac3223922986f0edf..55a7f643816a48caf304ba6d625c12f67541b7de 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 54d2758b54fd49d774b4dfe91a23215efd60bd1d..d2fccd6d110b8a6a5ea893322af2ca29f610d2b2 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 4fba571813a17b49f10b9f97e17d13f2a01bb565..8dd92ddbabe95047d7346030178dc49bb905e389 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 7262bebbeaf75a657a269943b180fd73499022fe..fb21a5a91f6cdbf509522b13d394901cedb616e4 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 648e90041fe3c2953176a9b9b26a7cb63d420214..b6d3abc651760355e2cf19a810e8d2c491a3a4f2 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 c18613a1f186d64f915f9db8fa71177a824dcda7..eef24bcc00fece4b8830274a7b0bef68d217dc8b 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 f4a8692821de3ba3ec72efdcd68c48facd4f7cff..7ccc3cea381b6dbddbd046ec63f3743cb8b4530e 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 c20bf567f1b4ab728d25c4bd5367fed1dd807dc2..6fb1d968c2e179894f336a9b5ed6fff7a4005f49 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 94e8f171ee2275f1b2d002cceb36e9505b5182d9..60c107c9ea4a744ae339ef3ee2a1fc4a06113fd6 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 96262a87b67497376f5f1d83f8f81dee8e406a59..a235c4ff5debe72fb396211dc2b4b3732b7a9fd5 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 f32b5df9f60c07f1d819cf06e896492469def5d7..cfb401fc43988a083c3d4cefad1133dc691bf93f 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 972e7931d57597e331d370f502670e38def9a140..5f797ff74eb81b1b2ef5490e2883f02ed1701d37 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 84a91e7152af473882c844d54525e9abeff70d4b..1eb6ee4db02866d89eaef2239992447b784ca24c 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 e570fee7f285c16b155128a31382aee776f0f526..1aa67296258877e1ba34c735495d2d2eb5f1121a 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 5195bdb7c25d106369eabb0dd894031e07d69bd5..5cded5c9814f6a691f524589f3da627d5cb8992c 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 d1405ef465a47f1c679095e6dd6885a90ed63b87..933132b068079dfb5faef71a4bd04a21f96f2acb 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 ceed1ffebc170828b83e370b702f66362998b732..b86d9aef77066befdda71fdf59dcb95c23faae2b 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 c9a23135ec5ecfdbf3841c0c247f8bce2df6ac11..eb195f464752259e8c06994aefbac804dca9dc2a 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 603208eb3a1d0e5fdbc85e3869bfac5956ba3ca9..6d87dc3d34679b2329e25d7194b3172176c72dc1 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 33e86c7f82e62adbecbe2f0ab3606f89e246fef4..2171112cc9efa4b012dc61f20ef798b97ecdc485 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 ed887dca2d5cbcb79ad0ec01cb49167aa08104f3..794283f4aebb1687fe705e6c5fc5005e02e73e62 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 eb9d1531fcfbd9c001b76a9946ccc398d95d516e..8961e153e8a3dc164e9c317028fc9f15e625bd8e 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 52ea02c4ae31933fef4f719db82c1493a10b18a3..881040218e6562ae1c75d17f17b57abbc7866064 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 1cf9de7928fa9e8efe8d3e4a9bb357bdf0a8e2b3..c794e4be1b1caaec773f9e4c3f342430a01ce82f 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 06ba2405258b9311bfeb5ca4f73196a063806ca0..97998c985f7af5a2ef375c9e26f7271c8f8d4dbf 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 3a64229e0e65255d3fede1f6f5d07dd7f5000489..9029d4fbc09bc183b8b26cae1c618666f518ac1b 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 1459a645ab99d033b625c5a36651ce0767070836..29374afba20aa72e7abdb1b3ab4a0d7eadcec96f 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 19531ca2e4042e831ad5e57a50d19311687910a3..0ee459dfb20e3ce23bae574ab0bea389599271bd 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 81dff3785c2b1652942601044ed27093a3858cc1..a57305d1570190ba61230b014b4c0bec1da423ae 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 a6de1ef4b0825780204b04cccd14a34ef61ddacc..afe73bccdad6b27be86cc5b509fb01fda44e6ce4 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 83a5a5c7b2168e4db1cd0fdb406364b51427d35b..537f8de5cf76db210c12605910bff1904c2e8ac3 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
 --------------------------------------------------------------------------------