diff --git a/tests/builtins/oracle/Longinit_sequencer.res.oracle b/tests/builtins/oracle/Longinit_sequencer.res.oracle
index 7593544dbd939e453a2870b1e76c873fc147295a..c07049acaa7e5c069d9802a28b3ea799f330be44 100644
--- a/tests/builtins/oracle/Longinit_sequencer.res.oracle
+++ b/tests/builtins/oracle/Longinit_sequencer.res.oracle
@@ -67,13 +67,11 @@
 [eva] Done for function subanalyze
 [eva] Recording results for analyze
 [eva] Done for function analyze
-[eva] tests/builtins/long_init.c:73: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/long_init.c:73: Call to builtin malloc
 [eva] tests/builtins/long_init.c:73: allocating variable __malloc_init_inner_l73
 [eva:alarm] tests/builtins/long_init.c:74: Warning: 
   pointer downcast. assert (unsigned int)alloc1 ≤ 2147483647;
-[eva] tests/builtins/long_init.c:75: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/long_init.c:75: Call to builtin malloc
 [eva] tests/builtins/long_init.c:75: allocating variable __malloc_init_inner_l75
 [eva] tests/builtins/long_init.c:77: Call to builtin free
 [eva] tests/builtins/long_init.c:77: 
@@ -162,8 +160,7 @@
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/long_init.c:103: 
   strong free on bases: {__malloc_init_inner_l73}
-[eva] tests/builtins/long_init.c:104: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/long_init.c:104: Call to builtin malloc
 [eva] tests/builtins/long_init.c:104: allocating variable __malloc_main_l104
 [eva] Recording results for main
 [eva] done for function main
@@ -434,8 +431,7 @@ Values at end of function main:
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/long_init2.c:103: 
   strong free on bases: {__malloc_init_inner_l73}
-[eva] tests/builtins/long_init2.c:104: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/long_init2.c:104: Call to builtin malloc
 [eva] tests/builtins/long_init2.c:104: allocating variable __malloc_main_l104
 [eva] Recording results for main
 [eva] done for function main
@@ -667,8 +663,7 @@ Values at end of function main:
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/long_init3.c:103: 
   strong free on bases: {__malloc_init_inner_l73}
-[eva] tests/builtins/long_init3.c:104: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/long_init3.c:104: Call to builtin malloc
 [eva] tests/builtins/long_init3.c:104: allocating variable __malloc_main_l104
 [eva] Recording results for main
 [eva] done for function main
diff --git a/tests/builtins/oracle/alloc.0.res.oracle b/tests/builtins/oracle/alloc.0.res.oracle
index b124e2220d17a6d8a85d3bb9dc74b91e716d5a75..9eb3d72cf3c8e053b93afcad8b11c1c369edd771 100644
--- a/tests/builtins/oracle/alloc.0.res.oracle
+++ b/tests/builtins/oracle/alloc.0.res.oracle
@@ -12,9 +12,9 @@
   u ∈ {0}
   v ∈ {0}
   ch ∈ {44}
-[eva] tests/builtins/alloc.c:16: Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/alloc.c:16: Call to builtin malloc
 [eva] tests/builtins/alloc.c:16: allocating variable __malloc_main_l16
-[eva] tests/builtins/alloc.c:17: Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/alloc.c:17: Call to builtin malloc
 [eva] tests/builtins/alloc.c:17: allocating variable __malloc_main_l17
 [eva:alarm] tests/builtins/alloc.c:18: Warning: 
   out of bounds write. assert \valid(p + (int)(-1));
@@ -32,7 +32,7 @@
   out of bounds write. assert \valid(t + 10);
 [kernel] tests/builtins/alloc.c:21: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
-[eva] tests/builtins/alloc.c:25: Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/alloc.c:25: Call to builtin malloc
 [eva] tests/builtins/alloc.c:25: allocating variable __malloc_main_l25
 [eva:alarm] tests/builtins/alloc.c:26: Warning: 
   pointer downcast. assert (unsigned int)q ≤ 2147483647;
@@ -47,9 +47,9 @@
   out of bounds write. assert \valid(r);
 [eva:alarm] tests/builtins/alloc.c:27: Warning: 
   out of bounds read. assert \valid_read(r + 1);
-[eva] tests/builtins/alloc.c:32: Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/alloc.c:32: Call to builtin malloc
 [eva] tests/builtins/alloc.c:32: allocating variable __malloc_main_l32
-[eva] tests/builtins/alloc.c:33: Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/alloc.c:33: Call to builtin malloc
 [eva] tests/builtins/alloc.c:33: allocating variable __malloc_main_l33
 [eva:alarm] tests/builtins/alloc.c:34: Warning: 
   out of bounds write. assert \valid(u);
@@ -116,12 +116,12 @@
   __malloc_main_l33[0] ∈ {35}
                    [1] ∈ {36}
 [from] Computing for function main
-[from] Computing for function Frama_C_malloc_fresh <-main
-[from] Done for function Frama_C_malloc_fresh
+[from] Computing for function malloc <-main
+[from] Done for function malloc
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_malloc_fresh:
+[from] Function malloc:
   __fc_heap_status FROM __fc_heap_status; size (and SELF)
   \result FROM __fc_heap_status; size
 [from] Function main:
diff --git a/tests/builtins/oracle/alloc.1.res.oracle b/tests/builtins/oracle/alloc.1.res.oracle
index 48c4356d116b6568051f121123841c9f5b03d047..26a82d1c76ca9ed9c70ab322c8c31b02d776ea00 100644
--- a/tests/builtins/oracle/alloc.1.res.oracle
+++ b/tests/builtins/oracle/alloc.1.res.oracle
@@ -13,7 +13,7 @@
   u ∈ {0}
   v ∈ {0}
   ch ∈ {44}
-[eva] tests/builtins/alloc.c:50: Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/alloc.c:50: Call to builtin malloc
 [eva] tests/builtins/alloc.c:50: allocating variable __malloc_main_abs_l50
 [eva:alarm] tests/builtins/alloc.c:51: Warning: 
   pointer downcast. assert (unsigned int)q ≤ 2147483647;
@@ -46,12 +46,12 @@
   __malloc_main_abs_l50 ∈
                        {{ NULL + [1..510] ; &__malloc_main_abs_l50 + {1} }}
 [from] Computing for function main_abs
-[from] Computing for function Frama_C_malloc_fresh <-main_abs
-[from] Done for function Frama_C_malloc_fresh
+[from] Computing for function malloc <-main_abs
+[from] Done for function malloc
 [from] Done for function main_abs
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_malloc_fresh:
+[from] Function malloc:
   __fc_heap_status FROM __fc_heap_status; size (and SELF)
   \result FROM __fc_heap_status; size
 [from] Function main_abs:
diff --git a/tests/builtins/oracle/allocated.1.res.oracle b/tests/builtins/oracle/allocated.1.res.oracle
index 0a5410846375e6424c9544508acbe145bab980e4..466af99615c47095ab32663de7dd8db25ebd535c 100644
--- a/tests/builtins/oracle/allocated.1.res.oracle
+++ b/tests/builtins/oracle/allocated.1.res.oracle
@@ -4,8 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
-[eva] tests/builtins/allocated.c:25: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:25: Call to builtin malloc
 [eva] tests/builtins/allocated.c:25: allocating variable __malloc_main_l25
 [eva] tests/builtins/allocated.c:25: assertion got status valid.
 [eva:alarm] tests/builtins/allocated.c:27: Warning: 
@@ -21,8 +20,7 @@
 [eva:malloc] tests/builtins/allocated.c:31: 
   strong free on bases: {__malloc_main_l25}
 [eva] tests/builtins/allocated.c:32: Frama_C_show_each_p_after_free: Bottom
-[eva] tests/builtins/allocated.c:36: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:36: Call to builtin malloc
 [eva] tests/builtins/allocated.c:36: allocating variable __malloc_main_l36
 [eva] tests/builtins/allocated.c:36: assertion got status valid.
 [eva] tests/builtins/allocated.c:40: 
@@ -49,11 +47,9 @@
   assert ¬\dangling(&p);
 [kernel] tests/builtins/allocated.c:46: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
-[eva] tests/builtins/allocated.c:50: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:50: Call to builtin malloc
 [eva] tests/builtins/allocated.c:50: allocating variable __malloc_main_l50
-[eva] tests/builtins/allocated.c:50: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:50: Call to builtin malloc
 [eva] tests/builtins/allocated.c:50: allocating variable __malloc_main_l50_0
 [eva] tests/builtins/allocated.c:50: assertion got status valid.
 [eva:alarm] tests/builtins/allocated.c:53: Warning: 
@@ -70,8 +66,7 @@
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/allocated.c:58: 
   strong free on bases: {__malloc_main_l50_0}
-[eva] tests/builtins/allocated.c:63: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:63: Call to builtin malloc
 [eva] tests/builtins/allocated.c:63: allocating variable __malloc_main_l63
 [eva] tests/builtins/allocated.c:63: assertion got status valid.
 [eva] tests/builtins/allocated.c:65: 
@@ -82,8 +77,7 @@
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/allocated.c:67: 
   strong free on bases: {__malloc_main_l63}
-[eva] tests/builtins/allocated.c:63: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:63: Call to builtin malloc
 [eva] tests/builtins/allocated.c:63: allocating variable __malloc_main_l63_0
 [eva] tests/builtins/allocated.c:65: 
   Frama_C_show_each_p: {{ &__malloc_main_l63_0 }}
@@ -91,8 +85,7 @@
 [eva] tests/builtins/allocated.c:67: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:67: 
   strong free on bases: {__malloc_main_l63_0}
-[eva] tests/builtins/allocated.c:63: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:63: Call to builtin malloc
 [eva] tests/builtins/allocated.c:63: allocating variable __malloc_main_l63_1
 [eva] tests/builtins/allocated.c:65: 
   Frama_C_show_each_p: {{ &__malloc_main_l63_1 }}
@@ -100,8 +93,7 @@
 [eva] tests/builtins/allocated.c:67: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:67: 
   strong free on bases: {__malloc_main_l63_1}
