diff --git a/doc/value/main.tex b/doc/value/main.tex
index 96d66840582568d5262abe620678ac86a58c9c23..0afcb450bff549d6154ee7f9f9d44de778deaae3 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -2605,7 +2605,8 @@ void init_analyzable(void)
 \label{dyn-alloc}
 
 Dynamic allocation is modeled by creating new bases.
-Each call to \lstinline|malloc| and \lstinline|realloc| potentially creates a
+Each call to \lstinline|malloc|/\lstinline|realloc|/\lstinline|calloc|
+potentially creates a
 new base, depending on the \emph{builtins} (described in section~\ref{libc})
 used -- possibly resulting in an unbounded number of such bases.
 Dynamically allocated bases behave mostly like statically allocated ones,
@@ -4975,8 +4976,8 @@ You can also manually specify each builtin to be used with option
 \lstinline|-eva-builtin|, which takes pairs of functions:
 the function to be replaced, and the name of the builtin that replaces it.
 For instance, option
-\lstinline|-eva-builtin malloc:Frama_C_malloc_fresh,free:Frama_C_free| enables
-builtins for the \lstinline|malloc| and \lstinline|free| functions of the
+\lstinline|-eva-builtin sin:Frama_C_sin,strlen:Frama_C_strlen| enables
+builtins for the \lstinline|sin| and \lstinline|strlen| functions of the
 standard library. Note that even if a builtin is specified this way,
 the function still needs to be declared to be used.
 %
@@ -5035,27 +5036,27 @@ and convergence (termination) when needed. Some differences between the
 \emph{strong} and \emph{weak} bases allocated by these builtins are
 explained in section~\ref{dyn-alloc}.
 
-\begin{table}[!ht]
-  \centering
-  \begin{tabular}{|c|c|c|}
-    \hline
-    C library function & Weak (always terminates) & Strong (more precise) \\
-    \hline
-    malloc & \lstinline|Frama_C_malloc_by_stack| & \lstinline|Frama_C_malloc_fresh| \\
-    calloc & \lstinline|Frama_C_calloc_by_stack| & \lstinline|Frama_C_calloc_fresh| \\
-    realloc & \lstinline|Frama_C_realloc| & \lstinline|Frama_C_realloc_multiple| \\
-    free & \multicolumn{2}{c|}{\lstinline|Frama_C_free|} \\
-    \hline
-  \end{tabular}\label{tab:alloc}
-  \caption{\FramaC builtins for dynamic allocation functions}
-\end{table}
+Option \lstinline|-eva-alloc-builtin| selects the behavior for allocation
+builtins, among the following:
 
-Note that function \lstinline|free| has a single builtin for both cases.
+\begin{description}
+\item[\texttt{by\_stack}]: create a few bases per callstack (the exact number
+  is given by option \lstinline|-eva-mlevel|, detailed later).
+  Always converges. This is the default value.
+\item[\texttt{fresh}]: create a new strong base for each call. The most
+  precise builtin, but may not converge (e.g. when called inside a loop).
+\item[\texttt{fresh\_weak}]: like the previous one, but using weak bases.
+\item[\texttt{imprecise}]: use a single, imprecise base, for {\em all}
+  allocations. Always converges.
+\end{description}
+
+The behavior of \lstinline|-eva-alloc-builtin| is global, unless overridden by
+{\em allocation annotations}, described below.
 
-Generally speaking, the safest approach is to start with the builtins on the
-left (\emph{weak}), to ensure that the analysis will terminate.
+Generally speaking, the safest approach is to start with the default builtin
+(\texttt{by\_stack}), to ensure that the analysis will terminate.
 If the results are imprecise, and the allocation function is not called inside
-a loop, then the strong variant may be tried. If you are mistaken, and the
+a loop, then the \texttt{fresh} variant may be tried. If you are mistaken, and the
 analysis starts diverging, it will print (by default) several messages of this
 form:
 
@@ -5068,11 +5069,21 @@ This indicates that new bases are being created.
 You must then manually interrupt the analysis and either unroll the loop
 entirely (see Section~\ref{loop-unroll}) or use a weak variant.
 
-By default, \emph{weak} builtins are used, but usage of
-\lstinline|-eva-builtin| takes precedence over preexisting associations.
-Another possibility is to call e.g. \lstinline|Frama_C_malloc_fresh| manually,
-for the allocations that are guaranteed to occur a finite number of times.
+\paragraph{Dynamic allocation annotations}
+
+The behavior of option \lstinline|-eva-alloc-builtin| can be locally overridden
+via \lstinline|eva_allocate| annotations preceding calls to dynamic allocation
+functions.
+For instance, the following annotation ensures that the call to
+\lstinline|calloc| below will use the \lstinline|fresh| builtin,
+regardless of the value of option \lstinline|-eva-alloc-builtin|:
+
+\begin{lstlisting}
+  /*@ eva_allocate fresh; */
+  part = (char*)calloc(plen + 1, sizeof(*part));
+\end{lstlisting}
 
+Other calls to \lstinline|calloc| will be unaffected by this annotation.
 
 \paragraph{Multiple locations per callstack}
 
@@ -5088,11 +5099,16 @@ termination for other loops.
 
 \paragraph{Memory allocation failure}
 
-By default, the memory allocation builtins in \Eva{} consider that
+By default, stdlib-related memory allocation builtins in \Eva{}
+(that is, \lstinline|malloc|, \lstinline|calloc| and \lstinline|realloc|)
+consider that
 the allocation may fail, thus \lstinline|NULL| is always returned as a possible
 value. To change this behavior (supposing that these functions never fail),
 use option \lstinline|-eva-no-alloc-returns-null|.
 
+Note that other allocation builtins, such as \lstinline|__fc_vla_alloc|
+(for variable-length arrays) and \lstinline|alloca|, {\em never} assume
+allocation fails.
 
 \section{Parameterizing the analysis}
 
@@ -5356,15 +5372,13 @@ They are listed here for completeness.
   \begin{tabular}{llll}
     \multicolumn{3}{c}{Dynamic memory allocation builtins} \\
     \hline
-    \lstinline|Frama_C_alloc_by_stack| &
-    \lstinline|Frama_C_vla_alloc_by_stack| &
-    \lstinline|Frama_C_malloc_fresh| \\
-    \lstinline|Frama_C_calloc_by_stack| &
-    \lstinline|Frama_C_calloc_fresh| &
-    \lstinline|Frama_C_free| \\
-    \lstinline|Frama_C_realloc| &
-    \lstinline|Frama_C_realloc_multiple| &
-    \lstinline|Frama_C_vla_free|
+    \lstinline|Frama_C_malloc| &
+    \lstinline|Frama_C_alloca| &
+    \lstinline|Frama_C_vla_alloc| \\
+    \lstinline|Frama_C_calloc| &
+    \lstinline|Frama_C_free| &
+    \lstinline|Frama_C_vla_free| \\
+    \lstinline|Frama_C_realloc|
   \end{tabular}
 \end{table}
 
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index dee1382281c94136b19e06645315db71d93de60e..3387cb48196b592ded4465313f97293ec2586884 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -33,7 +33,7 @@ let () = Value_parameters.set_warn_status wkey_weak_alloc Log.Winactive
 let wkey_imprecise_alloc = Value_parameters.register_warn_category
     "malloc:imprecise"
 
-(** {1 Dynamically allocated bases} *)
+(* ---------------------- Dynamically allocated bases ----------------------- *)
 
 module Base_hptmap = Hptmap.Make
     (Base.Base)
@@ -53,7 +53,12 @@ module Dynamic_Alloc_Bases =
     end)
 let () = Ast.add_monotonic_state Dynamic_Alloc_Bases.self
 
-(** {1 Auxiliary functions} *)
+(* -------------------------- Auxiliary functions  -------------------------- *)
+
+let current_call_site () =
+  match Value_util.call_stack () with
+  | (_kf, Kstmt stmt) :: _ -> stmt
+  | _ -> Cil.dummyStmt
 
 (* Remove some parts of the callstack:
    - Remove the bottom of the call tree until we get to the call site
@@ -77,11 +82,11 @@ let call_stack_no_wrappers () =
         stack
   in
   bottom_filter stack
-;;
 
 let register_malloced_base ?(stack=call_stack_no_wrappers ()) b =
   let stack_without_top = List.tl stack in
-  Dynamic_Alloc_Bases.set (Base_hptmap.add b stack_without_top (Dynamic_Alloc_Bases.get ()))
+  Dynamic_Alloc_Bases.set
+    (Base_hptmap.add b stack_without_top (Dynamic_Alloc_Bases.get ()))
 
 let fold_dynamic_bases (f: Base.t -> Value_types.Callstack.t -> 'a -> 'a) init =
   Base_hptmap.fold f (Dynamic_Alloc_Bases.get ()) init
@@ -144,7 +149,6 @@ let base_name prefix stack =
       prefix
       (if full_name then loop_full qstack else caller qstack)
       (stmt_line callsite)
-;;
 
 type var = Weak | Strong
 
@@ -252,7 +256,6 @@ let size_sure_valid b = match Base.validity b with
   | Base.Invalid | Base.Empty | Base.Unknown (_, None, _) -> Integer.zero
   | Base.Known (_, up) | Base.Unknown (_, Some up, _)
   | Base.Variable { Base.min_alloc = up } -> Integer.succ up
-;;
 
 (* Create a new offsetmap initialized to [bottom] on the entire allocable
    range, with the first [max_alloc] bits set to [v].
@@ -293,9 +296,8 @@ let add_zeroes = add_v (V_Or_Uninitialized.initialized Cvalue.V.singleton_zero)
    [ret]: result in case of success (e.g. a new base in case of malloc);
    [orig_state]: state before any allocation, returned in case of failure;
    [state_after_alloc]: state in case the allocation is successful;
-   [returns_null]: if given, forces the result to consider/ignore the possibility
-   of failure, despite -val-alloc-returns-null.
-*)
+   [returns_null]: if given, forces the result to consider/ignore the
+   possibility of failure, despite -val-alloc-returns-null. *)
 let wrap_fallible_alloc ?returns_null ret orig_state state_after_alloc =
   let default_returns_null = Value_parameters.AllocReturnsNull.get () in
   let returns_null = Extlib.opt_conv default_returns_null returns_null in