-[eva] tests/builtins/allocated.c:63: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:63: Call to builtin malloc
 [eva] tests/builtins/allocated.c:63: allocating variable __malloc_main_l63_2
 [eva] tests/builtins/allocated.c:65: 
   Frama_C_show_each_p: {{ &__malloc_main_l63_2 }}
@@ -109,8 +101,7 @@
 [eva] tests/builtins/allocated.c:67: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:67: 
   strong free on bases: {__malloc_main_l63_2}
-[eva] tests/builtins/allocated.c:73: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:73: Call to builtin malloc
 [eva] tests/builtins/allocated.c:73: allocating variable __malloc_main_l73
 [eva] tests/builtins/allocated.c:75: 
   Frama_C_show_each_p: {{ &__malloc_main_l73 }}
@@ -120,8 +111,7 @@
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/allocated.c:77: 
   strong free on bases: {__malloc_main_l73}
-[eva] tests/builtins/allocated.c:73: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:73: Call to builtin malloc
 [eva] tests/builtins/allocated.c:73: allocating variable __malloc_main_l73_0
 [eva] tests/builtins/allocated.c:75: 
   Frama_C_show_each_p: {{ &__malloc_main_l73_0 }}
@@ -129,8 +119,7 @@
 [eva] tests/builtins/allocated.c:77: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:77: 
   strong free on bases: {__malloc_main_l73_0}
-[eva] tests/builtins/allocated.c:73: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:73: Call to builtin malloc
 [eva] tests/builtins/allocated.c:73: allocating variable __malloc_main_l73_1
 [eva] tests/builtins/allocated.c:75: 
   Frama_C_show_each_p: {{ &__malloc_main_l73_1 }}
@@ -138,8 +127,7 @@
 [eva] tests/builtins/allocated.c:77: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:77: 
   strong free on bases: {__malloc_main_l73_1}
-[eva] tests/builtins/allocated.c:73: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:73: Call to builtin malloc
 [eva] tests/builtins/allocated.c:73: allocating variable __malloc_main_l73_2
 [eva] tests/builtins/allocated.c:75: 
   Frama_C_show_each_p: {{ &__malloc_main_l73_2 }}
@@ -147,8 +135,7 @@
 [eva] tests/builtins/allocated.c:77: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:77: 
   strong free on bases: {__malloc_main_l73_2}
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82
 [eva] tests/builtins/allocated.c:82: assertion got status valid.
 [eva] tests/builtins/allocated.c:87: Call to builtin free
@@ -156,11 +143,9 @@
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/allocated.c:87: 
   strong free on bases: {__malloc_main_l82}
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_0
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_1
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
@@ -174,20 +159,15 @@
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
   strong free on bases: {__malloc_main_l82_0}
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_2
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_3
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_4
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_5
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_6
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
@@ -249,77 +229,53 @@
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
   strong free on bases: {__malloc_main_l82_6}
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_8
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_9
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_10
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_11
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_12
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_13
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_14
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_15
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_16
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_17
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_18
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_19
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_20
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_21
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_22
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_23
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_24
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_25
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_26
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_27
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_28
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_29
-[eva] tests/builtins/allocated.c:82: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:82: Call to builtin malloc
 [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_30
 [eva] tests/builtins/allocated.c:84: 
   Trace partitioning superposing up to 100 states
@@ -905,8 +861,7 @@
 [eva] tests/builtins/allocated.c:87: Call to builtin free
 [eva:malloc] tests/builtins/allocated.c:87: 
   strong free on bases: {__malloc_main_l82_7}
-[eva] tests/builtins/allocated.c:91: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:91: Call to builtin malloc
 [eva] tests/builtins/allocated.c:91: allocating variable __malloc_main_l91
 [eva] tests/builtins/allocated.c:91: assertion got status valid.
 [eva] tests/builtins/allocated.c:92: Call to builtin free
@@ -916,8 +871,7 @@
   strong free on bases: {__malloc_main_l91}
 [eva:alarm] tests/builtins/allocated.c:96: Warning: 
   assertion 'Assume' got status unknown.
-[eva] tests/builtins/allocated.c:97: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:97: Call to builtin malloc
 [eva] tests/builtins/allocated.c:97: allocating variable __malloc_main_l97
 [eva] tests/builtins/allocated.c:97: Frama_C_show_each: {{ &__malloc_main_l97 }}
 [eva:alarm] tests/builtins/allocated.c:98: Warning: 
@@ -930,8 +884,7 @@
   strong free on bases: {__malloc_main_l97}
 [eva:alarm] tests/builtins/allocated.c:113: Warning: 
   assertion got status unknown.
-[eva] tests/builtins/allocated.c:114: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:114: Call to builtin malloc
 [eva] tests/builtins/allocated.c:114: allocating variable __malloc_main_l114
 [eva] tests/builtins/allocated.c:114: 
   Frama_C_show_each: {{ &__malloc_main_l114 }}
@@ -943,8 +896,7 @@
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/allocated.c:118: 
   strong free on bases: {__malloc_main_l114}
-[eva] tests/builtins/allocated.c:120: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/allocated.c:120: Call to builtin malloc
 [eva] tests/builtins/allocated.c:120: allocating variable __malloc_main_l120
 [eva] tests/builtins/allocated.c:120: 
   Frama_C_show_each: {{ &__malloc_main_l120 }}
@@ -956,84 +908,64 @@
   strong free on bases: {__malloc_main_l120}
 [eva] tests/builtins/allocated.c:127: 
   assertion 'alloca_bounds' got status valid.
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_malloc_fresh for function __fc_vla_alloc
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva] tests/builtins/allocated.c:127: allocating variable __malloc_main_l127
 [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_vla_free for function __fc_vla_free
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_malloc_fresh for function __fc_vla_alloc
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva] tests/builtins/allocated.c:127: allocating variable __malloc_main_l127_0
 [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {1}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_vla_free for function __fc_vla_free
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127_0}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_malloc_fresh for function __fc_vla_alloc
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva] tests/builtins/allocated.c:127: allocating variable __malloc_main_l127_1
 [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {2}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_vla_free for function __fc_vla_free
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127_1}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_malloc_fresh for function __fc_vla_alloc
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva] tests/builtins/allocated.c:127: allocating variable __malloc_main_l127_2
 [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {3}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_vla_free for function __fc_vla_free
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127_2}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_malloc_fresh for function __fc_vla_alloc
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva] tests/builtins/allocated.c:127: allocating variable __malloc_main_l127_3
 [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {4}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_vla_free for function __fc_vla_free
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127_3}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_malloc_fresh for function __fc_vla_alloc
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva] tests/builtins/allocated.c:127: allocating variable __malloc_main_l127_4
 [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {5}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_vla_free for function __fc_vla_free
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127_4}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_malloc_fresh for function __fc_vla_alloc
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva] tests/builtins/allocated.c:127: allocating variable __malloc_main_l127_5
 [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {6}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_vla_free for function __fc_vla_free
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127_5}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_malloc_fresh for function __fc_vla_alloc
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva] tests/builtins/allocated.c:127: allocating variable __malloc_main_l127_6
 [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {7}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_vla_free for function __fc_vla_free
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127_6}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_malloc_fresh for function __fc_vla_alloc
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva] tests/builtins/allocated.c:127: allocating variable __malloc_main_l127_7
 [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {8}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_vla_free for function __fc_vla_free
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127_7}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_malloc_fresh for function __fc_vla_alloc
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva] tests/builtins/allocated.c:127: allocating variable __malloc_main_l127_8
 [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {9}
-[eva] tests/builtins/allocated.c:127: 
-  Call to builtin Frama_C_vla_free for function __fc_vla_free
+[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127_8}
 [eva] Recording results for main
diff --git a/tests/builtins/oracle/calloc.1.res.oracle b/tests/builtins/oracle/calloc.1.res.oracle
index 535b360668c1cec5404dd95faa8bae976eaef893..e9d117220688f544cbd8899125650321883f78b5 100644
--- a/tests/builtins/oracle/calloc.1.res.oracle
+++ b/tests/builtins/oracle/calloc.1.res.oracle
@@ -4,28 +4,22 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
-[eva] tests/builtins/calloc.c:14: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:14: Call to builtin calloc
 [eva] tests/builtins/calloc.c:14: allocating variable __calloc_main_l14
-[eva] tests/builtins/calloc.c:17: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:17: Call to builtin calloc
 [eva] tests/builtins/calloc.c:17: allocating variable __calloc_main_l17
-[eva] tests/builtins/calloc.c:20: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:20: Call to builtin calloc
 [eva] tests/builtins/calloc.c:20: allocating variable __calloc_main_l20
-[eva] tests/builtins/calloc.c:23: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:23: Call to builtin calloc
 [eva] tests/builtins/calloc.c:23: allocating variable __calloc_main_l23
 [eva] tests/builtins/calloc.c:26: assertion got status valid.
 [eva] tests/builtins/calloc.c:27: assertion got status valid.
-[eva] tests/builtins/calloc.c:30: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:30: Call to builtin calloc
 [eva] tests/builtins/calloc.c:30: allocating variable __calloc_main_l30
 [eva] tests/builtins/calloc.c:33: assertion got status valid.
 [eva] tests/builtins/calloc.c:34: assertion got status valid.
 [eva] tests/builtins/calloc.c:35: assertion got status valid.
-[eva] tests/builtins/calloc.c:38: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:38: Call to builtin calloc
 [eva] tests/builtins/calloc.c:38: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva] tests/builtins/calloc.c:40: assertion got status valid.
diff --git a/tests/builtins/oracle/calloc.2.res.oracle b/tests/builtins/oracle/calloc.2.res.oracle
index 7ff1efdd5feed2c886dcdcb55138415454d6e095..e9d117220688f544cbd8899125650321883f78b5 100644
--- a/tests/builtins/oracle/calloc.2.res.oracle
+++ b/tests/builtins/oracle/calloc.2.res.oracle
@@ -4,28 +4,22 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
-[eva] tests/builtins/calloc.c:14: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:14: Call to builtin calloc
 [eva] tests/builtins/calloc.c:14: allocating variable __calloc_main_l14
-[eva] tests/builtins/calloc.c:17: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:17: Call to builtin calloc
 [eva] tests/builtins/calloc.c:17: allocating variable __calloc_main_l17
-[eva] tests/builtins/calloc.c:20: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:20: Call to builtin calloc
 [eva] tests/builtins/calloc.c:20: allocating variable __calloc_main_l20
-[eva] tests/builtins/calloc.c:23: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:23: Call to builtin calloc
 [eva] tests/builtins/calloc.c:23: allocating variable __calloc_main_l23
 [eva] tests/builtins/calloc.c:26: assertion got status valid.
 [eva] tests/builtins/calloc.c:27: assertion got status valid.
-[eva] tests/builtins/calloc.c:30: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:30: Call to builtin calloc
 [eva] tests/builtins/calloc.c:30: allocating variable __calloc_main_l30
 [eva] tests/builtins/calloc.c:33: assertion got status valid.
 [eva] tests/builtins/calloc.c:34: assertion got status valid.
 [eva] tests/builtins/calloc.c:35: assertion got status valid.
-[eva] tests/builtins/calloc.c:38: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:38: Call to builtin calloc
 [eva] tests/builtins/calloc.c:38: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva] tests/builtins/calloc.c:40: assertion got status valid.
diff --git a/tests/builtins/oracle/calloc.3.res.oracle b/tests/builtins/oracle/calloc.3.res.oracle
index 535b360668c1cec5404dd95faa8bae976eaef893..e9d117220688f544cbd8899125650321883f78b5 100644
--- a/tests/builtins/oracle/calloc.3.res.oracle
+++ b/tests/builtins/oracle/calloc.3.res.oracle
@@ -4,28 +4,22 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
-[eva] tests/builtins/calloc.c:14: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:14: Call to builtin calloc
 [eva] tests/builtins/calloc.c:14: allocating variable __calloc_main_l14
-[eva] tests/builtins/calloc.c:17: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:17: Call to builtin calloc
 [eva] tests/builtins/calloc.c:17: allocating variable __calloc_main_l17
-[eva] tests/builtins/calloc.c:20: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:20: Call to builtin calloc
 [eva] tests/builtins/calloc.c:20: allocating variable __calloc_main_l20
-[eva] tests/builtins/calloc.c:23: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:23: Call to builtin calloc
 [eva] tests/builtins/calloc.c:23: allocating variable __calloc_main_l23
 [eva] tests/builtins/calloc.c:26: assertion got status valid.
 [eva] tests/builtins/calloc.c:27: assertion got status valid.
-[eva] tests/builtins/calloc.c:30: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:30: Call to builtin calloc
 [eva] tests/builtins/calloc.c:30: allocating variable __calloc_main_l30
 [eva] tests/builtins/calloc.c:33: assertion got status valid.
 [eva] tests/builtins/calloc.c:34: assertion got status valid.
 [eva] tests/builtins/calloc.c:35: assertion got status valid.
-[eva] tests/builtins/calloc.c:38: 
-  Call to builtin Frama_C_calloc_fresh for function calloc
+[eva] tests/builtins/calloc.c:38: Call to builtin calloc
 [eva] tests/builtins/calloc.c:38: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva] tests/builtins/calloc.c:40: assertion got status valid.
diff --git a/tests/builtins/oracle/calloc.4.res.oracle b/tests/builtins/oracle/calloc.4.res.oracle
index 7ff1efdd5feed2c886dcdcb55138415454d6e095..e9d117220688f544cbd8899125650321883f78b5 100644
--- a/tests/builtins/oracle/calloc.4.res.oracle
+++ b/tests/builtins/oracle/calloc.4.res.oracle
@@ -4,28 +4,22 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
-[eva] tests/builtins/calloc.c:14: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:14: Call to builtin calloc
 [eva] tests/builtins/calloc.c:14: allocating variable __calloc_main_l14
-[eva] tests/builtins/calloc.c:17: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:17: Call to builtin calloc
 [eva] tests/builtins/calloc.c:17: allocating variable __calloc_main_l17
-[eva] tests/builtins/calloc.c:20: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:20: Call to builtin calloc
 [eva] tests/builtins/calloc.c:20: allocating variable __calloc_main_l20
-[eva] tests/builtins/calloc.c:23: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:23: Call to builtin calloc
 [eva] tests/builtins/calloc.c:23: allocating variable __calloc_main_l23
 [eva] tests/builtins/calloc.c:26: assertion got status valid.
 [eva] tests/builtins/calloc.c:27: assertion got status valid.
-[eva] tests/builtins/calloc.c:30: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:30: Call to builtin calloc
 [eva] tests/builtins/calloc.c:30: allocating variable __calloc_main_l30
 [eva] tests/builtins/calloc.c:33: assertion got status valid.
 [eva] tests/builtins/calloc.c:34: assertion got status valid.
 [eva] tests/builtins/calloc.c:35: assertion got status valid.
-[eva] tests/builtins/calloc.c:38: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+[eva] tests/builtins/calloc.c:38: Call to builtin calloc
 [eva] tests/builtins/calloc.c:38: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva] tests/builtins/calloc.c:40: assertion got status valid.
diff --git a/tests/builtins/oracle/calloc.5.res.oracle b/tests/builtins/oracle/calloc.5.res.oracle
index 679c1f964b2efcdc39a9b52a8af80ba2a8d09bd6..da3dbc95be53c68b8e10c9e80b5df119f0bb274b 100644
--- a/tests/builtins/oracle/calloc.5.res.oracle
+++ b/tests/builtins/oracle/calloc.5.res.oracle
@@ -4,25 +4,19 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
-[eva] tests/builtins/calloc.c:14: 
-  Call to builtin Frama_C_calloc_imprecise for function calloc
+[eva] tests/builtins/calloc.c:14: Call to builtin calloc
 [eva:malloc:imprecise] tests/builtins/calloc.c:14: Warning: 
   allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main
-[eva] tests/builtins/calloc.c:17: 
-  Call to builtin Frama_C_calloc_imprecise for function calloc
-[eva] tests/builtins/calloc.c:20: 
-  Call to builtin Frama_C_calloc_imprecise for function calloc
-[eva] tests/builtins/calloc.c:23: 
-  Call to builtin Frama_C_calloc_imprecise for function calloc
+[eva] tests/builtins/calloc.c:17: Call to builtin calloc
+[eva] tests/builtins/calloc.c:20: Call to builtin calloc
+[eva] tests/builtins/calloc.c:23: Call to builtin calloc
 [eva:alarm] tests/builtins/calloc.c:26: Warning: assertion got status unknown.
 [eva:alarm] tests/builtins/calloc.c:27: Warning: assertion got status unknown.
-[eva] tests/builtins/calloc.c:30: 
-  Call to builtin Frama_C_calloc_imprecise for function calloc
+[eva] tests/builtins/calloc.c:30: Call to builtin calloc
 [eva:alarm] tests/builtins/calloc.c:33: Warning: assertion got status unknown.
 [eva:alarm] tests/builtins/calloc.c:34: Warning: assertion got status unknown.
 [eva:alarm] tests/builtins/calloc.c:35: Warning: assertion got status unknown.
-[eva] tests/builtins/calloc.c:38: 
-  Call to builtin Frama_C_calloc_imprecise for function calloc
+[eva] tests/builtins/calloc.c:38: Call to builtin calloc
 [eva] tests/builtins/calloc.c:38: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva] tests/builtins/calloc.c:40: assertion got status valid.
diff --git a/tests/builtins/oracle/free.res.oracle b/tests/builtins/oracle/free.res.oracle
index c3f99748ef4e105b4ac514f33fb35fa4d2fd4b42..25410f0957bb50444bf632413500466b138444ad 100644
--- a/tests/builtins/oracle/free.res.oracle
+++ b/tests/builtins/oracle/free.res.oracle
@@ -6,11 +6,9 @@
   v ∈ [--..--]
 [eva] computing for function main1 <- main.
   Called from tests/builtins/free.c:44.
-[eva] tests/builtins/free.c:8: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/free.c:8: Call to builtin malloc
 [eva] tests/builtins/free.c:8: allocating variable __malloc_main1_l8
-[eva] tests/builtins/free.c:10: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/free.c:10: Call to builtin malloc
 [eva] tests/builtins/free.c:10: allocating variable __malloc_main1_l10
 [eva] tests/builtins/free.c:13: 
   Frama_C_dump_each:
@@ -46,8 +44,7 @@
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/free.c:14: 
   weak free on bases: {__malloc_main1_l8, __malloc_main1_l10}
-[eva] tests/builtins/free.c:16: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/free.c:16: Call to builtin malloc
 [eva] tests/builtins/free.c:16: allocating variable __malloc_main1_l16
 [eva] tests/builtins/free.c:18: Call to builtin free
 [eva] tests/builtins/free.c:18: 
@@ -58,8 +55,7 @@
 [eva] tests/builtins/free.c:21: 
   function free: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/free.c:21: strong free on bases: {}
-[eva] tests/builtins/free.c:23: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/free.c:23: Call to builtin malloc
 [eva] tests/builtins/free.c:23: allocating variable __malloc_main1_l23
 [eva] tests/builtins/free.c:26: Call to builtin free
 [eva] tests/builtins/free.c:26: 
@@ -69,8 +65,7 @@
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
   Called from tests/builtins/free.c:45.
-[eva] tests/builtins/free.c:35: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/free.c:35: Call to builtin malloc
 [eva] tests/builtins/free.c:35: allocating variable __malloc_main2_l35
 [eva] tests/builtins/free.c:39: Call to builtin free
 [eva] tests/builtins/free.c:39: 
diff --git a/tests/builtins/oracle/from_result.res.oracle b/tests/builtins/oracle/from_result.res.oracle
index 85a36a0aee67f36c171549c6dab7303977215c3f..c301602f03176ca2b6758e2e5016e331d4083bc3 100644
--- a/tests/builtins/oracle/from_result.res.oracle
+++ b/tests/builtins/oracle/from_result.res.oracle
@@ -6,13 +6,13 @@
   
 [eva] computing for function bar <- main.
   Called from tests/builtins/from_result.c:32.