@@ -312,14 +314,14 @@ let pp_validity fmt (v1, v2) =
   else Format.fprintf fmt "0..%a/%a" Int.pretty v1 Int.pretty v2
 
 
-(** {1 Malloc} *)
+(* --------------------------------- Malloc --------------------------------- *)
 
-(* Create a new variable of size [sizev] with deallocation type [deallocation],
-   using [stack] to infer a type.
+(* Create a new variable of size [sizev] with deallocation type [deallocation].
    Returns the new base, and its maximum validity.
    Note that [_state] is not used, but it is present to ensure a compatible
    signature with [alloc_by_stack]. *)
-let alloc_abstract weak deallocation stack prefix sizev _state =
+let alloc_fresh weak deallocation prefix sizev _state =
+  let stack = call_stack_no_wrappers () in
   let tsize = guess_intended_malloc_type stack sizev (weak = Strong) in
   let type_base = type_from_nb_elems tsize in
   let var = create_new_var stack prefix type_base weak in
@@ -337,35 +339,11 @@ let alloc_abstract weak deallocation stack prefix sizev _state =
   (* note that min_alloc may be negative (-1) if the allocated size is 0 *)
   let weak = match weak with Weak -> true | Strong -> false in
   let variable_v = Base.create_variable_validity ~weak ~min_alloc ~max_alloc in
-  let new_base = Base.register_allocated_var var deallocation (Base.Variable variable_v) in
+  let validity = Base.Variable variable_v in
+  let new_base = Base.register_allocated_var var deallocation validity in
   register_malloced_base ~stack new_base;
   new_base, max_alloc
 
-(* Simplest allocation function: a new base each time, of the required size. *)
-let alloc_fresh ?(prefix="malloc") weak region state actuals =
-  match actuals with
-  | [_, size, _] ->
-    let stack = call_stack_no_wrappers () in
-    let base, max_valid = alloc_abstract weak region stack prefix size state in
-    let new_state = add_uninitialized state base max_valid in
-    let ret = V.inject base Ival.zero in
-    let c_values = wrap_fallible_alloc ret state new_state in
-    { Value_types.c_values = c_values ;
-      c_clobbered = Base.SetLattice.bottom;
-      c_cacheable = Value_types.NoCacheCallers;
-      c_from = None;
-    }
-  | _ -> raise (Builtins.Invalid_nb_of_args 1)
-
-let () =
-  Builtins.register_builtin "Frama_C_malloc_fresh"
-    (alloc_fresh Strong Base.Malloc)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
-let () =
-  Builtins.register_builtin "Frama_C_malloc_fresh_weak"
-    (alloc_fresh Weak Base.Malloc)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
-
 module Base_with_Size = Datatype.Pair (Base.Base) (Datatype.Integer)
 
 (* Extremely aggressive and imprecise allocation: a single weak base for each
@@ -400,7 +378,7 @@ let string_of_region = function
   | Base.Alloca -> "via alloca"
 
 (* Only called when the 'weakest base' needs to be allocated. *)
-let alloc_imprecise_weakest_alloc region =
+let create_weakest_base region =
   let stack = [ fst (Globals.entry_point ()), Kglobal ] in
   let type_base =
     TArray (Cil.charType, None, Cil.empty_size_cache (), [])
@@ -414,100 +392,20 @@ let alloc_imprecise_weakest_alloc region =
   let variable_v =
     Base.create_variable_validity ~weak:true ~min_alloc ~max_alloc
   in
-  let new_base = Base.register_allocated_var var region (Base.Variable variable_v) in
+  let validity = Base.Variable variable_v in
+  let new_base = Base.register_allocated_var var region validity in
   register_malloced_base ~stack new_base;
   new_base, max_alloc
 
 (* used by calloc_abstract *)
-let alloc_imprecise_weakest_abstract region =
+let alloc_weakest_base region =
   let memo =
     match region with
     | Base.Malloc -> MallocedSingleMalloc.memo
     | Base.VLA -> MallocedSingleVLA.memo
     | Base.Alloca -> MallocedSingleAlloca.memo
   in
-  memo (fun () -> alloc_imprecise_weakest_alloc region)
-
-let alloc_imprecise_weakest_aux region _stack _prefix _sizev state =
-  let new_base, max_alloc = alloc_imprecise_weakest_abstract region in
-  let new_state = add_uninitialized state new_base max_alloc in
-  let ret = V.inject new_base Ival.zero in
-  ret, new_state
-
-let alloc_imprecise_weakest ?returns_null region state actuals =
-  match actuals with
-  | [_, _size, _] ->
-    begin
-      let ret, new_state = alloc_imprecise_weakest_aux region [] "" _size state in
-      let c_values = wrap_fallible_alloc ?returns_null ret state new_state in
-      { Value_types.c_values = c_values ;
-        c_clobbered = Base.SetLattice.bottom;
-        c_cacheable = Value_types.NoCacheCallers;
-        c_from = None;
-      }
-    end
-  | _ -> raise (Builtins.Invalid_nb_of_args 1)
-
-let () = Builtins.register_builtin
-    "Frama_C_malloc_imprecise" (alloc_imprecise_weakest Base.Malloc)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
-
-let zero_to_max_bytes () = Ival.inject_range
-    (Some Integer.zero) (Some (Bit_utils.max_byte_size ()))
-
-let alloc_size_ok intended_size =
-  try
-    let size = Cvalue.V.project_ival intended_size in
-    let ok_size = zero_to_max_bytes () in
-    if Ival.is_included size ok_size then Alarmset.True
-    else if Ival.intersects size ok_size then Alarmset.Unknown
-    else Alarmset.False
-  with Cvalue.V.Not_based_on_null -> Alarmset.Unknown (* garbled mix in size *)
-
-(* Generic function used both by [calloc_size] and [calloc_by_stack].
-   [calloc_f] is the actual function used (calloc_size or calloc_by_stack). *)
-let calloc_abstract calloc_f state actuals =
-  let stack = call_stack_no_wrappers () in
-  let nmemb, sizev =
-    match actuals with
-    | [(_exp, nmemb, _); (_, size, _)] -> nmemb, size
-    | _ -> raise (Builtins.Invalid_nb_of_args 2)
-  in
-  let alloc_size = Cvalue.V.mul nmemb sizev in
-  let size_ok = alloc_size_ok alloc_size in
-  if size_ok <> Alarmset.True then
-    Value_util.warning_once_current
-      "calloc out of bounds: assert(nmemb * size <= SIZE_MAX)";
-  if size_ok = Alarmset.False then (* size always overflows *)
-    { Value_types.c_values = [Eval_op.wrap_ptr Cvalue.V.singleton_zero, state];
-      c_clobbered = Base.SetLattice.bottom;
-      c_cacheable = Value_types.NoCacheCallers;
-      c_from = None;
-    }
-  else
-    let base, max_valid = calloc_f stack "calloc" alloc_size state in
-    let new_state = add_zeroes state base max_valid in
-    let returns_null = if size_ok = Alarmset.Unknown then Some true else None in
-    let ret = V.inject base Ival.zero in
-    let c_values = wrap_fallible_alloc ?returns_null ret state new_state in
-    { Value_types.c_values = c_values ;
-      c_clobbered = Base.SetLattice.bottom;
-      c_cacheable = Value_types.NoCacheCallers;
-      c_from = None;
-    }
-
-(* Equivalent to [malloc_fresh], but for [calloc]. *)
-let calloc_fresh weak state actuals =
-  calloc_abstract (alloc_abstract weak Base.Malloc) state actuals
-
-let () =
-  Builtins.register_builtin "Frama_C_calloc_fresh" (calloc_fresh Strong)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
-                                       Cil.theMachine.Cil.typeOfSizeOf]))
-let () =
-  Builtins.register_builtin "Frama_C_calloc_fresh_weak" (calloc_fresh Weak)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
-                                       Cil.theMachine.Cil.typeOfSizeOf]))
+  memo (fun () -> create_weakest_base region)
 
 (* Variables that have been returned by a call to an allocation function
    at this callstack. The first allocated variable is at the top of the
@@ -551,7 +449,8 @@ let update_variable_validity ?(make_weak=false) base sizev =
     base, max_valid_bits
   | _ -> Value_parameters.fatal "base is not Allocated: %a" Base.pretty base
 
-let alloc_by_stack_aux region stack prefix sizev state =
+let alloc_by_stack region prefix sizev state =
+  let stack = call_stack_no_wrappers () in
   let max_level = Value_parameters.MallocLevel.get () in
   let all_vars =
     try MallocedByStack.find stack
@@ -560,7 +459,7 @@ let alloc_by_stack_aux region stack prefix sizev state =
   let rec aux nb vars =
     match vars with
     | [] -> (* must allocate a new variable *)
-      let b, _ as r = alloc_abstract Strong region stack prefix sizev state in
+      let b, _ as r = alloc_fresh Strong region prefix sizev state in
       MallocedByStack.replace stack (all_vars @ [b]);
       r
     | b :: q ->
@@ -575,66 +474,93 @@ let alloc_by_stack_aux region stack prefix sizev state =
   in
   aux 0 all_vars
 
-(* For each callstack, the first MallocPrecision.get() are precise fresh
-   distinct locations. The following allocations all return the same
-   base, first strong, then weak, and which is extended as needed. *)
-let alloc_by_stack ?(prefix="malloc") region ?returns_null : Db.Value.builtin = fun state actuals->
-  let stack = call_stack_no_wrappers () in
-  let sizev = match actuals with
-    | [_,size,_] -> size
-    | _ -> raise (Builtins.Invalid_nb_of_args 1)
+let choose_base_allocation () =
+  let open Eva_annotations in
+  match get_allocation (current_call_site ()) with
+  | Fresh -> alloc_fresh Strong
+  | Fresh_weak -> alloc_fresh Weak
+  | By_stack -> alloc_by_stack
+  | Imprecise -> fun region _ _ _ -> alloc_weakest_base region
+
+let register_malloc ?replace name ?returns_null prefix region =
+  let builtin state args =
+    let size = match args with
+      | [ _, size, _ ] -> size
+      | _ -> raise (Builtins.Invalid_nb_of_args 1)
+    in
+    let allocate_base = choose_base_allocation () in
+    let new_base, max_alloc = allocate_base region prefix size state in
+    let new_state = add_uninitialized state new_base max_alloc in
+    let ret = V.inject new_base Ival.zero in
+    let c_values = wrap_fallible_alloc ?returns_null ret state new_state in
+    { Value_types.c_values = c_values ;
+      c_clobbered = Base.SetLattice.bottom;
+      c_cacheable = Value_types.NoCacheCallers;
+      c_from = None; }
   in
-  let base, max_valid = alloc_by_stack_aux region stack prefix sizev state in
-  let new_state = add_uninitialized state base max_valid in
-  let ret = V.inject base Ival.zero in
-  let c_values = wrap_fallible_alloc ?returns_null ret state new_state in
-  { Value_types.c_values = c_values ;
-    c_clobbered = Base.SetLattice.bottom;
-    c_from = None;
-    c_cacheable = Value_types.NoCacheCallers }
-;;
-let () = Builtins.register_builtin
-    ~replace:"malloc" "Frama_C_malloc_by_stack" (alloc_by_stack Base.Malloc)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
-let () = Builtins.register_builtin
-    ~replace:"__fc_vla_alloc" "Frama_C_vla_alloc_by_stack"
-    (alloc_by_stack Base.VLA ~returns_null:false)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
-let () = Builtins.register_builtin
-    "Frama_C_vla_alloc_imprecise"
-    (alloc_imprecise_weakest Base.VLA ~returns_null:false)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
-let () = Builtins.register_builtin
-    ~replace:"alloca" "Frama_C_alloca"
-    (alloc_by_stack ~prefix:"alloca" Base.Alloca ~returns_null:false)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
-let () = Builtins.register_builtin
-    "Frama_C_alloca_imprecise"
-    (alloc_imprecise_weakest Base.Alloca ~returns_null:false)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
-
-(* Equivalent to [alloc_by_stack], but for [calloc]. *)
-let calloc_by_stack : Db.Value.builtin = fun state actuals ->
-  calloc_abstract (alloc_by_stack_aux Base.Malloc) state actuals
-
-let () = Builtins.register_builtin
-    ~replace:"calloc" "Frama_C_calloc_by_stack" calloc_by_stack
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
-                                       Cil.theMachine.Cil.typeOfSizeOf]))
-
-(* Equivalent to [malloc_imprecise_weakest], but for [calloc]. *)
-let calloc_imprecise_weakest : Db.Value.builtin = fun state actuals ->
-  let calloc_f _stack _prefix _sizev _state =
-    alloc_imprecise_weakest_abstract Base.Malloc
+  let name = "Frama_C_" ^ name in
+  let typ () = Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf] in
+  Builtins.register_builtin ?replace name builtin ~typ
+
+let () =
+  register_malloc ~replace:"malloc" "malloc" "malloc" Base.Malloc;
+  register_malloc ~replace:"__fc_vla_alloc" "vla_alloc" "malloc" Base.VLA
+    ~returns_null:false;
+  register_malloc ~replace:"alloca" "alloca" "alloca" Base.Alloca
+    ~returns_null:false
+
+(* --------------------------------- Calloc --------------------------------- *)
+
+let zero_to_max_bytes () = Ival.inject_range
+    (Some Integer.zero) (Some (Bit_utils.max_byte_size ()))
+
+let alloc_size_ok intended_size =
+  try
+    let size = Cvalue.V.project_ival intended_size in
+    let ok_size = zero_to_max_bytes () in
+    if Ival.is_included size ok_size then Alarmset.True
+    else if Ival.intersects size ok_size then Alarmset.Unknown
+    else Alarmset.False
+  with Cvalue.V.Not_based_on_null -> Alarmset.Unknown (* garbled mix in size *)
+
+let calloc_builtin state args =
+  let nmemb, sizev =
+    match args with
+    | [(_, nmemb, _); (_, size, _)] -> nmemb, size
+    | _ -> raise (Builtins.Invalid_nb_of_args 2)
+  in
+  let size = Cvalue.V.mul nmemb sizev in
+  let size_ok = alloc_size_ok size in
+  if size_ok <> Alarmset.True then
+    Value_util.warning_once_current
+      "calloc out of bounds: assert(nmemb * size <= SIZE_MAX)";
+  let c_values =
+    if size_ok = Alarmset.False (* size always overflows *)
+    then [Eval_op.wrap_ptr Cvalue.V.singleton_zero, state]
+    else
+      let allocate_base = choose_base_allocation () in
+      let base, max_valid = allocate_base Base.Malloc "calloc" size state in
+      let new_state = add_zeroes state base max_valid in
+      let returns_null =
+        if size_ok = Alarmset.Unknown then Some true else None
+      in
+      let ret = V.inject base Ival.zero in
+      wrap_fallible_alloc ?returns_null ret state new_state
   in