-[eva] tests/builtins/from_result.c:18: Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/from_result.c:18: Call to builtin malloc
 [eva] tests/builtins/from_result.c:18: allocating variable __malloc_bar_l18
 [eva] Recording results for bar
 [eva] Done for function bar
 [eva] computing for function bar <- main.
   Called from tests/builtins/from_result.c:33.
-[eva] tests/builtins/from_result.c:18: Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/from_result.c:18: Call to builtin malloc
 [eva] tests/builtins/from_result.c:18: allocating variable __malloc_bar_l18_0
 [eva] Recording results for bar
 [eva] Done for function bar
@@ -36,12 +36,12 @@
 [eva] Done for function foo
 [eva] Recording results for main
 [eva] done for function main
-[from] Computing for function bar
-[from] Computing for function Frama_C_malloc_fresh <-bar
-[from] Done for function Frama_C_malloc_fresh
-[from] Done for function bar
 [from] Computing for function change_t
 [from] Done for function change_t
+[from] Computing for function bar
+[from] Computing for function malloc <-bar
+[from] Done for function malloc
+[from] Done for function bar
 [from] Computing for function main
 [from] Computing for function create_t <-main
 [from] Done for function create_t
@@ -52,14 +52,6 @@
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_malloc_fresh:
-  __fc_heap_status FROM __fc_heap_status; size (and SELF)
-  \result FROM __fc_heap_status; size
-[from] Function bar:
-  __fc_heap_status FROM __fc_heap_status (and SELF)
-  __malloc_bar_l18 FROM __fc_heap_status; x (and SELF)
-  __malloc_bar_l18_0 FROM __fc_heap_status; x (and SELF)
-  \result FROM __fc_heap_status
 [from] Function change_t:
   v.a FROM t0; x
    .b FROM t0; y
@@ -69,6 +61,14 @@
   \result FROM x; y
 [from] Function foo:
   \result FROM ANYTHING(origin:Unknown)
+[from] Function malloc:
+  __fc_heap_status FROM __fc_heap_status; size (and SELF)
+  \result FROM __fc_heap_status; size
+[from] Function bar:
+  __fc_heap_status FROM __fc_heap_status (and SELF)
+  __malloc_bar_l18 FROM __fc_heap_status; x (and SELF)
+  __malloc_bar_l18_0 FROM __fc_heap_status; x (and SELF)
+  \result FROM __fc_heap_status
 [from] Function main:
   __fc_heap_status FROM __fc_heap_status (and SELF)
   __malloc_bar_l18 FROM __fc_heap_status (and SELF)
diff --git a/tests/builtins/oracle/gcc_zero_length_array.res.oracle b/tests/builtins/oracle/gcc_zero_length_array.res.oracle
index 176fc455f84536af22bcf0749ba6b3fc14b56095..30061ac03dfa213caac301e75447eec5d9506b30 100644
--- a/tests/builtins/oracle/gcc_zero_length_array.res.oracle
+++ b/tests/builtins/oracle/gcc_zero_length_array.res.oracle
@@ -6,8 +6,7 @@
   
 [eva] computing for function make_fam <- main.
   Called from tests/builtins/gcc_zero_length_array.c:24.
-[eva] tests/builtins/gcc_zero_length_array.c:15: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/gcc_zero_length_array.c:15: Call to builtin malloc
 [eva] tests/builtins/gcc_zero_length_array.c:15: 
   allocating variable __malloc_make_fam_l15
 [eva] Recording results for make_fam