-  calloc_abstract calloc_f state actuals
+  { Value_types.c_values;
+    c_clobbered = Base.SetLattice.bottom;
+    c_cacheable = Value_types.NoCacheCallers;
+    c_from = None; }
 
-let () = Builtins.register_builtin
-    "Frama_C_calloc_imprecise" calloc_imprecise_weakest
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
-                                       Cil.theMachine.Cil.typeOfSizeOf]))
+let () =
+  let name = "Frama_C_calloc" in
+  let typ () =
+    let sizeof_typ = Cil.theMachine.Cil.typeOfSizeOf in
+    Cil.voidPtrType, [ sizeof_typ; sizeof_typ ]
+  in
+  Builtins.register_builtin ~replace:"calloc" name calloc_builtin ~typ
 
-(** {1 Free} *)
+(* ---------------------------------- Free ---------------------------------- *)
 
 (* Change all references to bases into ESCAPINGADDR into the given state,
    and remove those bases from the state entirely when [exact] holds *)
@@ -783,7 +709,7 @@ let free_automatic_bases stack state =
     state'
   end
 
-(** {1 Realloc} *)
+(* -------------------------------- Realloc --------------------------------- *)
 
 (* Note: realloc never fails during read/write operations, hence we can
    always ignore the validity of locations. (We craft them ourselves anyway.)
@@ -826,12 +752,11 @@ let realloc_alloc_copy weak bases_to_realloc null_in_arg sizev state =
     Base.Hptset.pretty bases_to_realloc;
   assert (not (Model.(equal state bottom || equal state top)));
   let _size_valid, size_max = extract_size sizev in (* bytes everywhere *)
-  let stack = call_stack_no_wrappers () in
   let base, max_valid =
     let prefix = "realloc" in
     match weak with
-    | Strong -> alloc_abstract Strong Base.Malloc stack prefix sizev state
-    | Weak -> alloc_by_stack_aux Base.Malloc stack prefix sizev state
+    | Strong -> alloc_fresh Strong Base.Malloc prefix sizev state
+    | Weak -> alloc_by_stack Base.Malloc prefix sizev state
   in
   (* Make sure that [ret] will be present in the result: we bind it at least
      to bottom everywhere *)
@@ -842,7 +767,8 @@ let realloc_alloc_copy weak bases_to_realloc null_in_arg sizev state =
   let lbases = Base.Hptset.elements bases_to_realloc in
   let dst_state =
     (* uninitialized on all reallocated valid bits *)
-    let offsm = offsm_with_v V_Or_Uninitialized.uninitialized (Base.validity base) max_valid in
+    let uninit = V_Or_Uninitialized.uninitialized in
+    let offsm = offsm_with_v uninit (Base.validity base) max_valid in
     let offsm =
       if null_in_arg then offsm (* In this case, realloc may copy nothing *)
       else
@@ -872,7 +798,7 @@ let realloc_alloc_copy weak bases_to_realloc null_in_arg sizev state =
 (* Auxiliary function for [realloc]. All the bases in [bases] are realloced
    one by one, plus NULL if [null] holds. This function acts as if we had
    first made a disjunction on the pointer passed to [realloc]. *)
-let realloc_multiple state size bases null =
+let realloc_multiple bases null size state =
   (* this function should never be used with weak allocs *)
   let aux_bases b acc = Base.Hptset.singleton b :: acc in
   let lbases = Base.Hptset.fold aux_bases bases [] in
@@ -888,75 +814,51 @@ let realloc_multiple state size bases null =
     join res (realloc_alloc_copy Strong Base.Hptset.empty true size state)
   else res
 
-(* Multiple indicates that existing bases are reallocated into as many new
-   bases. *)
-let realloc ~multiple state args = match args with
-  | [ (_,ptr,_); (_,size,_) ] ->
-    let (bases, card_ok, null) = resolve_bases_to_free ptr in
-    if card_ok > 0 then
-      let orig_state = state in
-      let ret, state =
-        if multiple
-        then realloc_multiple state size bases null
-        else realloc_alloc_copy Weak bases null size state
-      in
-      (* Maybe the calls above made [ret] weak, and it
-         was among the arguments. In this case, do not free it entirely! *)
-      let weak = Base.Hptset.exists Base.is_weak bases in
-      let strong = card_ok <= 1 && not weak in
-      (* free old bases. *)
-      let state, changed = free_aux state ~strong bases in
-      let c_values = wrap_fallible_alloc ret orig_state state in
-      { Value_types.c_values;
-        c_clobbered = Builtins.clobbered_set_from_ret state ret;
-        c_cacheable = Value_types.NoCacheCallers;
-        c_from = Some changed;
-      }
-    else (* Invalid call. *)
-      { Value_types.c_values = [] ;
-        c_clobbered = Base.SetLattice.bottom;
-        c_cacheable = Value_types.NoCacheCallers;
-        c_from = None;
-      }
-  | _ -> raise (Builtins.Invalid_nb_of_args 2)
-
-let () = Builtins.register_builtin
-    ~replace:"realloc" "Frama_C_realloc" (realloc ~multiple:false)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.voidPtrType;
-                                       Cil.theMachine.Cil.typeOfSizeOf]))
-let () = Builtins.register_builtin
-    "Frama_C_realloc_multiple" (realloc ~multiple:true)
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.voidPtrType;
-                                       Cil.theMachine.Cil.typeOfSizeOf]))
-
-let realloc_imprecise_weakest state args = match args with
-  | [ (_,ptr,_); (_,_size,_) ] ->
-    let (bases, card_ok, _null) = resolve_bases_to_free ptr in
-    if card_ok > 0 then
-      let orig_state = state in
-      let ret, state = alloc_imprecise_weakest_aux Base.Malloc [] "" _size state in
-      (* free old bases. *)
-      let state, changed = free_aux state ~strong:false bases in
-      let c_values = wrap_fallible_alloc ret orig_state state in
-      { Value_types.c_values;
-        c_clobbered = Builtins.clobbered_set_from_ret state ret;
-        c_cacheable = Value_types.NoCacheCallers;
-        c_from = Some changed;
-      }
-    else (* Invalid call. *)
-      { Value_types.c_values = [] ;
-        c_clobbered = Base.SetLattice.bottom;
-        c_cacheable = Value_types.NoCacheCallers;
-        c_from = None;
-      }
-  | _ -> raise (Builtins.Invalid_nb_of_args 2)
+let realloc_imprecise_weakest _bases _null _size state =
+  let new_base, max_alloc = alloc_weakest_base Base.Malloc in
+  let state = add_uninitialized state new_base max_alloc in
+  let ret = V.inject new_base Ival.zero in
+  ret, state
+
+let choose_bases_reallocation () =
+  let open Eva_annotations in
+  match get_allocation (current_call_site ()) with
+  | Fresh | Fresh_weak -> realloc_multiple
+  | By_stack -> realloc_alloc_copy Weak
+  | Imprecise -> realloc_imprecise_weakest
+
+let realloc_builtin state args =
+  let ptr, size =
+    match args with
+    | [ (_, ptr, _); (_, size, _) ] -> ptr, size
+    | _ -> raise (Builtins.Invalid_nb_of_args 2)
+  in
+  let bases, card_ok, null = resolve_bases_to_free ptr in
+  if card_ok > 0 then
+    let realloc = choose_bases_reallocation () in
+    let ret, new_state = realloc bases null size state in
+    (* Maybe the calls above made [ret] weak, and it
+       was among the arguments. In this case, do not free it entirely! *)
+    let strong = card_ok <= 1 && not Base.(Hptset.exists is_weak bases) in
+    (* free old bases. *)
+    let new_state, changed = free_aux new_state ~strong bases in
+    let c_values = wrap_fallible_alloc ret state new_state in
+    { Value_types.c_values;
+      c_clobbered = Builtins.clobbered_set_from_ret new_state ret;
+      c_cacheable = Value_types.NoCacheCallers;
+      c_from = Some changed; }
+  else (* Invalid call. *)
+    { Value_types.c_values = [] ;
+      c_clobbered = Base.SetLattice.bottom;
+      c_cacheable = Value_types.NoCacheCallers;
+      c_from = None; }
 
-let () = Builtins.register_builtin
-    "Frama_C_realloc_imprecise" realloc_imprecise_weakest
-    ~typ:(fun () -> (Cil.voidPtrType, [Cil.voidPtrType;
-                                       Cil.theMachine.Cil.typeOfSizeOf]))
+let () =
+  let name = "Frama_C_realloc" in
+  let typ () = Cil.(voidPtrType, [voidPtrType; theMachine.typeOfSizeOf]) in
+  Builtins.register_builtin ~replace:"realloc" name realloc_builtin ~typ
 
-(** {1 Leak detection} *)
+(* ----------------------------- Leak detection ----------------------------- *)
 
 (* Experimental, not to be released, leak detection built-in. *)
 (* Check if the base_to_check is present in one of
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 042ea9ac98a32b1383f87258e67abede69715546..59d825232185d389fc4365e3bec52135f73c2780 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -34,6 +34,7 @@ type flow_annotation =
   | FlowSplit of term
   | FlowMerge of term
 
+type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
 
 (* We use two representations for annotations :
    - the high level representation (HL) which is exported from this module
@@ -248,3 +249,57 @@ module Subdivision = Register (struct
 
 let get_subdivision_annot = Subdivision.get
 let add_subdivision_annot = Subdivision.add
+
+
+module Allocation = struct
+  let of_string = function
+    | "by_stack"   -> Some By_stack
+    | "fresh"      -> Some Fresh
+    | "fresh_weak" -> Some Fresh_weak
+    | "imprecise"  -> Some Imprecise
+    | _            -> None
+
+  let to_string = function
+    | By_stack   -> "by_stack"
+    | Fresh      -> "fresh"
+    | Fresh_weak -> "fresh_weak"
+    | Imprecise  -> "imprecise"
+
+  include Register (struct
+      type t = allocation_kind
+      let name = "eva_allocate"
+      let is_loop_annot = false
+
+      let parse ~typing_context:_ = function
+        | [{lexpr_node = PLvar s}] -> Extlib.the ~exn:Parse_error (of_string s)
+        | _ -> raise Parse_error
+
+      let export alloc_kind =
+        Ext_terms [Logic_const.tstring (to_string alloc_kind)]
+
+      let import = function
+        | Ext_terms [{term_node}] ->
+          (* Be kind and return By_stack by default. Someone is bound to write a
+             visitor that will simplify our term into something unrecognizable. *)
+          begin match term_node with
+            | TConst (LStr s) -> Extlib.opt_conv By_stack (of_string s)
+            | _ -> By_stack
+          end
+        | _ -> assert false
+
+      let print fmt alloc_kind =
+        Format.pp_print_string fmt (to_string alloc_kind)
+    end)
+
+  let get stmt =
+    match get stmt with
+    | [] -> Extlib.the (of_string (Value_parameters.AllocBuiltin.get ()))
+    | [x] -> x
+    | x :: _ ->
+      Value_parameters.warning ~current:true ~once:true
+        "Several eva_allocate annotations at the same statement; selecting %s\
+         and ignoring the others." (to_string x);
+      x
+end
+
+let get_allocation = Allocation.get
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index db6cbf66799d5fea0619a06cc09989d160516604..6a7ba48f7bee2fbf74401728d580429aaa495d20 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -39,10 +39,13 @@ type flow_annotation =
   | FlowSplit of Cil_types.term
   | FlowMerge of Cil_types.term
 
+type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
+
 val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
 val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
 val get_flow_annot : Cil_types.stmt -> flow_annotation list
 val get_subdivision_annot : Cil_types.stmt -> int list
+val get_allocation: Cil_types.stmt -> allocation_kind
 
 val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location ->
   Cil_types.stmt -> slevel_annotation -> unit
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 0677d81616ea2cf154b21d2f196cff39b916a58e..82e05def8e6ce595ed5383d0d079061118c936aa 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -1415,6 +1415,25 @@ let () = add_precision_dep ReductionDepth.parameter
 (* --- Dynamic allocation                                                 --- *)
 (* -------------------------------------------------------------------------- *)
 
+let () = Parameter_customize.set_group malloc
+module AllocBuiltin =
+  String
+    (struct
+      let option_name = "-eva-alloc-builtin"
+      let help = "Select the behavior of allocation builtins. \
+                  By default, they use up to [-eva-mlevel] bases \
+                  for each callstack (<by_stack>). They can also \
+                  use one <imprecise> base for all allocations, \
+                  create a <fresh> strong base at each call, \
+                  or create a <fresh_weak> base at each call."
+      let default = "by_stack"
+      let arg_name = "imprecise|by_stack|fresh|fresh_weak"
+    end)
+let () = add_precision_dep AllocBuiltin.parameter
+let () =
+  AllocBuiltin.set_possible_values
+    ["imprecise"; "by_stack"; "fresh"; "fresh_weak"]
+
 let () = Parameter_customize.set_group malloc
 module AllocFunctions =
   Filled_string_set
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index b31c526f8648c46fb06a6677000e518e45f4f94b..8375ac554c748bc7f4a861ea546502704e168937 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -149,6 +149,7 @@ module StopAtNthAlarm: Parameter_sig.Int
 
 (** Dynamic allocation *)
 
+module AllocBuiltin: Parameter_sig.String
 module AllocFunctions: Parameter_sig.String_set
 module AllocReturnsNull: Parameter_sig.Bool
 module MallocLevel: Parameter_sig.Int
diff --git a/tests/builtins/Longinit_sequencer.ml b/tests/builtins/Longinit_sequencer.ml
index 173d3b5062e2a0be3527edf3024c4745e5e49316..e08e24d518d009ebab3543964451095e79f1f765 100644
--- a/tests/builtins/Longinit_sequencer.ml
+++ b/tests/builtins/Longinit_sequencer.ml
@@ -35,7 +35,7 @@ let main () =
   let display_results state = Format.fprintf fmt "@[%a@]@\n" !Db.Value.display state in
   Dynamic.Parameter.String.set "" "tests/builtins/long_init.c";
   Dynamic.Parameter.String.set "-eva-save-fun-state" ("init_inner:" ^ tmpfile);
-  Dynamic.Parameter.String.set "-eva-builtin" "malloc:Frama_C_malloc_fresh";
+  Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
   Dynamic.Parameter.Bool.set "-eva-alloc-returns-null" false;
   Dynamic.Parameter.String.set "-eva-warn-key" "builtins:override=inactive";
   !Db.Value.compute ();
@@ -49,7 +49,7 @@ let main () =
   Dynamic.Parameter.String.set "-eva-load-fun-state" ("init_inner:" ^ tmpfile);
   (* set builtins in a different order to force kernel to recompute
      kernel function IDs *)
-  Dynamic.Parameter.String.set "-eva-builtin" "malloc:Frama_C_malloc_fresh";
+  Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
   !Db.Value.compute ();
   Callgraph.Uses.iter_in_rev_order display_results;
   Files.clear ();
@@ -59,7 +59,7 @@ let main () =
   Dynamic.Parameter.String.set "-eva-load-fun-state" ("init_outer:" ^ tmpfile);
   (* set builtins in a different order to force kernel to recompute
      kernel function IDs *)
-  Dynamic.Parameter.String.set "-eva-builtin" "malloc:Frama_C_malloc_fresh";
+  Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
   !Db.Value.compute ();
   Callgraph.Uses.iter_in_rev_order display_results;
   ok:=true (* no error, we can erase the file *)
diff --git a/tests/builtins/alloc.c b/tests/builtins/alloc.c
index 33f24cdc7d6562f40487a3693fa2b380742edc42..36f4a7c0333c46cbd473e24fd4022abf9c670fa5 100644
--- a/tests/builtins/alloc.c
+++ b/tests/builtins/alloc.c
@@ -1,10 +1,10 @@
 /* run.config*
    GCC:
-   STDOPT: #"-eva-no-builtins-auto"
-   STDOPT: #"-eva-no-builtins-auto -absolute-valid-range 0x100-0x200 -main main_abs"
+   STDOPT: #"-eva-alloc-builtin fresh"
+   STDOPT: #"-eva-alloc-builtin fresh -absolute-valid-range 0x100-0x200 -main main_abs"
 */
 
-#define malloc(n) Frama_C_malloc_fresh(n)
+
 #include "share/libc/stdlib.c"
 
 int *p,*q,*r,a,b;
diff --git a/tests/builtins/allocated.c b/tests/builtins/allocated.c
index 5bb5091919b3bbf490fef6dc3ca2b097f3a1ddf5..b09b532881c9ef6a322b5ad7292035bbdfd3d66e 100644
--- a/tests/builtins/allocated.c
+++ b/tests/builtins/allocated.c
@@ -1,6 +1,6 @@
 /* run.config*
    STDOPT: +"-slevel 1 -eva-mlevel 0"
-   STDOPT: +"-slevel 999 -eva-builtin malloc:Frama_C_malloc_fresh,__fc_vla_alloc:Frama_C_malloc_fresh,__fc_vla_free:Frama_C_vla_free"
+   STDOPT: +"-slevel 999 -eva-alloc-builtin fresh"
 */
 #define assert_bottom(exp) if (nondet) {exp; Frama_C_show_each_unreachable();}
 
diff --git a/tests/builtins/calloc.c b/tests/builtins/calloc.c
index 391526efc854f48c1a227508470978787b60aa80..eab8069d1467719ea917befd946c6d86e54e894d 100644
--- a/tests/builtins/calloc.c
+++ b/tests/builtins/calloc.c
@@ -1,10 +1,10 @@
 /* run.config*
  STDOPT: #"-eva-no-builtins-auto -eva-alloc-returns-null"
- STDOPT: #"-eva-no-builtins-auto -eva-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_fresh"
- STDOPT: #"-eva-no-builtins-auto -eva-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_by_stack"
- STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_fresh"
- STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_by_stack"
- STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_imprecise"
+ STDOPT: #"-eva-alloc-returns-null -eva-alloc-builtin fresh"
+ STDOPT: #"-eva-alloc-returns-null -eva-alloc-builtin by_stack"
+ STDOPT: #"-eva-no-alloc-returns-null -eva-alloc-builtin fresh"
+ STDOPT: #"-eva-no-alloc-returns-null -eva-alloc-builtin by_stack"
+ STDOPT: #"-eva-no-alloc-returns-null -eva-alloc-builtin imprecise"
  */
 #include <stdlib.h>
 #include <stdint.h>
diff --git a/tests/builtins/free.c b/tests/builtins/free.c
index f6d55190835a819d9f92c5038cc9319379f1fea5..a16798e5ff968dd534fa977323c62e9eb59112fb 100644
--- a/tests/builtins/free.c
+++ b/tests/builtins/free.c
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: #" -eva-builtin malloc:Frama_C_malloc_fresh"
+   STDOPT: #" -eva-alloc-builtin fresh"
 */
 #include "stdlib.h" 
 volatile v;
diff --git a/tests/builtins/from_result.c b/tests/builtins/from_result.c
index 1076c7ca5bc3f89a20b05d2ab84271e6dd8226ab..89e1f89ae0d5a0a1eab68b623367bad8f9dcccb1 100644
--- a/tests/builtins/from_result.c
+++ b/tests/builtins/from_result.c
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT:  @EVA_CONFIG@ -eva-no-builtins-auto -deps -journal-disable
+   OPT:  @EVA_CONFIG@ -eva-alloc-builtin fresh -deps -journal-disable
 */
-#define malloc(n) Frama_C_malloc_fresh(n)
+
 #include "../../share/libc/stdlib.c"
 
 struct T { int a; int b; };
diff --git a/tests/builtins/gcc_zero_length_array.c b/tests/builtins/gcc_zero_length_array.c
index 49102dfcfc59a49c49990330bcf851c68f8ef0c0..b990a598b0e4f9c25888f70e5a482fa9dfc4757f 100644
--- a/tests/builtins/gcc_zero_length_array.c
+++ b/tests/builtins/gcc_zero_length_array.c
@@ -1,5 +1,5 @@
 /* run.config*
-  STDOPT: +"-machdep gcc_x86_32 -eva-builtin malloc:Frama_C_malloc_fresh -slevel 11"
+  STDOPT: +"-machdep gcc_x86_32 -eva-alloc-builtin fresh -slevel 11"
  */
 #include <stdlib.h>
 
diff --git a/tests/builtins/malloc-deps.c b/tests/builtins/malloc-deps.c
index a50b7e99b2fc4190bc771320a65cedfedc6bf7de..312e2534df54f1c9d390c49abe5465673dc598cb 100644
--- a/tests/builtins/malloc-deps.c
+++ b/tests/builtins/malloc-deps.c
@@ -1,31 +1,28 @@
 /* run.config*
    OPT: -eva @EVA_CONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
 */
-#include <stddef.h>
-//@ assigns \result \from \nothing;
-void *Frama_C_malloc_fresh(size_t n);
-//@ assigns \result \from \nothing;
-void *Frama_C_malloc_fresh_weak(size_t n);
-//@ assigns \result \from \nothing;
-void *Frama_C_malloc_by_stack(size_t n);
+#include <stdlib.h>
 
 volatile int v;
 void g(int *p, int k) { p[k] = k; }
 
 void main(int i, int j) {
   int *p, *q;
-  p = Frama_C_malloc_fresh_weak(100);
+  /*@ eva_allocate fresh_weak; */
+  p = malloc(100);
   *p = i;
   *p = j; // Cannnot perform strong update for deps, variable is weak
 
-  q = Frama_C_malloc_fresh(100);
+  /*@ eva_allocate fresh; */
+  q = malloc(100);
   *q = i;
   *q = j; // Can perform strong update for deps
 
 
   int *r;
   for (int l=0; l<10; l++) {
-    r = Frama_C_malloc_by_stack((l+1)*4);
+    /*@ eva_allocate by_stack; */
+    r = malloc((l+1)*4);
     g(r, l+v); // Again, we can only perform weak updates (after iteration 1)
   }
 }
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index af2dbc58d5b2eff3d0a49890a02bf98bbfc295c7..fb9377fa0041f543e133230dab5ca534fcc32b61 100644
--- a/tests/builtins/malloc.c
+++ b/tests/builtins/malloc.c
@@ -1,24 +1,23 @@
 /* run.config*
-   OPT: -eva @EVA_CONFIG@ -slevel 10 -eva-mlevel 0
+   OPT: -eva @EVA_CONFIG@ -slevel 10 -eva-mlevel 0 -eva-alloc-builtin by_stack
 */
-#include <stddef.h>
-void *Frama_C_malloc_by_stack(size_t i);
-void *Frama_C_malloc_fresh(size_t i);
-void *Frama_C_malloc_imprecise(size_t i);
+#include <stdlib.h>
+
 void main(int c) {
   int x;
   int *s;
   if(c) {
     x = 1;
-    s = Frama_C_malloc_by_stack(100);
+    s = malloc(100);
   } else {
     x = 2;
     s = 0;
   }
 
-  int *p = Frama_C_malloc_by_stack(c);
-  int *q = Frama_C_malloc_by_stack(12);
-  int *r = Frama_C_malloc_fresh(100);
+  int *p = malloc(c);
+  int *q = malloc(12);
+  /*@ eva_allocate fresh; */
+  int *r = malloc(100);
   *p = 1;
   *(p+2) = 3;
   *(p+24999) = 4;
@@ -30,9 +29,11 @@ void main(int c) {
   *r = 1;
   *(r+2) = 3;
 
-  int *mw = Frama_C_malloc_imprecise(42);
+  /*@ eva_allocate imprecise; */
+  int *mw = malloc(42);
   *mw = 1;
-  int *mw2 = Frama_C_malloc_imprecise(42);
+  /*@ eva_allocate imprecise; */
+  int *mw2 = malloc(42);
   *mw2 = 2;
 
   //  *s = 1;
diff --git a/tests/builtins/malloc_individual.c b/tests/builtins/malloc_individual.c
index e85945c2ca8273433b7e09ae1e96223a4f761067..790ffba5e5b8e51afd50bc2b27c2eff238af28bc 100644
--- a/tests/builtins/malloc_individual.c
+++ b/tests/builtins/malloc_individual.c
@@ -1,7 +1,7 @@
 /* run.config*
-   STDOPT: #"-eva-no-builtins-auto"
+   STDOPT: #"-eva-alloc-builtin fresh"
 */
-#define malloc(n) Frama_C_malloc_fresh(n)
+
 #include "share/libc/stdlib.c"
 
 int *p;
diff --git a/tests/builtins/malloc_memexec.c b/tests/builtins/malloc_memexec.c
index 2a0434c008580b6802e46d28c4f5627791898dc9..cac60b4be3121fe0fe79ea701fee95860d0420a3 100644
--- a/tests/builtins/malloc_memexec.c
+++ b/tests/builtins/malloc_memexec.c
@@ -1,13 +1,7 @@
 /* run.config*
    OPT: -eva @EVA_CONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
 */
-#include <stddef.h>
-//@ assigns \result;
-void *Frama_C_malloc_fresh(size_t n);
-
-//@ assigns \result;
-void *Frama_C_malloc_fresh_weak(size_t n);
-
+#include <stdlib.h>
 
 void f(int *p, int i) {
   *p = i;
@@ -16,7 +10,8 @@ void f(int *p, int i) {
 volatile v;
 
 void main() {
-  int *p = Frama_C_malloc_fresh (4);
+  /*@ eva_allocate fresh; */
+  int *p = malloc (4);
   if (v) {
     f(p, 2);
     f(p, 1); // This call or the corresponding one below could be cached. It is not, because we forbid memexec to take full updates to a strong variable into account for malloced bases, because they may become weak later
@@ -24,7 +19,8 @@ void main() {
     f(p, 1);
   }
 
-  int *q = Frama_C_malloc_fresh_weak (4);
+  /*@ eva_allocate fresh_weak; */
+  int *q = malloc (4);
   if (v) {
     f(q, 2);
     f(q, 1);
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/realloc2.res.oracle b/tests/builtins/oracle/realloc2.res.oracle
index 3e64362a4143ed84c51a86a34065c718ec9dddd2..ceb190b0e2be70b31386c7eaec10029e068cd7d3 100644
--- a/tests/builtins/oracle/realloc2.res.oracle
+++ b/tests/builtins/oracle/realloc2.res.oracle
@@ -6,8 +6,7 @@
   nondet ∈ [--..--]
 [eva] computing for function test_exact_null <- main.
   Called from tests/builtins/realloc2.c:194.
-[eva] tests/builtins/realloc2.c:27: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:27: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:27: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {}
@@ -22,8 +21,7 @@
 [eva] Done for function test_exact_null
 [eva] computing for function test_exact_null_free <- main.
   Called from tests/builtins/realloc2.c:195.
-[eva] tests/builtins/realloc2.c:32: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:32: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:32: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {}
@@ -41,8 +39,7 @@
   Called from tests/builtins/realloc2.c:37.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:38: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:38: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:38: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_exact_nonnull_expand_l36}
@@ -65,8 +62,7 @@
   Called from tests/builtins/realloc2.c:45.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:46: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:46: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:46: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_exact_nonnull_shrink_l44}
@@ -89,8 +85,7 @@
   Called from tests/builtins/realloc2.c:52.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:53: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:53: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:53: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_exact_nonnull_free_l51}
@@ -105,8 +100,7 @@
 [eva] tests/builtins/realloc2.c:57: Call to builtin malloc
 [eva] tests/builtins/realloc2.c:57: 
   allocating variable __malloc_test_maybe_nonnull_l57
-[eva] tests/builtins/realloc2.c:58: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:58: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:58: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_maybe_nonnull_l57}
@@ -129,8 +123,7 @@
   Called from tests/builtins/realloc2.c:64.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:65: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:65: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:65: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_same_size_l63}
@@ -142,8 +135,7 @@
 [eva] Done for function test_same_size
 [eva] computing for function test_imprecise_size <- main.
   Called from tests/builtins/realloc2.c:201.
-[eva] tests/builtins/realloc2.c:70: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:70: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:70: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {}
@@ -160,8 +152,7 @@
 [eva] Done for function test_imprecise_size
 [eva] computing for function test_imprecise_size_but_precise_fill <- main.
   Called from tests/builtins/realloc2.c:202.
-[eva] tests/builtins/realloc2.c:76: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:76: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:76: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {}
@@ -183,8 +174,7 @@
   Called from tests/builtins/realloc2.c:82.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:84: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:84: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:84: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_imprecise_size_free_l81}
@@ -203,8 +193,7 @@
 [eva] tests/builtins/realloc2.c:89: Call to builtin malloc
 [eva] tests/builtins/realloc2.c:89: 
   allocating variable __malloc_test_imprecise_both_l89
-[eva] tests/builtins/realloc2.c:91: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:91: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:91: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_imprecise_both_l89}
@@ -223,8 +212,7 @@
 [eva] tests/builtins/realloc2.c:96: Call to builtin malloc
 [eva] tests/builtins/realloc2.c:96: 
   allocating variable __malloc_test_possibly_invalid_realloc_l96
-[eva] tests/builtins/realloc2.c:99: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:99: Call to builtin realloc
 [eva:alarm] tests/builtins/realloc2.c:99: Warning: 
   function realloc: precondition 'freeable' got status unknown.
 [eva:malloc] bases_to_realloc: {__malloc_test_possibly_invalid_realloc_l96}
@@ -243,16 +231,14 @@
 [eva] tests/builtins/realloc2.c:104: Call to builtin malloc
 [eva] tests/builtins/realloc2.c:104: 
   allocating variable __malloc_test_invalid_realloc_l104
-[eva] tests/builtins/realloc2.c:106: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:106: Call to builtin realloc
 [eva:alarm] tests/builtins/realloc2.c:106: Warning: 
   function realloc: precondition 'freeable' got status invalid.
 [eva] Recording results for test_invalid_realloc
 [eva] Done for function test_invalid_realloc
 [eva] computing for function test_invalid_realloc2 <- main.
   Called from tests/builtins/realloc2.c:207.
-[eva] tests/builtins/realloc2.c:111: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:111: Call to builtin realloc
 [eva:alarm] tests/builtins/realloc2.c:111: Warning: 
   function realloc: precondition 'freeable' got status invalid.
 [eva] Recording results for test_invalid_realloc2
@@ -262,8 +248,7 @@
 [eva] tests/builtins/realloc2.c:116: Call to builtin malloc
 [eva] tests/builtins/realloc2.c:116: 
   allocating variable __malloc_test_invalid_realloc3_l116
-[eva] tests/builtins/realloc2.c:119: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:119: Call to builtin realloc
 [eva:alarm] tests/builtins/realloc2.c:119: Warning: 
   function realloc: precondition 'freeable' got status invalid.
 [eva] Recording results for test_invalid_realloc3
@@ -273,8 +258,7 @@
 [eva] tests/builtins/realloc2.c:124: Call to builtin malloc
 [eva] tests/builtins/realloc2.c:124: 
   allocating variable __malloc_test_realloc_sequence_l124
-[eva] tests/builtins/realloc2.c:125: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:125: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:125: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_realloc_sequence_l124}
@@ -282,8 +266,7 @@
   allocating variable __realloc_test_realloc_sequence_l125
 [eva:malloc] tests/builtins/realloc2.c:125: 
   strong free on bases: {__malloc_test_realloc_sequence_l124}
-[eva] tests/builtins/realloc2.c:126: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:126: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:126: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__realloc_test_realloc_sequence_l125}
@@ -306,8 +289,7 @@
   Called from tests/builtins/realloc2.c:134.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:138: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:138: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:138: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_realloc_loop_l131}