diff --git a/tests/builtins/oracle/malloc-deps.res.oracle b/tests/builtins/oracle/malloc-deps.res.oracle
index 3d9d469a1915936ad60fcfe7f8589d9e44add84b..5a0c179552e632e5c31ca0ae464581762dae7c8d 100644
--- a/tests/builtins/oracle/malloc-deps.res.oracle
+++ b/tests/builtins/oracle/malloc-deps.res.oracle
@@ -4,103 +4,103 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   v ∈ [--..--]
-[eva] tests/builtins/malloc-deps.c:17: Call to builtin Frama_C_malloc_fresh_weak
-[eva] tests/builtins/malloc-deps.c:17: 
-  allocating weak variable __malloc_w_main_l17
-[eva] tests/builtins/malloc-deps.c:21: Call to builtin Frama_C_malloc_fresh
-[eva] tests/builtins/malloc-deps.c:21: allocating variable __malloc_main_l21
-[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
-[eva] tests/builtins/malloc-deps.c:28: allocating variable __malloc_main_l28
+[eva] tests/builtins/malloc-deps.c:12: Call to builtin malloc
+[eva] tests/builtins/malloc-deps.c:12: 
+  allocating weak variable __malloc_w_main_l12
+[eva] tests/builtins/malloc-deps.c:17: Call to builtin malloc
+[eva] tests/builtins/malloc-deps.c:17: allocating variable __malloc_main_l17
+[eva] tests/builtins/malloc-deps.c:25: Call to builtin malloc
+[eva] tests/builtins/malloc-deps.c:25: allocating variable __malloc_main_l25
 [eva] computing for function g <- main.
-  Called from tests/builtins/malloc-deps.c:29.
-[eva:alarm] tests/builtins/malloc-deps.c:13: Warning: 
+  Called from tests/builtins/malloc-deps.c:26.
+[eva:alarm] tests/builtins/malloc-deps.c:7: Warning: 
   out of bounds write. assert \valid(p + k);
 [eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
 [eva] Done for function g
-[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc:weak] tests/builtins/malloc-deps.c:28: 
-  marking variable `__malloc_main_l28' as weak
-[eva:malloc] tests/builtins/malloc-deps.c:28: 
-  resizing variable `__malloc_w_main_l28' (0..31) to fit 0..63
-[eva:alarm] tests/builtins/malloc-deps.c:29: Warning: 
+[eva] tests/builtins/malloc-deps.c:25: Call to builtin malloc
+[eva:malloc:weak] tests/builtins/malloc-deps.c:25: 
+  marking variable `__malloc_main_l25' as weak
+[eva:malloc] tests/builtins/malloc-deps.c:25: 
+  resizing variable `__malloc_w_main_l25' (0..31) to fit 0..63
+[eva:alarm] tests/builtins/malloc-deps.c:26: Warning: 
   signed overflow. assert l + v ≤ 2147483647;
 [eva] computing for function g <- main.
-  Called from tests/builtins/malloc-deps.c:29.
+  Called from tests/builtins/malloc-deps.c:26.
 [eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
 [eva] Done for function g
-[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.c:28: 
-  resizing variable `__malloc_w_main_l28' (0..31/63) to fit 0..95
+[eva] tests/builtins/malloc-deps.c:25: Call to builtin malloc
+[eva:malloc] tests/builtins/malloc-deps.c:25: 
+  resizing variable `__malloc_w_main_l25' (0..31/63) to fit 0..95
 [eva] computing for function g <- main.
-  Called from tests/builtins/malloc-deps.c:29.
+  Called from tests/builtins/malloc-deps.c:26.
 [eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
 [eva] Done for function g
-[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.c:28: 
-  resizing variable `__malloc_w_main_l28' (0..31/95) to fit 0..127
+[eva] tests/builtins/malloc-deps.c:25: Call to builtin malloc
+[eva:malloc] tests/builtins/malloc-deps.c:25: 
+  resizing variable `__malloc_w_main_l25' (0..31/95) to fit 0..127
 [eva] computing for function g <- main.
-  Called from tests/builtins/malloc-deps.c:29.
+  Called from tests/builtins/malloc-deps.c:26.
 [eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
 [eva] Done for function g
-[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.c:28: 
-  resizing variable `__malloc_w_main_l28' (0..31/127) to fit 0..159
+[eva] tests/builtins/malloc-deps.c:25: Call to builtin malloc
+[eva:malloc] tests/builtins/malloc-deps.c:25: 
+  resizing variable `__malloc_w_main_l25' (0..31/127) to fit 0..159
 [eva] computing for function g <- main.
-  Called from tests/builtins/malloc-deps.c:29.
+  Called from tests/builtins/malloc-deps.c:26.
 [eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
 [eva] Done for function g
-[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.c:28: 
-  resizing variable `__malloc_w_main_l28' (0..31/159) to fit 0..191
+[eva] tests/builtins/malloc-deps.c:25: Call to builtin malloc
+[eva:malloc] tests/builtins/malloc-deps.c:25: 
+  resizing variable `__malloc_w_main_l25' (0..31/159) to fit 0..191
 [eva] computing for function g <- main.
-  Called from tests/builtins/malloc-deps.c:29.
+  Called from tests/builtins/malloc-deps.c:26.
 [eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
 [eva] Done for function g
-[eva] tests/builtins/malloc-deps.c:27: starting to merge loop iterations
-[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.c:28: 
-  resizing variable `__malloc_w_main_l28' (0..31/191) to fit 0..191/223
+[eva] tests/builtins/malloc-deps.c:23: starting to merge loop iterations
+[eva] tests/builtins/malloc-deps.c:25: Call to builtin malloc
+[eva:malloc] tests/builtins/malloc-deps.c:25: 
+  resizing variable `__malloc_w_main_l25' (0..31/191) to fit 0..191/223
 [eva] computing for function g <- main.
-  Called from tests/builtins/malloc-deps.c:29.
+  Called from tests/builtins/malloc-deps.c:26.
 [eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
 [eva] Done for function g
-[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.c:28: 
-  resizing variable `__malloc_w_main_l28' (0..31/223) to fit 0..191/255
+[eva] tests/builtins/malloc-deps.c:25: Call to builtin malloc
+[eva:malloc] tests/builtins/malloc-deps.c:25: 
+  resizing variable `__malloc_w_main_l25' (0..31/223) to fit 0..191/255
 [eva] computing for function g <- main.
-  Called from tests/builtins/malloc-deps.c:29.
+  Called from tests/builtins/malloc-deps.c:26.
 [eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
 [eva] Done for function g
-[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.c:28: 
-  resizing variable `__malloc_w_main_l28' (0..31/255) to fit 0..191/319
+[eva] tests/builtins/malloc-deps.c:25: Call to builtin malloc
+[eva:malloc] tests/builtins/malloc-deps.c:25: 
+  resizing variable `__malloc_w_main_l25' (0..31/255) to fit 0..191/319
 [eva] computing for function g <- main.
-  Called from tests/builtins/malloc-deps.c:29.
+  Called from tests/builtins/malloc-deps.c:26.
 [eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
 [eva] Done for function g
-[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.c:28: 
-  resizing variable `__malloc_w_main_l28' (0..31/319) to fit 0..191/319
+[eva] tests/builtins/malloc-deps.c:25: Call to builtin malloc
+[eva:malloc] tests/builtins/malloc-deps.c:25: 
+  resizing variable `__malloc_w_main_l25' (0..31/319) to fit 0..191/319
 [eva] computing for function g <- main.
-  Called from tests/builtins/malloc-deps.c:29.
+  Called from tests/builtins/malloc-deps.c:26.
 [eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
@@ -111,54 +111,53 @@
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function g:
-  __malloc_w_main_l28[0..9] ∈ [0..9] or UNINITIALIZED
+  __malloc_w_main_l25[0..9] ∈ [0..9] or UNINITIALIZED
 [eva:final-states] Values at end of function main:
-  p ∈ {{ &__malloc_w_main_l17[0] }}
-  q ∈ {{ &__malloc_main_l21[0] }}
-  r ∈ {{ &__malloc_w_main_l28[0] }}
-  __malloc_w_main_l17[0] ∈ [--..--] or UNINITIALIZED
+  __fc_heap_status ∈ [--..--]
+  p ∈ {{ &__malloc_w_main_l12[0] }}
+  q ∈ {{ &__malloc_main_l17[0] }}
+  r ∈ {{ &__malloc_w_main_l25[0] }}
+  __malloc_w_main_l12[0] ∈ [--..--] or UNINITIALIZED
                      [1..24] ∈ UNINITIALIZED
-  __malloc_main_l21[0] ∈ [--..--]
+  __malloc_main_l17[0] ∈ [--..--]
                    [1..24] ∈ UNINITIALIZED
-  __malloc_w_main_l28[0..9] ∈ [0..9] or UNINITIALIZED
+  __malloc_w_main_l25[0..9] ∈ [0..9] or UNINITIALIZED
 [from] Computing for function g
 [from] Done for function g
 [from] Computing for function main
-[from] Computing for function Frama_C_malloc_fresh_weak <-main
-[from] Done for function Frama_C_malloc_fresh_weak
-[from] Computing for function Frama_C_malloc_fresh <-main
-[from] Done for function Frama_C_malloc_fresh
-[from] Computing for function Frama_C_malloc_by_stack <-main
-[from] Done for function Frama_C_malloc_by_stack
+[from] Computing for function malloc <-main
+[from] Done for function malloc
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_malloc_by_stack:
-  \result FROM \nothing
-[from] Function Frama_C_malloc_fresh:
-  \result FROM \nothing
-[from] Function Frama_C_malloc_fresh_weak:
-  \result FROM \nothing
 [from] Function g:
-  __malloc_w_main_l28[0..9] FROM p; k (and SELF)
+  __malloc_w_main_l25[0..9] FROM p; k (and SELF)
+[from] Function malloc:
+  __fc_heap_status FROM __fc_heap_status; size (and SELF)
+  \result FROM __fc_heap_status; size
 [from] Function main:
-  __malloc_w_main_l17[0] FROM i; j (and SELF)
-  __malloc_main_l21[0] FROM j
-  __malloc_w_main_l28[0..9] FROM v (and SELF)
+  __fc_heap_status FROM __fc_heap_status (and SELF)
+  __malloc_w_main_l12[0] FROM __fc_heap_status; i; j (and SELF)
+  __malloc_main_l17[0] FROM __fc_heap_status; j
+  __malloc_w_main_l25[0..9] FROM __fc_heap_status; v (and SELF)
 [from] ====== END OF DEPENDENCIES ======
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to Frama_C_malloc_fresh_weak at tests/builtins/malloc-deps.c:17 (by main):
-  \result FROM \nothing
-[from] call to Frama_C_malloc_fresh at tests/builtins/malloc-deps.c:21 (by main):
-  \result FROM \nothing
-[from] call to Frama_C_malloc_by_stack at tests/builtins/malloc-deps.c:28 (by main):
-  \result FROM \nothing
-[from] call to g at tests/builtins/malloc-deps.c:29 (by main):
-  __malloc_w_main_l28[0..9] FROM p; k (and SELF)
+[from] call to malloc at tests/builtins/malloc-deps.c:12 (by main):
+  __fc_heap_status FROM __fc_heap_status; size (and SELF)
+  \result FROM __fc_heap_status; size
+[from] call to malloc at tests/builtins/malloc-deps.c:17 (by main):
+  __fc_heap_status FROM __fc_heap_status; size (and SELF)
+  \result FROM __fc_heap_status; size
+[from] call to malloc at tests/builtins/malloc-deps.c:25 (by main):
+  __fc_heap_status FROM __fc_heap_status; size (and SELF)
+  \result FROM __fc_heap_status; size
+[from] call to g at tests/builtins/malloc-deps.c:26 (by main):
+  __malloc_w_main_l25[0..9] FROM p; k (and SELF)
 [from] entry point:
-  __malloc_w_main_l17[0] FROM i; j (and SELF)
-  __malloc_main_l21[0] FROM j
-  __malloc_w_main_l28[0..9] FROM v (and SELF)
+  __fc_heap_status FROM __fc_heap_status (and SELF)
+  __malloc_w_main_l12[0] FROM __fc_heap_status; i; j (and SELF)
+  __malloc_main_l17[0] FROM __fc_heap_status; j
+  __malloc_w_main_l25[0..9] FROM __fc_heap_status; v (and SELF)
 [from] ====== END OF CALLWISE DEPENDENCIES ======
 [inout] InOut (internal) for function g:
   Operational inputs:
@@ -169,8 +168,8 @@
     \nothing
 [inout] InOut (internal) for function main:
   Operational inputs:
-    v; i; j
+    __fc_heap_status; v; i; j
   Operational inputs on termination:
-    v; i; j
+    __fc_heap_status; v; i; j
   Sure outputs:
-    p; q; l; __malloc_main_l21[0]
+    p; q; l; __malloc_main_l17[0]
diff --git a/tests/builtins/oracle/malloc.res.oracle b/tests/builtins/oracle/malloc.res.oracle
index 6bfbf908188b5a5853ee19749c30e75bcd07d56f..c074da92a87a89b73e242ff389bb0d511fa5eded 100644
--- a/tests/builtins/oracle/malloc.res.oracle
+++ b/tests/builtins/oracle/malloc.res.oracle
@@ -1,74 +1,69 @@
 [kernel] Parsing tests/builtins/malloc.c (with preprocessing)
-[kernel:annot:missing-spec] tests/builtins/malloc.c:8: Warning: 
-  Neither code nor specification for function Frama_C_malloc_fresh, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/builtins/malloc.c:8: Warning: 
-  Neither code nor specification for function Frama_C_malloc_by_stack, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/builtins/malloc.c:8: Warning: 
-  Neither code nor specification for function Frama_C_malloc_imprecise, generating default assigns from the prototype
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] tests/builtins/malloc.c:13: Call to builtin Frama_C_malloc_by_stack
-[eva] tests/builtins/malloc.c:13: allocating variable __malloc_main_l13
-[eva] tests/builtins/malloc.c:19: Call to builtin Frama_C_malloc_by_stack
-[eva] tests/builtins/malloc.c:19: allocating variable __malloc_main_l19
-[eva] tests/builtins/malloc.c:19: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc.c:19: 
-  resizing variable `__malloc_main_l19' (0..-1/34359738359) to fit 0..-1
-[eva] tests/builtins/malloc.c:20: Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/malloc.c:11: Call to builtin malloc
+[eva] tests/builtins/malloc.c:11: allocating variable __malloc_main_l11
+[eva] tests/builtins/malloc.c:17: Call to builtin malloc
+[eva] tests/builtins/malloc.c:17: allocating variable __malloc_main_l17
+[eva] tests/builtins/malloc.c:17: Call to builtin malloc
+[eva:malloc] tests/builtins/malloc.c:17: 
+  resizing variable `__malloc_main_l17' (0..-1/34359738359) to fit 0..-1
+[eva] tests/builtins/malloc.c:18: Call to builtin malloc
+[eva] tests/builtins/malloc.c:18: allocating variable __malloc_main_l18
+[eva] tests/builtins/malloc.c:18: Call to builtin malloc
+[eva] tests/builtins/malloc.c:20: Call to builtin malloc
 [eva] tests/builtins/malloc.c:20: allocating variable __malloc_main_l20
-[eva] tests/builtins/malloc.c:20: Call to builtin Frama_C_malloc_by_stack
-[eva] tests/builtins/malloc.c:21: Call to builtin Frama_C_malloc_fresh
-[eva] tests/builtins/malloc.c:21: allocating variable __malloc_main_l21
-[eva] tests/builtins/malloc.c:21: Call to builtin Frama_C_malloc_fresh
-[eva] tests/builtins/malloc.c:21: allocating variable __malloc_main_l21_0
-[eva:alarm] tests/builtins/malloc.c:22: Warning: 
+[eva] tests/builtins/malloc.c:20: Call to builtin malloc
+[eva] tests/builtins/malloc.c:20: allocating variable __malloc_main_l20_0
+[eva:alarm] tests/builtins/malloc.c:21: Warning: 
   out of bounds write. assert \valid(p);
-[eva:alarm] tests/builtins/malloc.c:23: Warning: 
+[eva:alarm] tests/builtins/malloc.c:22: Warning: 
   out of bounds write. assert \valid(p + 2);
-[eva:alarm] tests/builtins/malloc.c:24: Warning: 
+[eva:alarm] tests/builtins/malloc.c:23: Warning: 
   out of bounds write. assert \valid(p + 24999);
-[eva] tests/builtins/malloc.c:27: 
-  Frama_C_show_each: {{ &__malloc_main_l20 + {8} }}
-[eva] tests/builtins/malloc.c:27: 
-  Frama_C_show_each: {{ &__malloc_main_l20 + {8} }}
-[eva] tests/builtins/malloc.c:33: Call to builtin Frama_C_malloc_imprecise
+[eva] tests/builtins/malloc.c:26: 
+  Frama_C_show_each: {{ &__malloc_main_l18 + {8} }}
+[eva] tests/builtins/malloc.c:26: 
+  Frama_C_show_each: {{ &__malloc_main_l18 + {8} }}
+[eva] tests/builtins/malloc.c:33: Call to builtin malloc
 [eva:malloc:imprecise] tests/builtins/malloc.c:33: Warning: 
   allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main
-[eva] tests/builtins/malloc.c:33: Call to builtin Frama_C_malloc_imprecise
+[eva] tests/builtins/malloc.c:33: Call to builtin malloc
 [eva:alarm] tests/builtins/malloc.c:34: Warning: 
   out of bounds write. assert \valid(mw);
-[eva] tests/builtins/malloc.c:35: Call to builtin Frama_C_malloc_imprecise
-[eva] tests/builtins/malloc.c:35: Call to builtin Frama_C_malloc_imprecise
-[eva:alarm] tests/builtins/malloc.c:36: Warning: 
+[eva] tests/builtins/malloc.c:36: Call to builtin malloc
+[eva] tests/builtins/malloc.c:36: Call to builtin malloc
+[eva:alarm] tests/builtins/malloc.c:37: Warning: 
   out of bounds write. assert \valid(mw2);
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
+  __fc_heap_status ∈ [--..--]
   x ∈ {1; 2}
-  s ∈ {{ NULL ; &__malloc_main_l13[0] }}
-  p ∈ {{ (int *)&__malloc_main_l19 }}
-  q ∈ {{ &__malloc_main_l20[0] }}
-  r ∈ {{ &__malloc_main_l21[0] ; &__malloc_main_l21_0[0] }}
+  s ∈ {{ NULL ; &__malloc_main_l11[0] }}
+  p ∈ {{ (int *)&__malloc_main_l17 }}
+  q ∈ {{ &__malloc_main_l18[0] }}
+  r ∈ {{ &__malloc_main_l20[0] ; &__malloc_main_l20_0[0] }}
   mw ∈ {{ (int *)&__alloc_w_main }}
   mw2 ∈ {{ (int *)&__alloc_w_main }}
-  __malloc_main_l19[bits 0 to 31] ∈ {1}
+  __malloc_main_l17[bits 0 to 31] ∈ {1}
                    [4..7] ∈ UNINITIALIZED
                    [bits 64 to 95] ∈ {3}
                    [12..99995] ∈ UNINITIALIZED
                    [bits 799968 to 799999] ∈ {4}
                    [100000..4294967294] ∈ UNINITIALIZED
-  __malloc_main_l20[0] ∈ {1}
+  __malloc_main_l18[0] ∈ {1}
                    [1] ∈ UNINITIALIZED
                    [2] ∈ {3}
-  __malloc_main_l21[0] ∈ {1}
+  __malloc_main_l20[0] ∈ {1}
                    [1] ∈ UNINITIALIZED
                    [2] ∈ {3}
                    [3..24] ∈ UNINITIALIZED
-  __malloc_main_l21_0[0] ∈ {1}
+  __malloc_main_l20_0[0] ∈ {1}
                      [1] ∈ UNINITIALIZED
                      [2] ∈ {3}
                      [3..24] ∈ UNINITIALIZED
diff --git a/tests/builtins/oracle/malloc_individual.res.oracle b/tests/builtins/oracle/malloc_individual.res.oracle
index 60ceadf293e353c27bc8ad4c83afacd7cc090d0e..0c0cdcc43936e6bd0d6bd915596eac3fc86f6416 100644
--- a/tests/builtins/oracle/malloc_individual.res.oracle
+++ b/tests/builtins/oracle/malloc_individual.res.oracle
@@ -7,8 +7,7 @@
   A ∈ {0}
   B ∈ {0}
   C ∈ {0}
-[eva] tests/builtins/malloc_individual.c:12: 
-  Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/malloc_individual.c:12: Call to builtin malloc
 [eva] tests/builtins/malloc_individual.c:12: 
   allocating variable __malloc_main_l12
 [eva:alarm] tests/builtins/malloc_individual.c:15: Warning: 
@@ -24,12 +23,12 @@
   C ∈ {4}
   __malloc_main_l12 ∈ {3}
 [from] Computing for function main
-[from] Computing for function Frama_C_malloc_fresh <-main
-[from] Done for function Frama_C_malloc_fresh
+[from] Computing for function malloc <-main
+[from] Done for function malloc
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_malloc_fresh:
+[from] Function malloc:
   __fc_heap_status FROM __fc_heap_status; size (and SELF)
   \result FROM __fc_heap_status; size
 [from] Function main:
diff --git a/tests/builtins/oracle/malloc_memexec.res.oracle b/tests/builtins/oracle/malloc_memexec.res.oracle
index f996d1a7b6c825b554f371750e4ac23b3630e3c6..4e64150236a87c592acaac67623c7fe26cc34f24 100644
--- a/tests/builtins/oracle/malloc_memexec.res.oracle
+++ b/tests/builtins/oracle/malloc_memexec.res.oracle
@@ -4,67 +4,65 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   v ∈ [--..--]
-[eva] tests/builtins/malloc_memexec.c:19: Call to builtin Frama_C_malloc_fresh
-[eva] tests/builtins/malloc_memexec.c:19: allocating variable __malloc_main_l19
+[eva] tests/builtins/malloc_memexec.c:14: Call to builtin malloc
+[eva] tests/builtins/malloc_memexec.c:14: allocating variable __malloc_main_l14
 [eva] computing for function f <- main.
-  Called from tests/builtins/malloc_memexec.c:21.
+  Called from tests/builtins/malloc_memexec.c:16.
 [eva] Recording results for f
 [eva] Done for function f
 [eva] computing for function f <- main.
-  Called from tests/builtins/malloc_memexec.c:22.
+  Called from tests/builtins/malloc_memexec.c:17.
 [eva] Recording results for f
 [eva] Done for function f
 [eva] computing for function f <- main.
-  Called from tests/builtins/malloc_memexec.c:24.
+  Called from tests/builtins/malloc_memexec.c:19.
 [eva] Recording results for f
 [eva] Done for function f
-[eva] tests/builtins/malloc_memexec.c:27: 
-  Call to builtin Frama_C_malloc_fresh_weak
-[eva] tests/builtins/malloc_memexec.c:27: 
-  allocating weak variable __malloc_w_main_l27
+[eva] tests/builtins/malloc_memexec.c:23: Call to builtin malloc
+[eva] tests/builtins/malloc_memexec.c:23: 
+  allocating weak variable __malloc_w_main_l23
 [eva] computing for function f <- main.
-  Called from tests/builtins/malloc_memexec.c:29.
+  Called from tests/builtins/malloc_memexec.c:25.
 [eva] Recording results for f
 [eva] Done for function f
 [eva] computing for function f <- main.
-  Called from tests/builtins/malloc_memexec.c:30.
+  Called from tests/builtins/malloc_memexec.c:26.
 [eva] Recording results for f
 [eva] Done for function f
 [eva] computing for function f <- main.
-  Called from tests/builtins/malloc_memexec.c:32.
+  Called from tests/builtins/malloc_memexec.c:28.
 [eva] Recording results for f
 [eva] Done for function f
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function f:
-  __malloc_main_l19 ∈ {1; 2}
-  __malloc_w_main_l27[0] ∈ {1; 2} or UNINITIALIZED
+  __malloc_main_l14 ∈ {1; 2}
+  __malloc_w_main_l23[0] ∈ {1; 2} or UNINITIALIZED
 [eva:final-states] Values at end of function main:
-  p ∈ {{ &__malloc_main_l19 }}
-  q ∈ {{ &__malloc_w_main_l27[0] }}
-  __malloc_main_l19 ∈ {1}
-  __malloc_w_main_l27[0] ∈ {1; 2} or UNINITIALIZED
+  __fc_heap_status ∈ [--..--]
+  p ∈ {{ &__malloc_main_l14 }}
+  q ∈ {{ &__malloc_w_main_l23[0] }}
+  __malloc_main_l14 ∈ {1}
+  __malloc_w_main_l23[0] ∈ {1; 2} or UNINITIALIZED
 [from] Computing for function f
 [from] Done for function f
 [from] Computing for function main
-[from] Computing for function Frama_C_malloc_fresh <-main
-[from] Done for function Frama_C_malloc_fresh
-[from] Computing for function Frama_C_malloc_fresh_weak <-main
-[from] Done for function Frama_C_malloc_fresh_weak
+[from] Computing for function malloc <-main
+[from] Done for function malloc
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_malloc_fresh:
-  \result FROM ANYTHING(origin:Unknown)
-[from] Function Frama_C_malloc_fresh_weak:
-  \result FROM ANYTHING(origin:Unknown)
 [from] Function f:
-  __malloc_main_l19 FROM p; i (and SELF)
-  __malloc_w_main_l27[0] FROM p; i (and SELF)
+  __malloc_main_l14 FROM p; i (and SELF)
+  __malloc_w_main_l23[0] FROM p; i (and SELF)
+[from] Function malloc:
+  __fc_heap_status FROM __fc_heap_status; size (and SELF)
+  \result FROM __fc_heap_status; size
 [from] Function main:
-  __malloc_main_l19 FROM ANYTHING(origin:Unknown) (and SELF)
-  __malloc_w_main_l27[0] FROM ANYTHING(origin:Unknown) (and SELF)
+  __fc_heap_status FROM __fc_heap_status (and SELF)
+  __malloc_main_l14 FROM __fc_heap_status; v (and SELF)
+  __malloc_w_main_l23[0] FROM __fc_heap_status; v (and SELF)
 [from] ====== END OF DEPENDENCIES ======
 [inout] InOut (internal) for function f:
   Operational inputs:
@@ -75,8 +73,8 @@
     \nothing
 [inout] InOut (internal) for function main:
   Operational inputs:
-    v
+    __fc_heap_status; v
   Operational inputs on termination:
-    v
+    __fc_heap_status; v
   Sure outputs:
-    p; q; __malloc_main_l19
+    p; q; __malloc_main_l14
diff --git a/tests/builtins/oracle/realloc.res.oracle b/tests/builtins/oracle/realloc.res.oracle
index 9555b2ee2355ad999ed6d8af372676fe1b6171f4..c18f992849bb8e7fb4e3d609a6cb3b552e6fb608 100644
--- a/tests/builtins/oracle/realloc.res.oracle
+++ b/tests/builtins/oracle/realloc.res.oracle
@@ -6,8 +6,7 @@
   v ∈ [--..--]
 [eva] computing for function main1 <- main.
   Called from tests/builtins/realloc.c:160.
-[eva] tests/builtins/realloc.c:12: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:12: Call to builtin malloc
 [eva] tests/builtins/realloc.c:12: allocating variable __malloc_main1_l12
 [eva] tests/builtins/realloc.c:15: 
   Frama_C_dump_each:
@@ -79,8 +78,7 @@
 [eva] tests/builtins/realloc.c:22: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/builtins/realloc.c:23: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:23: Call to builtin malloc
 [eva] tests/builtins/realloc.c:23: allocating variable __malloc_main2_l23
 [eva:alarm] tests/builtins/realloc.c:24: Warning: 
   out of bounds write. assert \valid(r + i);
@@ -126,11 +124,9 @@
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
   Called from tests/builtins/realloc.c:162.
-[eva] tests/builtins/realloc.c:32: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:32: Call to builtin malloc
 [eva] tests/builtins/realloc.c:32: allocating variable __malloc_main3_l32
-[eva] tests/builtins/realloc.c:35: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:35: Call to builtin malloc
 [eva] tests/builtins/realloc.c:35: allocating variable __malloc_main3_l35
 [eva] computing for function Frama_C_interval <- main3 <- main.
   Called from tests/builtins/realloc.c:39.
@@ -235,11 +231,9 @@
 [eva] tests/builtins/realloc.c:54: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/builtins/realloc.c:55: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:55: Call to builtin malloc
 [eva] tests/builtins/realloc.c:55: allocating variable __malloc_main4_l55
-[eva] tests/builtins/realloc.c:56: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:56: Call to builtin malloc
 [eva] tests/builtins/realloc.c:56: allocating variable __malloc_main4_l56
 [eva:alarm] tests/builtins/realloc.c:59: Warning: 
   out of bounds write. assert \valid(q + i);
@@ -362,8 +356,7 @@
 [eva] Done for function main4
 [eva] computing for function main5 <- main.
   Called from tests/builtins/realloc.c:164.
-[eva] tests/builtins/realloc.c:76: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:76: Call to builtin malloc
 [eva] tests/builtins/realloc.c:76: allocating variable __malloc_main5_l76
 [eva] computing for function Frama_C_interval <- main5 <- main.
   Called from tests/builtins/realloc.c:78.
@@ -450,8 +443,7 @@
 [eva] tests/builtins/realloc.c:92: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/builtins/realloc.c:93: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:93: Call to builtin malloc
 [eva] tests/builtins/realloc.c:93: allocating variable __malloc_main6_l93
 [eva] tests/builtins/realloc.c:102: 
   Frama_C_show_each: {{ &x ; &__malloc_main6_l93 + {4} }}
@@ -467,8 +459,7 @@
 [eva] Done for function main6
 [eva] computing for function main7 <- main.
   Called from tests/builtins/realloc.c:166.
-[eva] tests/builtins/realloc.c:110: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:110: Call to builtin malloc
 [eva] tests/builtins/realloc.c:110: allocating variable __malloc_main7_l110
 [eva] tests/builtins/realloc.c:115: Call to builtin realloc
 [eva] tests/builtins/realloc.c:115: 
@@ -537,8 +528,7 @@
 [eva] Done for function main7
 [eva] computing for function main8 <- main.
   Called from tests/builtins/realloc.c:167.
-[eva] tests/builtins/realloc.c:123: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:123: Call to builtin malloc
 [eva] tests/builtins/realloc.c:123: allocating variable __malloc_main8_l123
 [eva] tests/builtins/realloc.c:126: Call to builtin realloc
 [eva] tests/builtins/realloc.c:126: 
@@ -579,8 +569,7 @@
 [eva] Done for function main8
 [eva] computing for function main9 <- main.
   Called from tests/builtins/realloc.c:168.
-[eva] tests/builtins/realloc.c:132: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:132: Call to builtin malloc
 [eva] tests/builtins/realloc.c:132: allocating variable __malloc_main9_l132
 [eva] tests/builtins/realloc.c:135: Call to builtin realloc
 [eva] tests/builtins/realloc.c:135: 
@@ -621,8 +610,7 @@
 [eva] Done for function main9
 [eva] computing for function main10 <- main.
   Called from tests/builtins/realloc.c:169.
-[eva] tests/builtins/realloc.c:147: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc.c:147: Call to builtin malloc
 [eva] tests/builtins/realloc.c:147: allocating variable __malloc_main10_l147
 [eva] tests/builtins/realloc.c:152: Call to builtin realloc
 [eva] tests/builtins/realloc.c:152: 
diff --git a/tests/builtins/oracle/realloc_imprecise.res.oracle b/tests/builtins/oracle/realloc_imprecise.res.oracle
index 346a55355c0f64cf362f127e98845f8691bee8b6..8bdb26d5e8e18e4fc7b05c7fa21f8029bf740621 100644
--- a/tests/builtins/oracle/realloc_imprecise.res.oracle
+++ b/tests/builtins/oracle/realloc_imprecise.res.oracle
@@ -4,8 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   v ∈ [--..--]
-[eva] tests/builtins/realloc_imprecise.c:10: 
-  Call to builtin Frama_C_malloc_imprecise for function malloc
+[eva] tests/builtins/realloc_imprecise.c:10: Call to builtin malloc
 [eva:malloc:imprecise] tests/builtins/realloc_imprecise.c:10: Warning: 
   allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main
 [eva:alarm] tests/builtins/realloc_imprecise.c:11: Warning: 
diff --git a/tests/builtins/oracle/realloc_multiple.0.res.oracle b/tests/builtins/oracle/realloc_multiple.0.res.oracle
index 9e00330021274a3cba7e16899bce6fa1d0937cc8..777d99715e8d72f9cc7205f6b99b225cbcb53fbb 100644
--- a/tests/builtins/oracle/realloc_multiple.0.res.oracle
+++ b/tests/builtins/oracle/realloc_multiple.0.res.oracle
@@ -6,11 +6,9 @@
   
 [eva] computing for function main1 <- main.
   Called from tests/builtins/realloc_multiple.c:75.
-[eva] tests/builtins/realloc_multiple.c:9: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:9: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:9: allocating variable __malloc_main1_l9
-[eva] tests/builtins/realloc_multiple.c:12: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:12: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:12: 
   allocating variable __malloc_main1_l12
 [eva] computing for function Frama_C_interval <- main1 <- main.
@@ -97,12 +95,10 @@
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
   Called from tests/builtins/realloc_multiple.c:76.
-[eva] tests/builtins/realloc_multiple.c:30: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:30: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:30: 
   allocating variable __malloc_main2_l30
-[eva] tests/builtins/realloc_multiple.c:33: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:33: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:33: 
   allocating variable __malloc_main2_l33
 [eva] computing for function Frama_C_interval <- main2 <- main.
@@ -196,12 +192,10 @@
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
   Called from tests/builtins/realloc_multiple.c:77.
-[eva] tests/builtins/realloc_multiple.c:52: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:52: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:52: 
   allocating variable __malloc_main3_l52
-[eva] tests/builtins/realloc_multiple.c:53: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:53: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:53: 
   allocating variable __malloc_main3_l53
 [eva] computing for function Frama_C_interval <- main3 <- main.
diff --git a/tests/builtins/oracle/realloc_multiple.1.res.oracle b/tests/builtins/oracle/realloc_multiple.1.res.oracle
index facf3d7f3a3a3e0b1b85fec505165e2a5f702320..be93b554e712d4482fb6ba182845b45330a90630 100644
--- a/tests/builtins/oracle/realloc_multiple.1.res.oracle
+++ b/tests/builtins/oracle/realloc_multiple.1.res.oracle
@@ -6,15 +6,13 @@
   
 [eva] computing for function main1 <- main.
   Called from tests/builtins/realloc_multiple.c:75.
-[eva] tests/builtins/realloc_multiple.c:9: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:9: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:9: allocating variable __malloc_main1_l9
 [eva:alarm] tests/builtins/realloc_multiple.c:10: Warning: 
   out of bounds write. assert \valid(q + i);
 [kernel] tests/builtins/realloc_multiple.c:10: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
-[eva] tests/builtins/realloc_multiple.c:12: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:12: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:12: 
   allocating variable __malloc_main1_l12
 [eva:alarm] tests/builtins/realloc_multiple.c:13: Warning: 
@@ -134,16 +132,14 @@
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
   Called from tests/builtins/realloc_multiple.c:76.
-[eva] tests/builtins/realloc_multiple.c:30: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:30: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:30: 
   allocating variable __malloc_main2_l30
 [eva:alarm] tests/builtins/realloc_multiple.c:31: Warning: 
   out of bounds write. assert \valid(q + i);
 [kernel] tests/builtins/realloc_multiple.c:31: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
-[eva] tests/builtins/realloc_multiple.c:33: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:33: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:33: 
   allocating variable __malloc_main2_l33
 [eva:alarm] tests/builtins/realloc_multiple.c:34: Warning: 
@@ -270,16 +266,13 @@
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
   Called from tests/builtins/realloc_multiple.c:77.
-[eva] tests/builtins/realloc_multiple.c:52: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:52: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:52: 
   allocating variable __malloc_main3_l52
-[eva] tests/builtins/realloc_multiple.c:53: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:53: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:53: 
   allocating variable __malloc_main3_l53
-[eva] tests/builtins/realloc_multiple.c:53: 
-  Call to builtin Frama_C_malloc_fresh for function malloc
+[eva] tests/builtins/realloc_multiple.c:53: Call to builtin malloc
 [eva] tests/builtins/realloc_multiple.c:53: 
   allocating variable __malloc_main3_l53_0
 [eva:alarm] tests/builtins/realloc_multiple.c:57: Warning: 
diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle
index c6859df65a9866ee566f9514128b1249f697875a..37622a4661e535a999a35b086a3d4f101dd16d0e 100644
--- a/tests/libc/oracle/stdlib_c.0.res.oracle
+++ b/tests/libc/oracle/stdlib_c.0.res.oracle
@@ -5,7 +5,7 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] tests/libc/stdlib_c.c:14: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:14: allocating variable __calloc_main_l14
 [eva] tests/libc/stdlib_c.c:16: assertion got status valid.
 [eva] computing for function Frama_C_size_t_interval <- main.
@@ -18,61 +18,61 @@
   Called from tests/libc/stdlib_c.c:20.
 [eva] Done for function Frama_C_size_t_interval
 [eva] tests/libc/stdlib_c.c:21: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:21: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva] tests/libc/stdlib_c.c:21: allocating variable __calloc_main_l21
 [eva] tests/libc/stdlib_c.c:21: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:23: assertion got status valid.
 [eva] tests/libc/stdlib_c.c:27: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:27: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva] tests/libc/stdlib_c.c:27: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:27: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:27: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:28: assertion got status valid.
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:32: allocating variable __calloc_main_l32
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31) to fit 0..63
 [eva:alarm] tests/libc/stdlib_c.c:33: Warning: 
   out of bounds write. assert \valid(s + (unsigned int)(i - 1));
 [eva] tests/libc/stdlib_c.c:31: starting to merge loop iterations
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/63) to fit 0..63/95
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/95) to fit 0..63/127
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:32: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/127) to fit 0..63/34359738367
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32'
   (0..31/34359738367) to fit 0..63/34359738367
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32'
   (0..31/34359738367) to fit 0..63/34359738367
@@ -80,7 +80,7 @@
   Called from tests/libc/stdlib_c.c:37.
 [eva] share/libc/stdlib.c:196: 
   assertion 'alignment_is_a_suitable_power_of_two' got status valid.
-[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
 [eva] share/libc/stdlib.c:199: allocating variable __malloc_posix_memalign_l199
 [eva] Recording results for posix_memalign
 [eva] Done for function posix_memalign
@@ -93,7 +93,7 @@
 [eva] Done for function free
 [eva] computing for function posix_memalign <- main.
   Called from tests/libc/stdlib_c.c:39.
-[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
 [eva] share/libc/stdlib.c:199: 
   allocating variable __malloc_posix_memalign_l199_0
 [eva] Recording results for posix_memalign
diff --git a/tests/libc/oracle/stdlib_c.1.res.oracle b/tests/libc/oracle/stdlib_c.1.res.oracle
index b87733adc52dff64e5e3c6b23eb532c56cd2a6c0..430cfeea5d9f8fa392f3f0e9ee52837bc52208bc 100644
--- a/tests/libc/oracle/stdlib_c.1.res.oracle
+++ b/tests/libc/oracle/stdlib_c.1.res.oracle
@@ -5,7 +5,7 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] tests/libc/stdlib_c.c:14: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:14: allocating variable __calloc_main_l14
 [eva] tests/libc/stdlib_c.c:16: assertion got status valid.
 [eva] computing for function Frama_C_size_t_interval <- main.
@@ -15,83 +15,83 @@
   function Frama_C_size_t_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_size_t_interval
 [eva] tests/libc/stdlib_c.c:21: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:21: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva] tests/libc/stdlib_c.c:21: allocating variable __calloc_main_l21
 [eva] tests/libc/stdlib_c.c:23: assertion got status valid.
 [eva] tests/libc/stdlib_c.c:27: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:27: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva] tests/libc/stdlib_c.c:27: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:28: assertion got status valid.
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:32: allocating variable __calloc_main_l32
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31) to fit 0..63
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/63) to fit 0..63
 [eva:alarm] tests/libc/stdlib_c.c:33: Warning: 
   out of bounds write. assert \valid(s + (unsigned int)(i - 1));
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/63) to fit 0..95
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/95) to fit 0..95
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/95) to fit 0..127
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/127) to fit 0..127
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/127) to fit 0..159
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/159) to fit 0..159
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/159) to fit 0..191
 [eva] tests/libc/stdlib_c.c:31: starting to merge loop iterations
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/191) to fit 0..191/223
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/223) to fit 0..191/255
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva] tests/libc/stdlib_c.c:32: Warning: 
   calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32' (0..31/255) to fit 0..191/34359738367
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32'
   (0..31/34359738367) to fit 0..191/34359738367
 [eva] tests/libc/stdlib_c.c:32: 
-  Call to builtin Frama_C_calloc_by_stack for function calloc
+  Call to builtin Frama_C_calloc for function calloc
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32'
   (0..31/34359738367) to fit 0..191/34359738367
@@ -99,7 +99,7 @@
   Called from tests/libc/stdlib_c.c:37.
 [eva] share/libc/stdlib.c:196: 
   assertion 'alignment_is_a_suitable_power_of_two' got status valid.
-[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
 [eva] share/libc/stdlib.c:199: allocating variable __malloc_posix_memalign_l199
 [eva] Recording results for posix_memalign
 [eva] Done for function posix_memalign
@@ -112,7 +112,7 @@
 [eva] Done for function free
 [eva] computing for function posix_memalign <- main.
   Called from tests/libc/stdlib_c.c:39.
-[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
 [eva] share/libc/stdlib.c:199: 
   allocating variable __malloc_posix_memalign_l199_0
 [eva] Recording results for posix_memalign
diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle
index fbcbc924edbd2afa3d722765d61531a826a64d72..70c7ee08e99296fccc2a6c4343097a301d929b71 100644
--- a/tests/libc/oracle/stdlib_c.2.res.oracle
+++ b/tests/libc/oracle/stdlib_c.2.res.oracle
@@ -6,7 +6,7 @@
   
 [eva] computing for function calloc <- main.
   Called from tests/libc/stdlib_c.c:14.
-[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
 [eva] share/libc/stdlib.c:72: allocating variable __malloc_calloc_l72
 [eva] computing for function memset <- calloc <- main.
   Called from share/libc/stdlib.c:73.
@@ -27,7 +27,7 @@
 [eva] Done for function Frama_C_size_t_interval
 [eva] computing for function calloc <- main.
   Called from tests/libc/stdlib_c.c:21.
-[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
 [eva] share/libc/stdlib.c:72: allocating variable __malloc_calloc_l72_0
 [eva] computing for function memset <- calloc <- main.
   Called from share/libc/stdlib.c:73.
@@ -44,7 +44,7 @@
 [eva] tests/libc/stdlib_c.c:28: assertion got status valid.
 [eva] computing for function calloc <- main.
   Called from tests/libc/stdlib_c.c:32.
-[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
 [eva] share/libc/stdlib.c:72: allocating variable __malloc_calloc_l72_1
 [eva] computing for function memset <- calloc <- main.
   Called from share/libc/stdlib.c:73.
@@ -54,7 +54,7 @@
 [eva] tests/libc/stdlib_c.c:31: starting to merge loop iterations
 [eva] computing for function calloc <- main.
   Called from tests/libc/stdlib_c.c:32.
-[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
 [eva] computing for function memset <- calloc <- main.
   Called from share/libc/stdlib.c:73.
 [eva] Done for function memset
@@ -64,7 +64,7 @@
   out of bounds write. assert \valid(s + (unsigned int)(i - 1));
 [eva] computing for function calloc <- main.
   Called from tests/libc/stdlib_c.c:32.
-[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
 [eva] computing for function memset <- calloc <- main.
   Called from share/libc/stdlib.c:73.
 [eva] Done for function memset
@@ -72,7 +72,7 @@
 [eva] Done for function calloc
 [eva] computing for function calloc <- main.
   Called from tests/libc/stdlib_c.c:32.
-[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
 [eva] computing for function memset <- calloc <- main.
   Called from share/libc/stdlib.c:73.
 [eva] Done for function memset
@@ -80,7 +80,7 @@
 [eva] Done for function calloc
 [eva] computing for function calloc <- main.
   Called from tests/libc/stdlib_c.c:32.
-[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
 [eva] computing for function memset <- calloc <- main.
   Called from share/libc/stdlib.c:73.
 [eva] Done for function memset
@@ -88,7 +88,7 @@
 [eva] Done for function calloc
 [eva] computing for function calloc <- main.
   Called from tests/libc/stdlib_c.c:32.
-[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:72: Call to builtin Frama_C_malloc
 [eva] computing for function memset <- calloc <- main.
   Called from share/libc/stdlib.c:73.
 [eva] Done for function memset
@@ -98,7 +98,7 @@
   Called from tests/libc/stdlib_c.c:37.
 [eva] share/libc/stdlib.c:196: 
   assertion 'alignment_is_a_suitable_power_of_two' got status valid.
-[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
 [eva] share/libc/stdlib.c:199: allocating variable __malloc_posix_memalign_l199
 [eva] Recording results for posix_memalign
 [eva] Done for function posix_memalign
@@ -111,7 +111,7 @@
 [eva] Done for function free
 [eva] computing for function posix_memalign <- main.
   Called from tests/libc/stdlib_c.c:39.
-[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:199: Call to builtin Frama_C_malloc
 [eva] share/libc/stdlib.c:199: 
   allocating variable __malloc_posix_memalign_l199_0
 [eva] Recording results for posix_memalign