@@ -319,8 +301,7 @@
   Called from tests/builtins/realloc2.c:142.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:138: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:138: Call to builtin realloc
 [eva:malloc] bases_to_realloc: {__realloc_test_realloc_loop_l138}
 [eva:malloc:weak] tests/builtins/realloc2.c:138: 
   marking variable `__realloc_test_realloc_loop_l138' as weak
@@ -332,8 +313,7 @@
   Called from tests/builtins/realloc2.c:142.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:138: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:138: Call to builtin realloc
 [eva:malloc] bases_to_realloc: {__realloc_w_test_realloc_loop_l138}
 [eva:malloc] tests/builtins/realloc2.c:138: 
   resizing variable `__realloc_w_test_realloc_loop_l138'
@@ -344,8 +324,7 @@
   Called from tests/builtins/realloc2.c:142.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:138: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:138: Call to builtin realloc
 [eva:malloc] bases_to_realloc: {__realloc_w_test_realloc_loop_l138}
 [eva:malloc] tests/builtins/realloc2.c:138: 
   resizing variable `__realloc_w_test_realloc_loop_l138'
@@ -356,8 +335,7 @@
   Called from tests/builtins/realloc2.c:142.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:138: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:138: Call to builtin realloc
 [eva:malloc] bases_to_realloc: {__realloc_w_test_realloc_loop_l138}
 [eva:malloc] tests/builtins/realloc2.c:138: 
   resizing variable `__realloc_w_test_realloc_loop_l138'
@@ -378,8 +356,7 @@
 [eva] tests/builtins/realloc2.c:154: Call to builtin malloc
 [eva] tests/builtins/realloc2.c:154: 
   allocating variable __malloc_test_realloc_multiple_bases_l154
-[eva] tests/builtins/realloc2.c:156: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:156: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:156: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_realloc_multiple_bases_l151}
@@ -387,8 +364,7 @@
   allocating variable __realloc_test_realloc_multiple_bases_l156
 [eva:malloc] tests/builtins/realloc2.c:156: 
   strong free on bases: {__malloc_test_realloc_multiple_bases_l151}
-[eva] tests/builtins/realloc2.c:158: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:158: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:158: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] 
@@ -414,8 +390,7 @@
   Called from tests/builtins/realloc2.c:165.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:166: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:166: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:166: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_realloc_multiple_bases2_l163}
@@ -430,8 +405,7 @@
   Called from tests/builtins/realloc2.c:168.
 [eva] Recording results for fill2
 [eva] Done for function fill2
-[eva] tests/builtins/realloc2.c:169: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:169: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:169: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] 
@@ -442,8 +416,7 @@
 [eva:malloc] tests/builtins/realloc2.c:169: 
   weak free on bases: {__realloc_test_realloc_multiple_bases2_l166,
                        __malloc_test_realloc_multiple_bases2_l166}
-[eva] tests/builtins/realloc2.c:171: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:171: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:171: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__realloc_test_realloc_multiple_bases2_l169}
@@ -462,8 +435,7 @@
   Called from tests/builtins/realloc2.c:176.
 [eva] Recording results for fill2
 [eva] Done for function fill2
-[eva] tests/builtins/realloc2.c:177: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:177: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:177: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] 
@@ -485,8 +457,7 @@
 [eva] tests/builtins/realloc2.c:184: Call to builtin malloc
 [eva] tests/builtins/realloc2.c:184: 
   allocating variable __malloc_test_realloc_multiple_bases_loop_l184
-[eva] tests/builtins/realloc2.c:187: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:187: Call to builtin realloc
 [eva] tests/builtins/realloc2.c:187: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_test_realloc_multiple_bases_loop_l184}
@@ -499,8 +470,7 @@
 [eva] Recording results for fill
 [eva] Done for function fill
 [eva] tests/builtins/realloc2.c:185: starting to merge loop iterations
-[eva] tests/builtins/realloc2.c:187: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:187: Call to builtin realloc
 [eva:malloc] 
   bases_to_realloc: {__malloc_test_realloc_multiple_bases_loop_l184,
                      __realloc_test_realloc_multiple_bases_loop_l187}
@@ -516,8 +486,7 @@
   Called from tests/builtins/realloc2.c:189.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:187: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:187: Call to builtin realloc
 [eva:malloc] 
   bases_to_realloc: {__malloc_test_realloc_multiple_bases_loop_l184,
                      __realloc_w_test_realloc_multiple_bases_loop_l187}
@@ -531,8 +500,7 @@
   Called from tests/builtins/realloc2.c:189.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:187: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:187: Call to builtin realloc
 [eva:malloc] 
   bases_to_realloc: {__malloc_test_realloc_multiple_bases_loop_l184,
                      __realloc_w_test_realloc_multiple_bases_loop_l187}
@@ -546,8 +514,7 @@
   Called from tests/builtins/realloc2.c:189.
 [eva] Recording results for fill
 [eva] Done for function fill
-[eva] tests/builtins/realloc2.c:187: 
-  Call to builtin Frama_C_realloc for function realloc
+[eva] tests/builtins/realloc2.c:187: Call to builtin realloc
 [eva:malloc] 
   bases_to_realloc: {__malloc_test_realloc_multiple_bases_loop_l184,
                      __realloc_w_test_realloc_multiple_bases_loop_l187}
diff --git a/tests/builtins/oracle/realloc_imprecise.res.oracle b/tests/builtins/oracle/realloc_imprecise.res.oracle
index 346a55355c0f64cf362f127e98845f8691bee8b6..4440159774e9ec80b1a03cdd6dabc2e404cd86b8 100644
--- a/tests/builtins/oracle/realloc_imprecise.res.oracle
+++ b/tests/builtins/oracle/realloc_imprecise.res.oracle
@@ -4,20 +4,17 @@
 [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: 
   out of bounds write. assert \valid(p);
-[eva] tests/builtins/realloc_imprecise.c:13: 
-  Call to builtin Frama_C_realloc_imprecise for function realloc
+[eva] tests/builtins/realloc_imprecise.c:13: Call to builtin realloc
 [eva] tests/builtins/realloc_imprecise.c:13: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/realloc_imprecise.c:13: 
   weak free on bases: {__alloc_w_main}
-[eva] tests/builtins/realloc_imprecise.c:15: 
-  Call to builtin Frama_C_realloc_imprecise for function realloc
+[eva] tests/builtins/realloc_imprecise.c:15: Call to builtin realloc
 [eva] tests/builtins/realloc_imprecise.c:15: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] tests/builtins/realloc_imprecise.c:15: 
diff --git a/tests/builtins/oracle/realloc_multiple.0.res.oracle b/tests/builtins/oracle/realloc_multiple.0.res.oracle
index 9e00330021274a3cba7e16899bce6fa1d0937cc8..d90f95f45a564ffc1091d7da875c0f92bfdbc6d1 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.
@@ -45,8 +43,7 @@
   __malloc_main1_l9[0..4] ∈ {5}
   __malloc_main1_l12[0..5] ∈ {6}
   ==END OF DUMP==
-[eva] tests/builtins/realloc_multiple.c:23: 
-  Call to builtin Frama_C_realloc_multiple for function realloc
+[eva] tests/builtins/realloc_multiple.c:23: Call to builtin realloc
 [eva] tests/builtins/realloc_multiple.c:23: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_main1_l12}
@@ -97,12 +94,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.
@@ -136,8 +131,7 @@
   __malloc_main2_l30[0..4] ∈ {7}
   __malloc_main2_l33[0..5] ∈ {8}
   ==END OF DUMP==
-[eva] tests/builtins/realloc_multiple.c:45: 
-  Call to builtin Frama_C_realloc_multiple for function realloc
+[eva] tests/builtins/realloc_multiple.c:45: Call to builtin realloc
 [eva] tests/builtins/realloc_multiple.c:45: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_main2_l33}
@@ -196,12 +190,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.
@@ -238,8 +230,7 @@
   __malloc_main3_l52 ∈ {{ &x }}
   __malloc_main3_l53 ∈ {{ &y }}
   ==END OF DUMP==
-[eva] tests/builtins/realloc_multiple.c:65: 
-  Call to builtin Frama_C_realloc_multiple for function realloc
+[eva] tests/builtins/realloc_multiple.c:65: Call to builtin realloc
 [eva] tests/builtins/realloc_multiple.c:65: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_main3_l53}
diff --git a/tests/builtins/oracle/realloc_multiple.1.res.oracle b/tests/builtins/oracle/realloc_multiple.1.res.oracle
index facf3d7f3a3a3e0b1b85fec505165e2a5f702320..f8c4c7bdce1caeb4fc45e8dbddacc3f13caf6f76 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: 
@@ -53,8 +51,7 @@
   __malloc_main1_l9[0..4] ∈ {5}
   __malloc_main1_l12[0..5] ∈ {6}
   ==END OF DUMP==
-[eva] tests/builtins/realloc_multiple.c:23: 
-  Call to builtin Frama_C_realloc_multiple for function realloc
+[eva] tests/builtins/realloc_multiple.c:23: Call to builtin realloc
 [eva] tests/builtins/realloc_multiple.c:23: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_main1_l12}
@@ -134,16 +131,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: 
@@ -181,8 +176,7 @@
   __malloc_main2_l30[0..4] ∈ {7}
   __malloc_main2_l33[0..5] ∈ {8}
   ==END OF DUMP==
-[eva] tests/builtins/realloc_multiple.c:45: 
-  Call to builtin Frama_C_realloc_multiple for function realloc
+[eva] tests/builtins/realloc_multiple.c:45: Call to builtin realloc
 [eva] tests/builtins/realloc_multiple.c:45: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_main2_l33}
@@ -270,16 +264,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: 
@@ -324,8 +315,7 @@
   __malloc_main3_l52 ∈ {{ &x }}
   __malloc_main3_l53 ∈ {{ &y }}
   ==END OF DUMP==
-[eva] tests/builtins/realloc_multiple.c:65: 
-  Call to builtin Frama_C_realloc_multiple for function realloc
+[eva] tests/builtins/realloc_multiple.c:65: Call to builtin realloc
 [eva] tests/builtins/realloc_multiple.c:65: 
   function realloc: precondition 'freeable' got status valid.
 [eva:malloc] bases_to_realloc: {__malloc_main3_l53}
diff --git a/tests/builtins/realloc.c b/tests/builtins/realloc.c
index 08db98c71601626d53a0f0f78f31fe799cbff246..77b69e12e8cb4c541f63607aa0e74f438c74bb10 100644
--- a/tests/builtins/realloc.c
+++ b/tests/builtins/realloc.c
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: +"-slevel 10 -eva-builtin malloc:Frama_C_malloc_fresh -eva-warn-copy-indeterminate @all"
+   STDOPT: +"-slevel 10 -eva-alloc-builtin by_stack -eva-warn-copy-indeterminate @all"
 */
 
 #include <stdlib.h>
diff --git a/tests/builtins/realloc2.c b/tests/builtins/realloc2.c
index 21e2de33052fd23a1de6a6f210bfb654a2e81abf..6614f80f06f487e9e7e554c4f8bbb3651c1ccb46 100644
--- a/tests/builtins/realloc2.c
+++ b/tests/builtins/realloc2.c
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: #"-eva-builtin realloc:Frama_C_realloc -eva-mlevel 0 -inout-callwise -inout-no-print "
+   STDOPT: #"-eva-mlevel 0 -inout-callwise -inout-no-print "
 */
 #include <stdlib.h>
 
diff --git a/tests/builtins/realloc_imprecise.c b/tests/builtins/realloc_imprecise.c
index bd9e002b64b2fc82554c3578f90877ee93a1fa45..f8d72562a67ed163730ea605d257e64a501f7f79 100644
--- a/tests/builtins/realloc_imprecise.c
+++ b/tests/builtins/realloc_imprecise.c
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: +"-eva-builtin malloc:Frama_C_malloc_imprecise,realloc:Frama_C_realloc_imprecise"
+   STDOPT: +"-eva-alloc-builtin imprecise"
 */
 
 #include <stdlib.h>
diff --git a/tests/builtins/realloc_multiple.c b/tests/builtins/realloc_multiple.c
index 8657eb4bd84b3077a25b7dd0b088be5c485624e6..1e5825544465ea4e4bc1ffee2f459fdbb5a5ef05 100644
--- a/tests/builtins/realloc_multiple.c
+++ b/tests/builtins/realloc_multiple.c
@@ -1,6 +1,6 @@
 /* run.config*
-   STDOPT: +"-slevel 10 -eva-builtin malloc:Frama_C_malloc_fresh,realloc:Frama_C_realloc_multiple -eva-malloc-functions malloc,realloc"
-   STDOPT: +"-slevel 10 -eva-builtin malloc:Frama_C_malloc_fresh,realloc:Frama_C_realloc_multiple -eva-malloc-functions malloc,realloc -eva-alloc-returns-null"
+   STDOPT: +"-slevel 10 -eva-alloc-builtin fresh -eva-malloc-functions malloc,realloc"
+   STDOPT: +"-slevel 10 -eva-alloc-builtin fresh -eva-malloc-functions malloc,realloc -eva-alloc-returns-null"
 */
 #include <stdlib.h>
 #include "__fc_builtin.h"
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
diff --git a/tests/libc/stdlib_c.c b/tests/libc/stdlib_c.c
index d265774bec565ed9ea9b83b45ff1620f44465221..f021a7551c10da4cd12bf630fa7df7a4b009086e 100644
--- a/tests/libc/stdlib_c.c
+++ b/tests/libc/stdlib_c.c
@@ -1,10 +1,10 @@
 /* run.config
-   STDOPT: #"-eva-no-builtins-auto -slevel 10 -eva-builtin calloc:Frama_C_calloc_by_stack -eva-msg-key malloc"
-   STDOPT: #"-eva-no-builtins-auto -slevel 10 -eva-builtin calloc:Frama_C_calloc_by_stack -eva-no-alloc-returns-null -eva-msg-key malloc"
+   STDOPT: #"-eva-no-builtins-auto -slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-msg-key malloc"
+   STDOPT: #"-eva-no-builtins-auto -slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-no-alloc-returns-null -eva-msg-key malloc"
    STDOPT: #"-eva-no-builtins-auto"
 */ // slevel is used to unroll loops
 
-#define malloc(n) Frama_C_malloc_by_stack(n)
+#define malloc(n) Frama_C_malloc(n)
 #include "stdlib.c"
 #include "__fc_builtin.h"
 #include <stdint.h>