From e5b0fdbb96936f5e0265257e4dcc3a30651c5e1c Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 26 Sep 2024 09:56:05 +0200
Subject: [PATCH] [Eva] add some dkeys for malloc-related functions
---
.../eva/domains/cvalue/builtins_malloc.ml | 12 +-
.../tests/md/oracle/cwe126.res.oracle | 4 +-
.../oracle/multiple-va_start.res.oracle | 2 +-
.../tests/defined/oracle/va_copy.res.oracle | 2 +-
tests/builtins/oracle/alloc-vla.res.oracle | 2 +-
tests/builtins/oracle/alloc.0.res.oracle | 10 +-
tests/builtins/oracle/alloc.1.res.oracle | 2 +-
tests/builtins/oracle/alloc_weak.res.oracle | 12 +-
tests/builtins/oracle/allocated.0.res.oracle | 22 ++--
tests/builtins/oracle/allocated.1.res.oracle | 116 +++++++++---------
tests/builtins/oracle/calloc.1.res.oracle | 10 +-
tests/builtins/oracle/calloc.2.res.oracle | 10 +-
tests/builtins/oracle/calloc.3.res.oracle | 10 +-
tests/builtins/oracle/calloc.4.res.oracle | 10 +-
tests/builtins/oracle/free.res.oracle | 10 +-
tests/builtins/oracle/from_result.res.oracle | 4 +-
.../oracle/gcc_zero_length_array.res.oracle | 3 +-
.../oracle/imprecise-malloc-free.res.oracle | 9 +-
tests/builtins/oracle/malloc-deps.res.oracle | 6 +-
.../oracle/malloc-optimistic.res.oracle | 22 ++--
.../oracle/malloc-size-zero.0.res.oracle | 15 ++-
.../oracle/malloc-size-zero.1.res.oracle | 4 +-
tests/builtins/oracle/malloc.res.oracle | 10 +-
.../builtins/oracle/malloc_bug_tr.res.oracle | 2 +-
.../oracle/malloc_individual.res.oracle | 2 +-
.../builtins/oracle/malloc_memexec.res.oracle | 5 +-
.../oracle/malloc_multiple.res.oracle | 54 +++++---
.../builtins/oracle/memexec-malloc.res.oracle | 8 +-
tests/builtins/oracle/memset.res.oracle | 3 +-
.../oracle/memset_malloc_0.res.oracle | 2 +-
tests/builtins/oracle/realloc.res.oracle | 50 ++++----
tests/builtins/oracle/realloc2.res.oracle | 102 +++++++++------
.../oracle/realloc_multiple.0.res.oracle | 33 ++---
.../oracle/realloc_multiple.1.res.oracle | 35 +++---
.../builtins/oracle/str_allocated.res.oracle | 2 +-
tests/builtins/oracle/vla.res.oracle | 4 +-
tests/libc/oracle/alloca_h.res.oracle | 23 ++--
tests/libc/oracle/argz_c.res.oracle | 42 ++++---
tests/libc/oracle/glob_c.res.oracle | 18 ++-
tests/libc/oracle/netdb_c.res.oracle | 9 +-
tests/libc/oracle/search_h.res.oracle | 2 +-
tests/libc/oracle/stdio_c.res.oracle | 12 +-
tests/libc/oracle/stdlib_c.0.res.oracle | 17 +--
tests/libc/oracle/stdlib_c.1.res.oracle | 17 +--
tests/libc/oracle/stdlib_c.2.res.oracle | 20 +--
tests/libc/oracle/wchar_c_h.0.res.oracle | 6 +-
tests/misc/oracle/array_sizeof.res.oracle | 2 +-
tests/rte_manual/oracle/sizeof.res.oracle | 5 +-
.../value/oracle/abstract_struct_1.res.oracle | 2 +-
tests/value/oracle/empty_struct.5.res.oracle | 4 +-
tests/value/oracle/gauges.res.oracle | 2 +-
51 files changed, 444 insertions(+), 346 deletions(-)
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index 1ee6b82715c..9c38fcc3a97 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -29,6 +29,14 @@ open Lattice_bounds
let dkey = Self.register_category "malloc"
~help:"messages from the builtins interpreting dynamic allocations"
+let dkey_new = Self.register_category "malloc:new"
+ ~help:"messages emitted at the creation of new bases"
+let () = Self.add_debug_keys dkey_new
+
+let dkey_auto_free = Self.register_category "malloc:automatic-free"
+ ~help:"messages emitted when bases are automatically freed (alloca or VLA)"
+let () = Self.add_debug_keys dkey_auto_free
+
let wkey_weak_alloc = Self.register_warn_category "malloc:weak"
let () = Self.set_warn_status wkey_weak_alloc Log.Winactive
@@ -322,7 +330,7 @@ let alloc_fresh weak deallocation prefix sizev _state =
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
- Self.result ~current:true ~once:true
+ Self.result ~dkey:dkey_new ~current:true ~once:true
"@[allocating %svariable %a@]%t"
(if weak = Weak then "weak " else "") Printer.pp_varinfo var
Eva_utils.pp_callstack;
@@ -688,7 +696,7 @@ let free_automatic_bases stack state =
in
if Base.Hptset.is_empty bases_to_free then state
else begin
- Self.result ~current:true ~once:true
+ Self.result ~dkey:dkey_auto_free ~current:true ~once:true
"freeing automatic bases: %a" Base.Hptset.pretty bases_to_free;
let state', _changed = free_aux state ~strong:true bases_to_free in
(* TODO: propagate 'freed' bases for From? *)
diff --git a/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
index f8fc6e591f5..aa34eaebd50 100644
--- a/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
+++ b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle
@@ -2,12 +2,12 @@
[eva] Analyzing a complete application starting at main
[eva:initial-state] Values of globals at initialization
-[eva] cwe126.c:77: allocating variable __malloc_goodG2B_l77
+[eva:malloc:new] cwe126.c:77: allocating variable __malloc_goodG2B_l77
[eva] using specification for function exit
[eva] FRAMAC_SHARE/libc/string.h:167:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva] cwe126.c:63: starting to merge loop iterations
-[eva] cwe126.c:41:
+[eva:malloc:new] cwe126.c:41:
allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l41
[eva] cwe126.c:27: starting to merge loop iterations
[eva:alarm] cwe126.c:29: Warning:
diff --git a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
index 25efd1adf49..6180fce0e33 100644
--- a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
@@ -2,7 +2,7 @@
[variadic] multiple-va_start.c:32:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[eva] multiple-va_start.c:20: allocating variable __malloc_pack_l20
+[eva:malloc:new] multiple-va_start.c:20: allocating variable __malloc_pack_l20
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function pack:
__fc_heap_status ∈ [--..--]
diff --git a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
index 2092b713a57..4e0baaa971f 100644
--- a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
@@ -1,7 +1,7 @@
[variadic] va_copy.c:9: Declaration of variadic function pack.
[variadic] va_copy.c:32: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[eva] va_copy.c:21: allocating variable __malloc_pack_l21
+[eva:malloc:new] va_copy.c:21: allocating variable __malloc_pack_l21
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function pack:
__fc_heap_status ∈ [--..--]
diff --git a/tests/builtins/oracle/alloc-vla.res.oracle b/tests/builtins/oracle/alloc-vla.res.oracle
index 36507d1fe07..9ca582251ec 100644
--- a/tests/builtins/oracle/alloc-vla.res.oracle
+++ b/tests/builtins/oracle/alloc-vla.res.oracle
@@ -8,7 +8,7 @@
Called from alloc-vla.c:12.
[eva] alloc-vla.c:6: assertion 'alloca_bounds' got status valid.
[eva] alloc-vla.c:6: Call to builtin __fc_vla_alloc
-[eva] alloc-vla.c:6: allocating variable __malloc_f_l6
+[eva:malloc:new] alloc-vla.c:6: allocating variable __malloc_f_l6
[eva] alloc-vla.c:7: Call to builtin free
[eva:alarm] alloc-vla.c:7: Warning:
function free: precondition 'freeable' got status invalid.
diff --git a/tests/builtins/oracle/alloc.0.res.oracle b/tests/builtins/oracle/alloc.0.res.oracle
index 54ebc937040..822782fce6b 100644
--- a/tests/builtins/oracle/alloc.0.res.oracle
+++ b/tests/builtins/oracle/alloc.0.res.oracle
@@ -13,9 +13,9 @@
v ∈ {0}
ch ∈ {44}
[eva] alloc.c:16: Call to builtin malloc
-[eva] alloc.c:16: allocating variable __malloc_main_l16
+[eva:malloc:new] alloc.c:16: allocating variable __malloc_main_l16
[eva] alloc.c:17: Call to builtin malloc
-[eva] alloc.c:17: allocating variable __malloc_main_l17
+[eva:malloc:new] alloc.c:17: allocating variable __malloc_main_l17
[eva:alarm] alloc.c:18: Warning:
out of bounds write. assert \valid(p + (int)(-1));
[kernel] alloc.c:18: Warning:
@@ -31,7 +31,7 @@
[kernel] alloc.c:21: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] alloc.c:25: Call to builtin malloc
-[eva] alloc.c:25: allocating variable __malloc_main_l25
+[eva:malloc:new] alloc.c:25: allocating variable __malloc_main_l25
[eva:alarm] alloc.c:26: Warning:
pointer downcast. assert (unsigned int)q ≤ 2147483647;
[eva:alarm] alloc.c:26: Warning:
@@ -43,9 +43,9 @@
[eva:alarm] alloc.c:27: Warning: out of bounds write. assert \valid(r);
[eva:alarm] alloc.c:27: Warning: out of bounds read. assert \valid_read(r + 1);
[eva] alloc.c:32: Call to builtin malloc
-[eva] alloc.c:32: allocating variable __malloc_main_l32
+[eva:malloc:new] alloc.c:32: allocating variable __malloc_main_l32
[eva] alloc.c:33: Call to builtin malloc
-[eva] alloc.c:33: allocating variable __malloc_main_l33
+[eva:malloc:new] alloc.c:33: allocating variable __malloc_main_l33
[eva:alarm] alloc.c:34: Warning: out of bounds write. assert \valid(u);
[eva:alarm] alloc.c:35: Warning: out of bounds write. assert \valid(u);
[eva:alarm] alloc.c:36: Warning: out of bounds write. assert \valid(u + 1);
diff --git a/tests/builtins/oracle/alloc.1.res.oracle b/tests/builtins/oracle/alloc.1.res.oracle
index 9d78cea78ca..4d22c5ce69c 100644
--- a/tests/builtins/oracle/alloc.1.res.oracle
+++ b/tests/builtins/oracle/alloc.1.res.oracle
@@ -14,7 +14,7 @@
v ∈ {0}
ch ∈ {44}
[eva] alloc.c:50: Call to builtin malloc
-[eva] alloc.c:50: allocating variable __malloc_main_abs_l50
+[eva:malloc:new] alloc.c:50: allocating variable __malloc_main_abs_l50
[eva:alarm] alloc.c:51: Warning:
pointer downcast. assert (unsigned int)q ≤ 2147483647;
[eva:alarm] alloc.c:51: Warning:
diff --git a/tests/builtins/oracle/alloc_weak.res.oracle b/tests/builtins/oracle/alloc_weak.res.oracle
index f13229d6c23..fe9898c64f9 100644
--- a/tests/builtins/oracle/alloc_weak.res.oracle
+++ b/tests/builtins/oracle/alloc_weak.res.oracle
@@ -9,7 +9,7 @@
[eva] computing for function main1 <- main.
Called from alloc_weak.c:93.
[eva] alloc_weak.c:23: Call to builtin malloc
-[eva] alloc_weak.c:23: allocating variable __malloc_main1_l23
+[eva:malloc:new] alloc_weak.c:23: allocating variable __malloc_main1_l23
[eva] alloc_weak.c:23: Call to builtin malloc
[eva:malloc:weak] alloc_weak.c:23: marking variable `__malloc_main1_l23' as weak
[eva] computing for function copy <- main1 <- main.
@@ -38,7 +38,7 @@
[eva] computing for function main2 <- main.
Called from alloc_weak.c:94.
[eva] alloc_weak.c:37: Call to builtin malloc
-[eva] alloc_weak.c:37: allocating variable __malloc_main2_l37
+[eva:malloc:new] alloc_weak.c:37: allocating variable __malloc_main2_l37
[eva:alarm] alloc_weak.c:37: Warning:
pointer downcast.
assert (unsigned int)tmp ≤ 2147483647;
@@ -56,7 +56,7 @@
[eva] computing for function main3 <- main.
Called from alloc_weak.c:95.
[eva] alloc_weak.c:51: Call to builtin malloc
-[eva] alloc_weak.c:51: allocating variable __malloc_main3_l51
+[eva:malloc:new] alloc_weak.c:51: allocating variable __malloc_main3_l51
[eva] alloc_weak.c:50: starting to merge loop iterations
[eva] alloc_weak.c:51: Call to builtin malloc
[eva:malloc:weak] alloc_weak.c:51: marking variable `__malloc_main3_l51' as weak
@@ -75,9 +75,11 @@
[eva] computing for function convergence_issue <- main.
Called from alloc_weak.c:96.
[eva] alloc_weak.c:73: Call to builtin calloc
-[eva] alloc_weak.c:73: allocating variable __calloc_convergence_issue_l73
+[eva:malloc:new] alloc_weak.c:73:
+ allocating variable __calloc_convergence_issue_l73
[eva] alloc_weak.c:82: Call to builtin calloc
-[eva] alloc_weak.c:82: allocating variable __calloc_convergence_issue_l82
+[eva:malloc:new] alloc_weak.c:82:
+ allocating variable __calloc_convergence_issue_l82
[eva] alloc_weak.c:74: starting to merge loop iterations
[eva:alarm] alloc_weak.c:80: Warning:
out of bounds read. assert \valid_read((p + size) - 1);
diff --git a/tests/builtins/oracle/allocated.0.res.oracle b/tests/builtins/oracle/allocated.0.res.oracle
index f3305d57c0a..789283dae7a 100644
--- a/tests/builtins/oracle/allocated.0.res.oracle
+++ b/tests/builtins/oracle/allocated.0.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] allocated.c:25: Call to builtin malloc
-[eva] allocated.c:25: allocating variable __malloc_main_l25
+[eva:malloc:new] allocated.c:25: allocating variable __malloc_main_l25
[eva] allocated.c:25: assertion got status valid.
[eva:alarm] allocated.c:27: Warning:
out of bounds read. assert \valid_read(p + 1);
@@ -18,7 +18,7 @@
[eva:malloc] allocated.c:31: strong free on bases: {__malloc_main_l25}
[eva] allocated.c:32: Frama_C_show_each_p_after_free: ⊥
[eva] allocated.c:36: Call to builtin malloc
-[eva] allocated.c:36: allocating variable __malloc_main_l36
+[eva:malloc:new] allocated.c:36: allocating variable __malloc_main_l36
[eva] allocated.c:36: assertion got status valid.
[eva] allocated.c:40: Frama_C_show_each_p: {{ &__malloc_main_l36 }}
[eva] allocated.c:41: Frama_C_show_each_p0: {13}
@@ -38,7 +38,7 @@
[kernel] allocated.c:46: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] allocated.c:50: Call to builtin malloc
-[eva] allocated.c:50: allocating variable __malloc_main_l50
+[eva:malloc:new] allocated.c:50: allocating variable __malloc_main_l50
[eva] allocated.c:50: assertion got status valid.
[eva:alarm] allocated.c:53: Warning: out of bounds write. assert \valid(p + 2);
[eva] allocated.c:54: Frama_C_show_each_p: {{ &__malloc_main_l50 }}
@@ -49,7 +49,7 @@
[eva] allocated.c:58: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:58: strong free on bases: {__malloc_main_l50}
[eva] allocated.c:63: Call to builtin malloc
-[eva] allocated.c:63: allocating variable __malloc_main_l63
+[eva:malloc:new] allocated.c:63: allocating variable __malloc_main_l63
[eva] allocated.c:63: assertion got status valid.
[eva] allocated.c:65: Frama_C_show_each_p: {{ &__malloc_main_l63 }}
[eva] allocated.c:66: Frama_C_show_each_p0: {0}
@@ -72,7 +72,7 @@
[eva] allocated.c:67: Call to builtin free
[eva:malloc] allocated.c:67: strong free on bases: {__malloc_main_l63}
[eva] allocated.c:73: Call to builtin malloc
-[eva] allocated.c:73: allocating variable __malloc_main_l73
+[eva:malloc:new] allocated.c:73: allocating variable __malloc_main_l73
[eva] allocated.c:75: Frama_C_show_each_p: {{ &__malloc_main_l73 }}
[eva] allocated.c:76: Frama_C_show_each_p0: {0}
[eva] allocated.c:77: Call to builtin free
@@ -95,7 +95,7 @@
[eva] allocated.c:77: Call to builtin free
[eva:malloc] allocated.c:77: strong free on bases: {__malloc_main_l73}
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82
[eva] allocated.c:82: assertion got status valid.
[eva] allocated.c:87: Call to builtin free
[eva] allocated.c:87: function free: precondition 'freeable' got status valid.
@@ -123,14 +123,14 @@
[eva:malloc] allocated.c:82:
resizing variable `__malloc_w_main_l82' (0..-1/95) to fit 0..31/95
[eva] allocated.c:91: Call to builtin malloc
-[eva] allocated.c:91: allocating variable __malloc_main_l91
+[eva:malloc:new] allocated.c:91: allocating variable __malloc_main_l91
[eva] allocated.c:91: assertion got status valid.
[eva] allocated.c:92: Call to builtin free
[eva] allocated.c:92: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:92: strong free on bases: {__malloc_main_l91}
[eva:alarm] allocated.c:96: Warning: assertion 'Assume' got status unknown.
[eva] allocated.c:97: Call to builtin malloc
-[eva] allocated.c:97: allocating variable __malloc_main_l97
+[eva:malloc:new] allocated.c:97: allocating variable __malloc_main_l97
[eva] allocated.c:97: Frama_C_show_each: {{ &__malloc_main_l97 }}
[eva:alarm] allocated.c:98: Warning: out of bounds write. assert \valid(p);
[eva] allocated.c:110: Frama_C_show_each: {0}
@@ -139,7 +139,7 @@
[eva:malloc] allocated.c:111: strong free on bases: {__malloc_main_l97}
[eva:alarm] allocated.c:113: Warning: assertion got status unknown.
[eva] allocated.c:114: Call to builtin malloc
-[eva] allocated.c:114: allocating variable __malloc_main_l114
+[eva:malloc:new] allocated.c:114: allocating variable __malloc_main_l114
[eva] allocated.c:114: Frama_C_show_each: {{ &__malloc_main_l114 }}
[eva:alarm] allocated.c:115: Warning: out of bounds write. assert \valid(p);
[eva] allocated.c:117: Frama_C_show_each: {0}
@@ -147,7 +147,7 @@
[eva] allocated.c:118: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:118: strong free on bases: {__malloc_main_l114}
[eva] allocated.c:120: Call to builtin malloc
-[eva] allocated.c:120: allocating variable __malloc_main_l120
+[eva:malloc:new] allocated.c:120: allocating variable __malloc_main_l120
[eva] allocated.c:120: Frama_C_show_each: {{ &__malloc_main_l120 }}
[eva] allocated.c:123: Frama_C_show_each: ⊥
[eva] allocated.c:125: Call to builtin free
@@ -155,7 +155,7 @@
[eva:malloc] allocated.c:125: strong free on bases: {__malloc_main_l120}
[eva] allocated.c:127: assertion 'alloca_bounds' got status valid.
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127
[eva] allocated.c:131: Frama_C_show_each: {0}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
diff --git a/tests/builtins/oracle/allocated.1.res.oracle b/tests/builtins/oracle/allocated.1.res.oracle
index b214327bf47..61693dca458 100644
--- a/tests/builtins/oracle/allocated.1.res.oracle
+++ b/tests/builtins/oracle/allocated.1.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] allocated.c:25: Call to builtin malloc
-[eva] allocated.c:25: allocating variable __malloc_main_l25
+[eva:malloc:new] allocated.c:25: allocating variable __malloc_main_l25
[eva] allocated.c:25: assertion got status valid.
[eva:alarm] allocated.c:27: Warning:
out of bounds read. assert \valid_read(p + 1);
@@ -18,7 +18,7 @@
[eva:malloc] allocated.c:31: strong free on bases: {__malloc_main_l25}
[eva] allocated.c:32: Frama_C_show_each_p_after_free: ⊥
[eva] allocated.c:36: Call to builtin malloc
-[eva] allocated.c:36: allocating variable __malloc_main_l36
+[eva:malloc:new] allocated.c:36: allocating variable __malloc_main_l36
[eva] allocated.c:36: assertion got status valid.
[eva] allocated.c:40: Frama_C_show_each_p: {{ &__malloc_main_l36 }}
[eva] allocated.c:41: Frama_C_show_each_p0: {13}
@@ -40,9 +40,9 @@
[kernel] allocated.c:46: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] allocated.c:50: Call to builtin malloc
-[eva] allocated.c:50: allocating variable __malloc_main_l50
+[eva:malloc:new] allocated.c:50: allocating variable __malloc_main_l50
[eva] allocated.c:50: Call to builtin malloc
-[eva] allocated.c:50: allocating variable __malloc_main_l50_0
+[eva:malloc:new] allocated.c:50: allocating variable __malloc_main_l50_0
[eva] allocated.c:50: assertion got status valid.
[eva:alarm] allocated.c:53: Warning: out of bounds write. assert \valid(p + 2);
[kernel] allocated.c:53: Warning:
@@ -55,7 +55,7 @@
[eva] allocated.c:58: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:58: strong free on bases: {__malloc_main_l50_0}
[eva] allocated.c:63: Call to builtin malloc
-[eva] allocated.c:63: allocating variable __malloc_main_l63
+[eva:malloc:new] allocated.c:63: allocating variable __malloc_main_l63
[eva] allocated.c:63: assertion got status valid.
[eva] allocated.c:65: Frama_C_show_each_p: {{ &__malloc_main_l63 }}
[eva] allocated.c:66: Frama_C_show_each_p0: {0}
@@ -63,58 +63,58 @@
[eva] allocated.c:67: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:67: strong free on bases: {__malloc_main_l63}
[eva] allocated.c:63: Call to builtin malloc
-[eva] allocated.c:63: allocating variable __malloc_main_l63_0
+[eva:malloc:new] allocated.c:63: allocating variable __malloc_main_l63_0
[eva] allocated.c:65: Frama_C_show_each_p: {{ &__malloc_main_l63_0 }}
[eva] allocated.c:66: Frama_C_show_each_p0: {1}
[eva] allocated.c:67: Call to builtin free
[eva:malloc] allocated.c:67: strong free on bases: {__malloc_main_l63_0}
[eva] allocated.c:63: Call to builtin malloc
-[eva] allocated.c:63: allocating variable __malloc_main_l63_1
+[eva:malloc:new] allocated.c:63: allocating variable __malloc_main_l63_1
[eva] allocated.c:65: Frama_C_show_each_p: {{ &__malloc_main_l63_1 }}
[eva] allocated.c:66: Frama_C_show_each_p0: {2}
[eva] allocated.c:67: Call to builtin free
[eva:malloc] allocated.c:67: strong free on bases: {__malloc_main_l63_1}
[eva] allocated.c:63: Call to builtin malloc
-[eva] allocated.c:63: allocating variable __malloc_main_l63_2
+[eva:malloc:new] allocated.c:63: allocating variable __malloc_main_l63_2
[eva] allocated.c:65: Frama_C_show_each_p: {{ &__malloc_main_l63_2 }}
[eva] allocated.c:66: Frama_C_show_each_p0: {3}
[eva] allocated.c:67: Call to builtin free
[eva:malloc] allocated.c:67: strong free on bases: {__malloc_main_l63_2}
[eva] allocated.c:73: Call to builtin malloc
-[eva] allocated.c:73: allocating variable __malloc_main_l73
+[eva:malloc:new] allocated.c:73: allocating variable __malloc_main_l73
[eva] allocated.c:75: Frama_C_show_each_p: {{ &__malloc_main_l73 }}
[eva] allocated.c:76: Frama_C_show_each_p0: {0}
[eva] allocated.c:77: Call to builtin free
[eva] allocated.c:77: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:77: strong free on bases: {__malloc_main_l73}
[eva] allocated.c:73: Call to builtin malloc
-[eva] allocated.c:73: allocating variable __malloc_main_l73_0
+[eva:malloc:new] allocated.c:73: allocating variable __malloc_main_l73_0
[eva] allocated.c:75: Frama_C_show_each_p: {{ &__malloc_main_l73_0 }}
[eva] allocated.c:76: Frama_C_show_each_p0: {1}
[eva] allocated.c:77: Call to builtin free
[eva:malloc] allocated.c:77: strong free on bases: {__malloc_main_l73_0}
[eva] allocated.c:73: Call to builtin malloc
-[eva] allocated.c:73: allocating variable __malloc_main_l73_1
+[eva:malloc:new] allocated.c:73: allocating variable __malloc_main_l73_1
[eva] allocated.c:75: Frama_C_show_each_p: {{ &__malloc_main_l73_1 }}
[eva] allocated.c:76: Frama_C_show_each_p0: {2}
[eva] allocated.c:77: Call to builtin free
[eva:malloc] allocated.c:77: strong free on bases: {__malloc_main_l73_1}
[eva] allocated.c:73: Call to builtin malloc
-[eva] allocated.c:73: allocating variable __malloc_main_l73_2
+[eva:malloc:new] allocated.c:73: allocating variable __malloc_main_l73_2
[eva] allocated.c:75: Frama_C_show_each_p: {{ &__malloc_main_l73_2 }}
[eva] allocated.c:76: Frama_C_show_each_p0: {3}
[eva] allocated.c:77: Call to builtin free
[eva:malloc] allocated.c:77: strong free on bases: {__malloc_main_l73_2}
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82
[eva] allocated.c:82: assertion got status valid.
[eva] allocated.c:87: Call to builtin free
[eva] allocated.c:87: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82}
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_0
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_0
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_1
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_1
[eva] allocated.c:87: Call to builtin free
[eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_1}
[eva] allocated.c:87: Call to builtin free
@@ -124,15 +124,15 @@
[eva] allocated.c:87: Call to builtin free
[eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_0}
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_2
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_2
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_3
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_3
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_4
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_4
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_5
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_5
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_6
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_6
[eva] allocated.c:87: Call to builtin free
[eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_2}
[eva] allocated.c:87: Call to builtin free
@@ -174,53 +174,53 @@
[eva] allocated.c:87: Call to builtin free
[eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_6}
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_7
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_7
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_8
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_8
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_9
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_9
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_10
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_10
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_11
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_11
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_12
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_12
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_13
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_13
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_14
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_14
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_15
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_15
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_16
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_16
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_17
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_17
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_18
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_18
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_19
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_19
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_20
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_20
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_21
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_21
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_22
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_22
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_23
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_23
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_24
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_24
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_25
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_25
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_26
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_26
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_27
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_27
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_28
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_28
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_29
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_29
[eva] allocated.c:82: Call to builtin malloc
-[eva] allocated.c:82: allocating variable __malloc_main_l82_30
+[eva:malloc:new] allocated.c:82: allocating variable __malloc_main_l82_30
[eva] allocated.c:84: Trace partitioning superposing up to 100 states
[eva] allocated.c:84: Trace partitioning superposing up to 200 states
[eva] allocated.c:84: Trace partitioning superposing up to 300 states
@@ -610,14 +610,14 @@
[eva] allocated.c:87: Call to builtin free
[eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
[eva] allocated.c:91: Call to builtin malloc
-[eva] allocated.c:91: allocating variable __malloc_main_l91
+[eva:malloc:new] allocated.c:91: allocating variable __malloc_main_l91
[eva] allocated.c:91: assertion got status valid.
[eva] allocated.c:92: Call to builtin free
[eva] allocated.c:92: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:92: strong free on bases: {__malloc_main_l91}
[eva:alarm] allocated.c:96: Warning: assertion 'Assume' got status unknown.
[eva] allocated.c:97: Call to builtin malloc
-[eva] allocated.c:97: allocating variable __malloc_main_l97
+[eva:malloc:new] allocated.c:97: allocating variable __malloc_main_l97
[eva] allocated.c:97: Frama_C_show_each: {{ &__malloc_main_l97 }}
[eva:alarm] allocated.c:98: Warning: out of bounds write. assert \valid(p);
[eva] allocated.c:110: Frama_C_show_each: {0}
@@ -626,7 +626,7 @@
[eva:malloc] allocated.c:111: strong free on bases: {__malloc_main_l97}
[eva:alarm] allocated.c:113: Warning: assertion got status unknown.
[eva] allocated.c:114: Call to builtin malloc
-[eva] allocated.c:114: allocating variable __malloc_main_l114
+[eva:malloc:new] allocated.c:114: allocating variable __malloc_main_l114
[eva] allocated.c:114: Frama_C_show_each: {{ &__malloc_main_l114 }}
[eva:alarm] allocated.c:115: Warning: out of bounds write. assert \valid(p);
[eva] allocated.c:117: Frama_C_show_each: {0}
@@ -634,7 +634,7 @@
[eva] allocated.c:118: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:118: strong free on bases: {__malloc_main_l114}
[eva] allocated.c:120: Call to builtin malloc
-[eva] allocated.c:120: allocating variable __malloc_main_l120
+[eva:malloc:new] allocated.c:120: allocating variable __malloc_main_l120
[eva] allocated.c:120: Frama_C_show_each: {{ &__malloc_main_l120 }}
[eva] allocated.c:123: Frama_C_show_each: ⊥
[eva] allocated.c:125: Call to builtin free
@@ -642,52 +642,52 @@
[eva:malloc] allocated.c:125: strong free on bases: {__malloc_main_l120}
[eva] allocated.c:127: assertion 'alloca_bounds' got status valid.
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127
[eva] allocated.c:131: Frama_C_show_each: {0}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127_0
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127_0
[eva] allocated.c:131: Frama_C_show_each: {1}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_0}
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127_1
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127_1
[eva] allocated.c:131: Frama_C_show_each: {2}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_1}
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127_2
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127_2
[eva] allocated.c:131: Frama_C_show_each: {3}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_2}
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127_3
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127_3
[eva] allocated.c:131: Frama_C_show_each: {4}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_3}
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127_4
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127_4
[eva] allocated.c:131: Frama_C_show_each: {5}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_4}
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127_5
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127_5
[eva] allocated.c:131: Frama_C_show_each: {6}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_5}
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127_6
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127_6
[eva] allocated.c:131: Frama_C_show_each: {7}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_6}
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127_7
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127_7
[eva] allocated.c:131: Frama_C_show_each: {8}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_7}
[eva] allocated.c:127: Call to builtin __fc_vla_alloc
-[eva] allocated.c:127: allocating variable __malloc_main_l127_8
+[eva:malloc:new] allocated.c:127: allocating variable __malloc_main_l127_8
[eva] allocated.c:131: Frama_C_show_each: {9}
[eva] allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_8}
diff --git a/tests/builtins/oracle/calloc.1.res.oracle b/tests/builtins/oracle/calloc.1.res.oracle
index dd49f843488..aeadce0c13d 100644
--- a/tests/builtins/oracle/calloc.1.res.oracle
+++ b/tests/builtins/oracle/calloc.1.res.oracle
@@ -5,17 +5,17 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] calloc.c:14: Call to builtin calloc
-[eva] calloc.c:14: allocating variable __calloc_main_l14
+[eva:malloc:new] calloc.c:14: allocating variable __calloc_main_l14
[eva] calloc.c:17: Call to builtin calloc
-[eva] calloc.c:17: allocating variable __calloc_main_l17
+[eva:malloc:new] calloc.c:17: allocating variable __calloc_main_l17
[eva] calloc.c:20: Call to builtin calloc
-[eva] calloc.c:20: allocating variable __calloc_main_l20
+[eva:malloc:new] calloc.c:20: allocating variable __calloc_main_l20
[eva] calloc.c:23: Call to builtin calloc
-[eva] calloc.c:23: allocating variable __calloc_main_l23
+[eva:malloc:new] calloc.c:23: allocating variable __calloc_main_l23
[eva] calloc.c:26: assertion got status valid.
[eva] calloc.c:27: assertion got status valid.
[eva] calloc.c:30: Call to builtin calloc
-[eva] calloc.c:30: allocating variable __calloc_main_l30
+[eva:malloc:new] calloc.c:30: allocating variable __calloc_main_l30
[eva] calloc.c:33: assertion got status valid.
[eva] calloc.c:34: assertion got status valid.
[eva] calloc.c:35: assertion got status valid.
diff --git a/tests/builtins/oracle/calloc.2.res.oracle b/tests/builtins/oracle/calloc.2.res.oracle
index dd49f843488..aeadce0c13d 100644
--- a/tests/builtins/oracle/calloc.2.res.oracle
+++ b/tests/builtins/oracle/calloc.2.res.oracle
@@ -5,17 +5,17 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] calloc.c:14: Call to builtin calloc
-[eva] calloc.c:14: allocating variable __calloc_main_l14
+[eva:malloc:new] calloc.c:14: allocating variable __calloc_main_l14
[eva] calloc.c:17: Call to builtin calloc
-[eva] calloc.c:17: allocating variable __calloc_main_l17
+[eva:malloc:new] calloc.c:17: allocating variable __calloc_main_l17
[eva] calloc.c:20: Call to builtin calloc
-[eva] calloc.c:20: allocating variable __calloc_main_l20
+[eva:malloc:new] calloc.c:20: allocating variable __calloc_main_l20
[eva] calloc.c:23: Call to builtin calloc
-[eva] calloc.c:23: allocating variable __calloc_main_l23
+[eva:malloc:new] calloc.c:23: allocating variable __calloc_main_l23
[eva] calloc.c:26: assertion got status valid.
[eva] calloc.c:27: assertion got status valid.
[eva] calloc.c:30: Call to builtin calloc
-[eva] calloc.c:30: allocating variable __calloc_main_l30
+[eva:malloc:new] calloc.c:30: allocating variable __calloc_main_l30
[eva] calloc.c:33: assertion got status valid.
[eva] calloc.c:34: assertion got status valid.
[eva] calloc.c:35: assertion got status valid.
diff --git a/tests/builtins/oracle/calloc.3.res.oracle b/tests/builtins/oracle/calloc.3.res.oracle
index dd49f843488..aeadce0c13d 100644
--- a/tests/builtins/oracle/calloc.3.res.oracle
+++ b/tests/builtins/oracle/calloc.3.res.oracle
@@ -5,17 +5,17 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] calloc.c:14: Call to builtin calloc
-[eva] calloc.c:14: allocating variable __calloc_main_l14
+[eva:malloc:new] calloc.c:14: allocating variable __calloc_main_l14
[eva] calloc.c:17: Call to builtin calloc
-[eva] calloc.c:17: allocating variable __calloc_main_l17
+[eva:malloc:new] calloc.c:17: allocating variable __calloc_main_l17
[eva] calloc.c:20: Call to builtin calloc
-[eva] calloc.c:20: allocating variable __calloc_main_l20
+[eva:malloc:new] calloc.c:20: allocating variable __calloc_main_l20
[eva] calloc.c:23: Call to builtin calloc
-[eva] calloc.c:23: allocating variable __calloc_main_l23
+[eva:malloc:new] calloc.c:23: allocating variable __calloc_main_l23
[eva] calloc.c:26: assertion got status valid.
[eva] calloc.c:27: assertion got status valid.
[eva] calloc.c:30: Call to builtin calloc
-[eva] calloc.c:30: allocating variable __calloc_main_l30
+[eva:malloc:new] calloc.c:30: allocating variable __calloc_main_l30
[eva] calloc.c:33: assertion got status valid.
[eva] calloc.c:34: assertion got status valid.
[eva] calloc.c:35: assertion got status valid.
diff --git a/tests/builtins/oracle/calloc.4.res.oracle b/tests/builtins/oracle/calloc.4.res.oracle
index dd49f843488..aeadce0c13d 100644
--- a/tests/builtins/oracle/calloc.4.res.oracle
+++ b/tests/builtins/oracle/calloc.4.res.oracle
@@ -5,17 +5,17 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] calloc.c:14: Call to builtin calloc
-[eva] calloc.c:14: allocating variable __calloc_main_l14
+[eva:malloc:new] calloc.c:14: allocating variable __calloc_main_l14
[eva] calloc.c:17: Call to builtin calloc
-[eva] calloc.c:17: allocating variable __calloc_main_l17
+[eva:malloc:new] calloc.c:17: allocating variable __calloc_main_l17
[eva] calloc.c:20: Call to builtin calloc
-[eva] calloc.c:20: allocating variable __calloc_main_l20
+[eva:malloc:new] calloc.c:20: allocating variable __calloc_main_l20
[eva] calloc.c:23: Call to builtin calloc
-[eva] calloc.c:23: allocating variable __calloc_main_l23
+[eva:malloc:new] calloc.c:23: allocating variable __calloc_main_l23
[eva] calloc.c:26: assertion got status valid.
[eva] calloc.c:27: assertion got status valid.
[eva] calloc.c:30: Call to builtin calloc
-[eva] calloc.c:30: allocating variable __calloc_main_l30
+[eva:malloc:new] calloc.c:30: allocating variable __calloc_main_l30
[eva] calloc.c:33: assertion got status valid.
[eva] calloc.c:34: assertion got status valid.
[eva] calloc.c:35: assertion got status valid.
diff --git a/tests/builtins/oracle/free.res.oracle b/tests/builtins/oracle/free.res.oracle
index 402a7224a2c..7e8b3e36c70 100644
--- a/tests/builtins/oracle/free.res.oracle
+++ b/tests/builtins/oracle/free.res.oracle
@@ -7,9 +7,9 @@
[eva] computing for function main1 <- main.
Called from free.c:44.
[eva] free.c:8: Call to builtin malloc
-[eva] free.c:8: allocating variable __malloc_main1_l8
+[eva:malloc:new] free.c:8: allocating variable __malloc_main1_l8
[eva] free.c:10: Call to builtin malloc
-[eva] free.c:10: allocating variable __malloc_main1_l10
+[eva:malloc:new] free.c:10: allocating variable __malloc_main1_l10
[eva] free.c:13:
Frama_C_dump_each:
# cvalue:
@@ -49,7 +49,7 @@
[eva:malloc] free.c:14:
weak free on bases: {__malloc_main1_l8, __malloc_main1_l10}
[eva] free.c:16: Call to builtin malloc
-[eva] free.c:16: allocating variable __malloc_main1_l16
+[eva:malloc:new] free.c:16: allocating variable __malloc_main1_l16
[eva] free.c:18: Call to builtin free
[eva] free.c:18: function free: precondition 'freeable' got status valid.
[eva:malloc] free.c:18: strong free on bases: {__malloc_main1_l16}
@@ -57,7 +57,7 @@
[eva] free.c:21: function free: precondition 'freeable' got status valid.
[eva:malloc] free.c:21: strong free on bases: {}
[eva] free.c:23: Call to builtin malloc
-[eva] free.c:23: allocating variable __malloc_main1_l23
+[eva:malloc:new] free.c:23: allocating variable __malloc_main1_l23
[eva] free.c:26: Call to builtin free
[eva] free.c:26: function free: precondition 'freeable' got status valid.
[eva:malloc] free.c:26: weak free on bases: {__malloc_main1_l23}
@@ -66,7 +66,7 @@
[eva] computing for function main2 <- main.
Called from free.c:45.
[eva] free.c:35: Call to builtin malloc
-[eva] free.c:35: allocating variable __malloc_main2_l35
+[eva:malloc:new] free.c:35: allocating variable __malloc_main2_l35
[eva] free.c:39: Call to builtin free
[eva] free.c:39: function free: precondition 'freeable' got status valid.
[eva:malloc] free.c:39: strong free on bases: {__malloc_main2_l35}
diff --git a/tests/builtins/oracle/from_result.res.oracle b/tests/builtins/oracle/from_result.res.oracle
index 5d1543b18fd..947ea0bed39 100644
--- a/tests/builtins/oracle/from_result.res.oracle
+++ b/tests/builtins/oracle/from_result.res.oracle
@@ -7,13 +7,13 @@
[eva] computing for function bar <- main.
Called from from_result.c:32.
[eva] from_result.c:18: Call to builtin malloc
-[eva] from_result.c:18: allocating variable __malloc_bar_l18
+[eva:malloc:new] 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 from_result.c:33.
[eva] from_result.c:18: Call to builtin malloc
-[eva] from_result.c:18: allocating variable __malloc_bar_l18_0
+[eva:malloc:new] from_result.c:18: allocating variable __malloc_bar_l18_0
[eva] Recording results for bar
[eva] Done for function bar
[eva] computing for function create_t <- main.
diff --git a/tests/builtins/oracle/gcc_zero_length_array.res.oracle b/tests/builtins/oracle/gcc_zero_length_array.res.oracle
index e206f5dec12..2de3773f803 100644
--- a/tests/builtins/oracle/gcc_zero_length_array.res.oracle
+++ b/tests/builtins/oracle/gcc_zero_length_array.res.oracle
@@ -7,7 +7,8 @@
[eva] computing for function make_fam <- main.
Called from gcc_zero_length_array.c:24.
[eva] gcc_zero_length_array.c:15: Call to builtin malloc
-[eva] gcc_zero_length_array.c:15: allocating variable __malloc_make_fam_l15
+[eva:malloc:new] gcc_zero_length_array.c:15:
+ allocating variable __malloc_make_fam_l15
[eva] Recording results for make_fam
[eva] Done for function make_fam
[eva] gcc_zero_length_array.c:26: Call to builtin free
diff --git a/tests/builtins/oracle/imprecise-malloc-free.res.oracle b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
index 12f3b1ea66b..559cff3d4d4 100644
--- a/tests/builtins/oracle/imprecise-malloc-free.res.oracle
+++ b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
@@ -21,11 +21,14 @@
Assigning imprecise value to size
because of arithmetic operation on addresses.
[eva] imprecise-malloc-free.c:14: Call to builtin malloc
-[eva] imprecise-malloc-free.c:14: allocating variable __malloc_main_l14
+[eva:malloc:new] imprecise-malloc-free.c:14:
+ allocating variable __malloc_main_l14
[eva] imprecise-malloc-free.c:15: Call to builtin malloc
-[eva] imprecise-malloc-free.c:15: allocating variable __malloc_main_l15
+[eva:malloc:new] imprecise-malloc-free.c:15:
+ allocating variable __malloc_main_l15
[eva] imprecise-malloc-free.c:16: Call to builtin malloc
-[eva] imprecise-malloc-free.c:16: allocating variable __malloc_main_l16
+[eva:malloc:new] imprecise-malloc-free.c:16:
+ allocating variable __malloc_main_l16
[eva] imprecise-malloc-free.c:18:
Frama_C_show_each:
{{ &__malloc_main_l14 }}, {{ &__malloc_main_l15 }}, {{ &__malloc_main_l16 }}
diff --git a/tests/builtins/oracle/malloc-deps.res.oracle b/tests/builtins/oracle/malloc-deps.res.oracle
index 78a74a85a12..4a24d0440cc 100644
--- a/tests/builtins/oracle/malloc-deps.res.oracle
+++ b/tests/builtins/oracle/malloc-deps.res.oracle
@@ -5,11 +5,11 @@
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
[eva] malloc-deps.c:12: Call to builtin malloc
-[eva] malloc-deps.c:12: allocating weak variable __malloc_w_main_l12
+[eva:malloc:new] malloc-deps.c:12: allocating weak variable __malloc_w_main_l12
[eva] malloc-deps.c:17: Call to builtin malloc
-[eva] malloc-deps.c:17: allocating variable __malloc_main_l17
+[eva:malloc:new] malloc-deps.c:17: allocating variable __malloc_main_l17
[eva] malloc-deps.c:25: Call to builtin malloc
-[eva] malloc-deps.c:25: allocating variable __malloc_main_l25
+[eva:malloc:new] malloc-deps.c:25: allocating variable __malloc_main_l25
[eva] computing for function g <- main.
Called from malloc-deps.c:26.
[eva:alarm] malloc-deps.c:7: Warning: out of bounds write. assert \valid(p + k);
diff --git a/tests/builtins/oracle/malloc-optimistic.res.oracle b/tests/builtins/oracle/malloc-optimistic.res.oracle
index 60e8831d456..b22dec34c0b 100644
--- a/tests/builtins/oracle/malloc-optimistic.res.oracle
+++ b/tests/builtins/oracle/malloc-optimistic.res.oracle
@@ -9,7 +9,7 @@
[eva] malloc-optimistic.c:16: Frama_C_show_each_1_1: {0}
[eva] malloc-optimistic.c:16: Frama_C_show_each_1_1: {1}
[eva] malloc-optimistic.c:17: Call to builtin malloc
-[eva] malloc-optimistic.c:17: allocating variable __malloc_main1_l17
+[eva:malloc:new] malloc-optimistic.c:17: allocating variable __malloc_main1_l17
[eva] malloc-optimistic.c:17: Call to builtin malloc
[eva:malloc] malloc-optimistic.c:17:
resizing variable `__malloc_main1_l17' (0..31) to fit 0..63
@@ -26,7 +26,7 @@
[eva] malloc-optimistic.c:26: Frama_C_show_each_2_1: {2}
[eva] malloc-optimistic.c:26: Frama_C_show_each_2_1: {1}
[eva] malloc-optimistic.c:27: Call to builtin malloc
-[eva] malloc-optimistic.c:27: allocating variable __malloc_main2_l27
+[eva:malloc:new] malloc-optimistic.c:27: allocating variable __malloc_main2_l27
[eva] malloc-optimistic.c:27: Call to builtin malloc
[eva:malloc] malloc-optimistic.c:27:
resizing variable `__malloc_main2_l27' (0..95) to fit 0..63
@@ -43,7 +43,8 @@
[eva] computing for function main_3_aux <- main3 <- main.
Called from malloc-optimistic.c:48.
[eva] malloc-optimistic.c:34: Call to builtin malloc
-[eva] malloc-optimistic.c:34: allocating variable __malloc_main_3_aux_l34
+[eva:malloc:new] malloc-optimistic.c:34:
+ allocating variable __malloc_main_3_aux_l34
[eva] Recording results for main_3_aux
[eva] Done for function main_3_aux
[eva] computing for function main_3_aux <- main3 <- main.
@@ -65,7 +66,8 @@
[eva] computing for function main_4_aux <- main4 <- main.
Called from malloc-optimistic.c:56.
[eva] malloc-optimistic.c:40: Call to builtin malloc
-[eva] malloc-optimistic.c:40: allocating variable __malloc_main_4_aux_l40
+[eva:malloc:new] malloc-optimistic.c:40:
+ allocating variable __malloc_main_4_aux_l40
[eva] Recording results for main_4_aux
[eva] Done for function main_4_aux
[eva] computing for function main_4_aux <- main4 <- main.
@@ -83,7 +85,7 @@
[eva] computing for function main5 <- main.
Called from malloc-optimistic.c:144.
[eva] malloc-optimistic.c:64: Call to builtin malloc
-[eva] malloc-optimistic.c:64: allocating variable __malloc_main5_l64
+[eva:malloc:new] malloc-optimistic.c:64: allocating variable __malloc_main5_l64
[eva] malloc-optimistic.c:64: Call to builtin malloc
[eva:malloc] malloc-optimistic.c:64:
resizing variable `__malloc_main5_l64' (0..31) to fit 0..63
@@ -449,7 +451,7 @@
[eva] computing for function main6 <- main.
Called from malloc-optimistic.c:145.
[eva] malloc-optimistic.c:77: Call to builtin malloc
-[eva] malloc-optimistic.c:77: allocating variable __malloc_main6_l77
+[eva:malloc:new] malloc-optimistic.c:77: allocating variable __malloc_main6_l77
[eva] malloc-optimistic.c:77: Call to builtin malloc
[eva:malloc] malloc-optimistic.c:77:
resizing variable `__malloc_main6_l77' (0..31) to fit 0..63
@@ -880,7 +882,7 @@
[eva] computing for function main7 <- main.
Called from malloc-optimistic.c:148.
[eva] malloc-optimistic.c:90: Call to builtin malloc
-[eva] malloc-optimistic.c:90: allocating variable __malloc_main7_l90
+[eva:malloc:new] malloc-optimistic.c:90: allocating variable __malloc_main7_l90
[eva] malloc-optimistic.c:90: Call to builtin malloc
[eva:malloc] malloc-optimistic.c:90:
resizing variable `__malloc_main7_l90' (0..31) to fit 0..63
@@ -1875,7 +1877,8 @@
[eva] computing for function main8 <- main.
Called from malloc-optimistic.c:149.
[eva] malloc-optimistic.c:103: Call to builtin malloc
-[eva] malloc-optimistic.c:103: allocating variable __malloc_main8_l103
+[eva:malloc:new] malloc-optimistic.c:103:
+ allocating variable __malloc_main8_l103
[eva] malloc-optimistic.c:103: Call to builtin malloc
[eva:malloc] malloc-optimistic.c:103:
resizing variable `__malloc_main8_l103' (0..31) to fit 0..63
@@ -3120,7 +3123,8 @@
[eva] computing for function main9 <- main.
Called from malloc-optimistic.c:150.
[eva] malloc-optimistic.c:119: Call to builtin malloc
-[eva] malloc-optimistic.c:119: allocating variable __malloc_main9_l119
+[eva:malloc:new] malloc-optimistic.c:119:
+ allocating variable __malloc_main9_l119
[eva] malloc-optimistic.c:120:
Frama_C_show_each: {0}, {{ &__malloc_main9_l119 }}
[eva] malloc-optimistic.c:122: Frama_C_show_each: {0}
diff --git a/tests/builtins/oracle/malloc-size-zero.0.res.oracle b/tests/builtins/oracle/malloc-size-zero.0.res.oracle
index 67dbcf45f09..46969acb5e8 100644
--- a/tests/builtins/oracle/malloc-size-zero.0.res.oracle
+++ b/tests/builtins/oracle/malloc-size-zero.0.res.oracle
@@ -7,7 +7,8 @@
[eva] computing for function my_calloc <- main.
Called from malloc-size-zero.c:16.
[eva] malloc-size-zero.c:10: Call to builtin malloc
-[eva] malloc-size-zero.c:10: allocating variable __malloc_my_calloc_l10
+[eva:malloc:new] malloc-size-zero.c:10:
+ allocating variable __malloc_my_calloc_l10
[eva] Recording results for my_calloc
[eva] Done for function my_calloc
[eva] malloc-size-zero.c:20: Frama_C_show_each_not_NULL_p1:
@@ -16,26 +17,30 @@
[eva] computing for function my_calloc <- main.
Called from malloc-size-zero.c:29.
[eva] malloc-size-zero.c:10: Call to builtin malloc
-[eva] malloc-size-zero.c:10: allocating variable __malloc_my_calloc_l10_0
+[eva:malloc:new] malloc-size-zero.c:10:
+ allocating variable __malloc_my_calloc_l10_0
[eva] Recording results for my_calloc
[eva] Done for function my_calloc
[eva] malloc-size-zero.c:27: starting to merge loop iterations
[eva] computing for function my_calloc <- main.
Called from malloc-size-zero.c:29.
[eva] malloc-size-zero.c:10: Call to builtin malloc
-[eva] malloc-size-zero.c:10: allocating variable __malloc_my_calloc_l10_1
+[eva:malloc:new] malloc-size-zero.c:10:
+ allocating variable __malloc_my_calloc_l10_1
[eva] Recording results for my_calloc
[eva] Done for function my_calloc
[eva] computing for function my_calloc <- main.
Called from malloc-size-zero.c:29.
[eva] malloc-size-zero.c:10: Call to builtin malloc
-[eva] malloc-size-zero.c:10: allocating variable __malloc_my_calloc_l10_2
+[eva:malloc:new] malloc-size-zero.c:10:
+ allocating variable __malloc_my_calloc_l10_2
[eva] Recording results for my_calloc
[eva] Done for function my_calloc
[eva] computing for function my_calloc <- main.
Called from malloc-size-zero.c:29.
[eva] malloc-size-zero.c:10: Call to builtin malloc
-[eva] malloc-size-zero.c:10: allocating variable __malloc_my_calloc_l10_3
+[eva:malloc:new] malloc-size-zero.c:10:
+ allocating variable __malloc_my_calloc_l10_3
[eva] Recording results for my_calloc
[eva] Done for function my_calloc
[eva] computing for function my_calloc <- main.
diff --git a/tests/builtins/oracle/malloc-size-zero.1.res.oracle b/tests/builtins/oracle/malloc-size-zero.1.res.oracle
index 6cbcd7bba07..51b8f812c59 100644
--- a/tests/builtins/oracle/malloc-size-zero.1.res.oracle
+++ b/tests/builtins/oracle/malloc-size-zero.1.res.oracle
@@ -7,7 +7,7 @@
[eva] computing for function my_calloc <- main.
Called from malloc-size-zero.c:16.
[eva] malloc-size-zero.c:10: Call to builtin malloc
-[eva] malloc-size-zero.c:10: allocating variable __malloc_main_l16
+[eva:malloc:new] malloc-size-zero.c:10: allocating variable __malloc_main_l16
[eva] Recording results for my_calloc
[eva] Done for function my_calloc
[eva] malloc-size-zero.c:20: Frama_C_show_each_not_NULL_p1:
@@ -16,7 +16,7 @@
[eva] computing for function my_calloc <- main.
Called from malloc-size-zero.c:29.
[eva] malloc-size-zero.c:10: Call to builtin malloc
-[eva] malloc-size-zero.c:10: allocating variable __malloc_main_l29
+[eva:malloc:new] malloc-size-zero.c:10: allocating variable __malloc_main_l29
[eva] Recording results for my_calloc
[eva] Done for function my_calloc
[eva] malloc-size-zero.c:27: starting to merge loop iterations
diff --git a/tests/builtins/oracle/malloc.res.oracle b/tests/builtins/oracle/malloc.res.oracle
index 5f863f78b8d..976bc7dc0fd 100644
--- a/tests/builtins/oracle/malloc.res.oracle
+++ b/tests/builtins/oracle/malloc.res.oracle
@@ -5,19 +5,19 @@
[eva:initial-state] Values of globals at initialization
[eva] malloc.c:11: Call to builtin malloc
-[eva] malloc.c:11: allocating variable __malloc_main_l11
+[eva:malloc:new] malloc.c:11: allocating variable __malloc_main_l11
[eva] malloc.c:17: Call to builtin malloc
-[eva] malloc.c:17: allocating variable __malloc_main_l17
+[eva:malloc:new] malloc.c:17: allocating variable __malloc_main_l17
[eva] malloc.c:17: Call to builtin malloc
[eva:malloc] malloc.c:17:
resizing variable `__malloc_main_l17' (0..-1/34359738359) to fit 0..-1
[eva] malloc.c:18: Call to builtin malloc
-[eva] malloc.c:18: allocating variable __malloc_main_l18
+[eva:malloc:new] malloc.c:18: allocating variable __malloc_main_l18
[eva] malloc.c:18: Call to builtin malloc
[eva] malloc.c:20: Call to builtin malloc
-[eva] malloc.c:20: allocating variable __malloc_main_l20
+[eva:malloc:new] malloc.c:20: allocating variable __malloc_main_l20
[eva] malloc.c:20: Call to builtin malloc
-[eva] malloc.c:20: allocating variable __malloc_main_l20_0
+[eva:malloc:new] malloc.c:20: allocating variable __malloc_main_l20_0
[eva:alarm] malloc.c:21: Warning: out of bounds write. assert \valid(p);
[eva:alarm] malloc.c:22: Warning: out of bounds write. assert \valid(p + 2);
[eva:alarm] malloc.c:23: Warning: out of bounds write. assert \valid(p + 24999);
diff --git a/tests/builtins/oracle/malloc_bug_tr.res.oracle b/tests/builtins/oracle/malloc_bug_tr.res.oracle
index d2efa197350..27d7e5af31d 100644
--- a/tests/builtins/oracle/malloc_bug_tr.res.oracle
+++ b/tests/builtins/oracle/malloc_bug_tr.res.oracle
@@ -11,7 +11,7 @@
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] malloc_bug_tr.c:12: Call to builtin malloc
-[eva] malloc_bug_tr.c:12: allocating variable __malloc_main_l12
+[eva:malloc:new] malloc_bug_tr.c:12: allocating variable __malloc_main_l12
[eva] malloc_bug_tr.c:13: Call to builtin memcpy
[eva] malloc_bug_tr.c:13:
function memcpy: precondition 'valid_dest' got status valid.
diff --git a/tests/builtins/oracle/malloc_individual.res.oracle b/tests/builtins/oracle/malloc_individual.res.oracle
index a7782384600..24aaaa3319b 100644
--- a/tests/builtins/oracle/malloc_individual.res.oracle
+++ b/tests/builtins/oracle/malloc_individual.res.oracle
@@ -8,7 +8,7 @@
B ∈ {0}
C ∈ {0}
[eva] malloc_individual.c:12: Call to builtin malloc
-[eva] malloc_individual.c:12: allocating variable __malloc_main_l12
+[eva:malloc:new] malloc_individual.c:12: allocating variable __malloc_main_l12
[eva:alarm] malloc_individual.c:15: Warning:
accessing uninitialized left-value. assert \initialized(p);
[eva] Recording results for main
diff --git a/tests/builtins/oracle/malloc_memexec.res.oracle b/tests/builtins/oracle/malloc_memexec.res.oracle
index 1791b356140..07be019cae2 100644
--- a/tests/builtins/oracle/malloc_memexec.res.oracle
+++ b/tests/builtins/oracle/malloc_memexec.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
[eva] malloc_memexec.c:14: Call to builtin malloc
-[eva] malloc_memexec.c:14: allocating variable __malloc_main_l14
+[eva:malloc:new] malloc_memexec.c:14: allocating variable __malloc_main_l14
[eva] computing for function f <- main.
Called from malloc_memexec.c:16.
[eva] Recording results for f
@@ -19,7 +19,8 @@
[eva] Recording results for f
[eva] Done for function f
[eva] malloc_memexec.c:23: Call to builtin malloc
-[eva] malloc_memexec.c:23: allocating weak variable __malloc_w_main_l23
+[eva:malloc:new] malloc_memexec.c:23:
+ allocating weak variable __malloc_w_main_l23
[eva] computing for function f <- main.
Called from malloc_memexec.c:25.
[eva] Recording results for f
diff --git a/tests/builtins/oracle/malloc_multiple.res.oracle b/tests/builtins/oracle/malloc_multiple.res.oracle
index eee3cf75205..d63a2ebb4c3 100644
--- a/tests/builtins/oracle/malloc_multiple.res.oracle
+++ b/tests/builtins/oracle/malloc_multiple.res.oracle
@@ -8,19 +8,26 @@
[eva] computing for function allocate_T <- main.
Called from malloc_multiple.c:42.
[eva] malloc_multiple.c:11: Call to builtin malloc
-[eva] malloc_multiple.c:11: allocating variable __malloc_allocate_T_l11
+[eva:malloc:new] malloc_multiple.c:11:
+ allocating variable __malloc_allocate_T_l11
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_0
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_0
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_1
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_1
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_2
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_2
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_3
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_3
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_4
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_4
[eva] malloc_multiple.c:14: Call to builtin malloc
[eva:malloc:weak] malloc_multiple.c:14:
marking variable `__malloc_allocate_T_l14_4' as weak
@@ -31,19 +38,26 @@
[eva] computing for function allocate_T <- main.
Called from malloc_multiple.c:43.
[eva] malloc_multiple.c:11: Call to builtin malloc
-[eva] malloc_multiple.c:11: allocating variable __malloc_allocate_T_l11_0
+[eva:malloc:new] malloc_multiple.c:11:
+ allocating variable __malloc_allocate_T_l11_0
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_5
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_5
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_6
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_6
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_7
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_7
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_8
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_8
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_9
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_9
[eva] malloc_multiple.c:14: Call to builtin malloc
-[eva] malloc_multiple.c:14: allocating variable __malloc_allocate_T_l14_10
+[eva:malloc:new] malloc_multiple.c:14:
+ allocating variable __malloc_allocate_T_l14_10
[eva] malloc_multiple.c:14: Call to builtin malloc
[eva:malloc:weak] malloc_multiple.c:14:
marking variable `__malloc_allocate_T_l14_10' as weak
@@ -54,32 +68,32 @@
[eva] computing for function allocate_and_free_last <- main.
Called from malloc_multiple.c:44.
[eva] malloc_multiple.c:29: Call to builtin malloc
-[eva] malloc_multiple.c:29:
+[eva:malloc:new] malloc_multiple.c:29:
allocating variable __malloc_allocate_and_free_last_l29
[eva] malloc_multiple.c:31:
Frama_C_show_each_F: {{ &__malloc_allocate_and_free_last_l29 }}
[eva] malloc_multiple.c:29: Call to builtin malloc
-[eva] malloc_multiple.c:29:
+[eva:malloc:new] malloc_multiple.c:29:
allocating variable __malloc_allocate_and_free_last_l29_0
[eva] malloc_multiple.c:31:
Frama_C_show_each_F: {{ &__malloc_allocate_and_free_last_l29_0 }}
[eva] malloc_multiple.c:29: Call to builtin malloc
-[eva] malloc_multiple.c:29:
+[eva:malloc:new] malloc_multiple.c:29:
allocating variable __malloc_allocate_and_free_last_l29_1
[eva] malloc_multiple.c:31:
Frama_C_show_each_F: {{ &__malloc_allocate_and_free_last_l29_1 }}
[eva] malloc_multiple.c:29: Call to builtin malloc
-[eva] malloc_multiple.c:29:
+[eva:malloc:new] malloc_multiple.c:29:
allocating variable __malloc_allocate_and_free_last_l29_2
[eva] malloc_multiple.c:31:
Frama_C_show_each_F: {{ &__malloc_allocate_and_free_last_l29_2 }}
[eva] malloc_multiple.c:29: Call to builtin malloc
-[eva] malloc_multiple.c:29:
+[eva:malloc:new] malloc_multiple.c:29:
allocating variable __malloc_allocate_and_free_last_l29_3
[eva] malloc_multiple.c:31:
Frama_C_show_each_F: {{ &__malloc_allocate_and_free_last_l29_3 }}
[eva] malloc_multiple.c:29: Call to builtin malloc
-[eva] malloc_multiple.c:29:
+[eva:malloc:new] malloc_multiple.c:29:
allocating variable __malloc_allocate_and_free_last_l29_4
[eva] malloc_multiple.c:31:
Frama_C_show_each_F: {{ &__malloc_allocate_and_free_last_l29_4 }}
diff --git a/tests/builtins/oracle/memexec-malloc.res.oracle b/tests/builtins/oracle/memexec-malloc.res.oracle
index 72ede79e78e..21784bb7920 100644
--- a/tests/builtins/oracle/memexec-malloc.res.oracle
+++ b/tests/builtins/oracle/memexec-malloc.res.oracle
@@ -21,13 +21,13 @@
[eva] computing for function alloc <- main.
Called from memexec-malloc.c:31.
[eva] memexec-malloc.c:15: Call to builtin malloc
-[eva] memexec-malloc.c:15: allocating variable __malloc_main_l31
+[eva:malloc:new] memexec-malloc.c:15: allocating variable __malloc_main_l31
[eva] Recording results for alloc
[eva] Done for function alloc
[eva] computing for function alloc <- main.
Called from memexec-malloc.c:32.
[eva] memexec-malloc.c:15: Call to builtin malloc
-[eva] memexec-malloc.c:15: allocating variable __malloc_main_l32
+[eva:malloc:new] memexec-malloc.c:15: allocating variable __malloc_main_l32
[eva] Recording results for alloc
[eva] Done for function alloc
[eva] computing for function k <- main.
@@ -35,7 +35,7 @@
[eva] computing for function alloc <- k <- main.
Called from memexec-malloc.c:19.
[eva] memexec-malloc.c:15: Call to builtin malloc
-[eva] memexec-malloc.c:15: allocating variable __malloc_k_l19
+[eva:malloc:new] memexec-malloc.c:15: allocating variable __malloc_k_l19
[eva] Recording results for alloc
[eva] Done for function alloc
[eva] Recording results for k
@@ -45,7 +45,7 @@
[eva] computing for function alloc <- k <- main.
Called from memexec-malloc.c:19.
[eva] memexec-malloc.c:15: Call to builtin malloc
-[eva] memexec-malloc.c:15: allocating variable __malloc_k_l19_0
+[eva:malloc:new] memexec-malloc.c:15: allocating variable __malloc_k_l19_0
[eva] Recording results for alloc
[eva] Done for function alloc
[eva] Recording results for k
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index 8d3fb8dfc87..1dba7ce5413 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -121,7 +121,8 @@
[eva] computing for function memset_weak_base <- main.
Called from memset.c:115.
[eva] memset.c:101: Call to builtin malloc
-[eva] memset.c:101: allocating weak variable __malloc_w_memset_weak_base_l101
+[eva:malloc:new] memset.c:101:
+ allocating weak variable __malloc_w_memset_weak_base_l101
[eva] memset.c:106: Call to builtin memset
[eva] memset.c:106: function memset: precondition 'valid_s' got status valid.
[eva:imprecision] memset.c:106:
diff --git a/tests/builtins/oracle/memset_malloc_0.res.oracle b/tests/builtins/oracle/memset_malloc_0.res.oracle
index a9308e4c721..908321373e9 100644
--- a/tests/builtins/oracle/memset_malloc_0.res.oracle
+++ b/tests/builtins/oracle/memset_malloc_0.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
p ∈ {0}
[eva] memset_malloc_0.c:17: Call to builtin malloc
-[eva] memset_malloc_0.c:17: allocating variable __malloc_main_l17
+[eva:malloc:new] memset_malloc_0.c:17: allocating variable __malloc_main_l17
[eva] memset_malloc_0.c:18: Call to builtin memset
[eva] memset_malloc_0.c:18:
function memset: precondition 'valid_s' got status valid.
diff --git a/tests/builtins/oracle/realloc.res.oracle b/tests/builtins/oracle/realloc.res.oracle
index cedab8abdd0..69de5538416 100644
--- a/tests/builtins/oracle/realloc.res.oracle
+++ b/tests/builtins/oracle/realloc.res.oracle
@@ -7,7 +7,7 @@
[eva] computing for function main1 <- main.
Called from realloc.c:177.
[eva] realloc.c:12: Call to builtin malloc
-[eva] realloc.c:12: allocating variable __malloc_main1_l12
+[eva:malloc:new] realloc.c:12: allocating variable __malloc_main1_l12
[eva] realloc.c:15:
Frama_C_dump_each:
# cvalue:
@@ -36,7 +36,7 @@
[eva] realloc.c:16: Call to builtin realloc
[eva] realloc.c:16: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main1_l12}
-[eva] realloc.c:16: allocating variable __realloc_main1_l16
+[eva:malloc:new] realloc.c:16: allocating variable __realloc_main1_l16
[eva:malloc] realloc.c:16: strong free on bases: {__malloc_main1_l12}
[eva] realloc.c:17:
Frama_C_dump_each:
@@ -78,12 +78,12 @@
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] realloc.c:23: Call to builtin malloc
-[eva] realloc.c:23: allocating variable __malloc_main2_l23
+[eva:malloc:new] realloc.c:23: allocating variable __malloc_main2_l23
[eva:alarm] realloc.c:24: Warning: out of bounds write. assert \valid(r + i);
[eva] realloc.c:26: Call to builtin realloc
[eva] realloc.c:26: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main2_l23}
-[eva] realloc.c:26: allocating variable __realloc_main2_l26
+[eva:malloc:new] realloc.c:26: allocating variable __realloc_main2_l26
[eva:malloc] realloc.c:26: strong free on bases: {__malloc_main2_l23}
[eva] realloc.c:27:
Frama_C_dump_each:
@@ -120,9 +120,9 @@
[eva] computing for function main3 <- main.
Called from realloc.c:179.
[eva] realloc.c:32: Call to builtin malloc
-[eva] realloc.c:32: allocating variable __malloc_main3_l32
+[eva:malloc:new] realloc.c:32: allocating variable __malloc_main3_l32
[eva] realloc.c:35: Call to builtin malloc
-[eva] realloc.c:35: allocating variable __malloc_main3_l35
+[eva:malloc:new] realloc.c:35: allocating variable __malloc_main3_l35
[eva] computing for function Frama_C_interval <- main3 <- main.
Called from realloc.c:39.
[eva] realloc.c:39:
@@ -159,7 +159,7 @@
[eva] realloc.c:46: Call to builtin realloc
[eva] realloc.c:46: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main3_l32, __malloc_main3_l35}
-[eva] realloc.c:46: allocating variable __realloc_main3_l46
+[eva:malloc:new] realloc.c:46: allocating variable __realloc_main3_l46
[eva:malloc] realloc.c:46:
weak free on bases: {__malloc_main3_l32, __malloc_main3_l35}
[eva] realloc.c:48:
@@ -223,9 +223,9 @@
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] realloc.c:55: Call to builtin malloc
-[eva] realloc.c:55: allocating variable __malloc_main4_l55
+[eva:malloc:new] realloc.c:55: allocating variable __malloc_main4_l55
[eva] realloc.c:56: Call to builtin malloc
-[eva] realloc.c:56: allocating variable __malloc_main4_l56
+[eva:malloc:new] realloc.c:56: allocating variable __malloc_main4_l56
[eva:alarm] realloc.c:59: Warning: out of bounds write. assert \valid(q + i);
[eva:alarm] realloc.c:58: Warning: out of bounds write. assert \valid(p + i);
[eva] realloc.c:61:
@@ -278,12 +278,12 @@
[eva] realloc.c:67: Call to builtin realloc
[eva] realloc.c:67: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main4_l55}
-[eva] realloc.c:67: allocating variable __realloc_main4_l67
+[eva:malloc:new] realloc.c:67: allocating variable __realloc_main4_l67
[eva:malloc] realloc.c:67: strong free on bases: {__malloc_main4_l55}
[eva] realloc.c:68: Call to builtin realloc
[eva] realloc.c:68: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main4_l56}
-[eva] realloc.c:68: allocating variable __realloc_main4_l68
+[eva:malloc:new] realloc.c:68: allocating variable __realloc_main4_l68
[eva:malloc] realloc.c:68: strong free on bases: {__malloc_main4_l56}
[eva] realloc.c:69:
Frama_C_dump_each:
@@ -342,7 +342,7 @@
[eva] computing for function main5 <- main.
Called from realloc.c:181.
[eva] realloc.c:76: Call to builtin malloc
-[eva] realloc.c:76: allocating variable __malloc_main5_l76
+[eva:malloc:new] realloc.c:76: allocating variable __malloc_main5_l76
[eva] computing for function Frama_C_interval <- main5 <- main.
Called from realloc.c:78.
[eva] realloc.c:78:
@@ -377,7 +377,7 @@
[eva] realloc.c:85: Call to builtin realloc
[eva] realloc.c:85: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main5_l76}
-[eva] realloc.c:85: allocating variable __realloc_main5_l85
+[eva:malloc:new] realloc.c:85: allocating variable __realloc_main5_l85
[eva:malloc] realloc.c:85: weak free on bases: {__malloc_main5_l76}
[eva] realloc.c:86:
Frama_C_dump_each:
@@ -426,7 +426,7 @@
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] realloc.c:93: Call to builtin malloc
-[eva] realloc.c:93: allocating variable __malloc_main6_l93
+[eva:malloc:new] realloc.c:93: allocating variable __malloc_main6_l93
[eva] realloc.c:102: Frama_C_show_each: {{ &x ; &__malloc_main6_l93 + {4} }}
[eva] realloc.c:103: Call to builtin realloc
[eva:alarm] realloc.c:103: Warning:
@@ -439,11 +439,11 @@
[eva] computing for function main7 <- main.
Called from realloc.c:183.
[eva] realloc.c:110: Call to builtin malloc
-[eva] realloc.c:110: allocating variable __malloc_main7_l110
+[eva:malloc:new] realloc.c:110: allocating variable __malloc_main7_l110
[eva] realloc.c:115: Call to builtin realloc
[eva] realloc.c:115: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main7_l110}
-[eva] realloc.c:115: allocating variable __realloc_main7_l115
+[eva:malloc:new] realloc.c:115: allocating variable __realloc_main7_l115
[eva:malloc] realloc.c:115: strong free on bases: {__malloc_main7_l110}
[eva] realloc.c:116:
Frama_C_dump_each:
@@ -506,11 +506,11 @@
[eva] computing for function main8 <- main.
Called from realloc.c:184.
[eva] realloc.c:123: Call to builtin malloc
-[eva] realloc.c:123: allocating variable __malloc_main8_l123
+[eva:malloc:new] realloc.c:123: allocating variable __malloc_main8_l123
[eva] realloc.c:126: Call to builtin realloc
[eva] realloc.c:126: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main8_l123}
-[eva] realloc.c:126: allocating variable __realloc_main8_l126
+[eva:malloc:new] realloc.c:126: allocating variable __realloc_main8_l126
[eva:malloc] realloc.c:126: strong free on bases: {__malloc_main8_l123}
[eva] realloc.c:127:
Frama_C_dump_each:
@@ -544,11 +544,11 @@
[eva] computing for function main9 <- main.
Called from realloc.c:185.
[eva] realloc.c:132: Call to builtin malloc
-[eva] realloc.c:132: allocating variable __malloc_main9_l132
+[eva:malloc:new] realloc.c:132: allocating variable __malloc_main9_l132
[eva] realloc.c:135: Call to builtin realloc
[eva] realloc.c:135: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main9_l132}
-[eva] realloc.c:135: allocating variable __realloc_main9_l135
+[eva:malloc:new] realloc.c:135: allocating variable __realloc_main9_l135
[eva:malloc] realloc.c:135: strong free on bases: {__malloc_main9_l132}
[eva] realloc.c:136:
Frama_C_dump_each:
@@ -582,11 +582,11 @@
[eva] computing for function main10 <- main.
Called from realloc.c:186.
[eva] realloc.c:147: Call to builtin malloc
-[eva] realloc.c:147: allocating variable __malloc_main10_l147
+[eva:malloc:new] realloc.c:147: allocating variable __malloc_main10_l147
[eva] realloc.c:152: Call to builtin realloc
[eva] realloc.c:152: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main10_l147}
-[eva] realloc.c:152: allocating variable __realloc_main10_l152
+[eva:malloc:new] realloc.c:152: allocating variable __realloc_main10_l152
[eva:malloc] realloc.c:152: strong free on bases: {__malloc_main10_l147}
[eva] realloc.c:154: Frama_C_show_each_main10: {4}
[eva] realloc.c:155:
@@ -650,12 +650,12 @@
[eva] computing for function main11 <- main.
Called from realloc.c:187.
[eva] realloc.c:160: Call to builtin malloc
-[eva] realloc.c:160: allocating variable __malloc_main11_l160
+[eva:malloc:new] realloc.c:160: allocating variable __malloc_main11_l160
[eva] realloc.c:165: Call to builtin reallocarray
[eva] realloc.c:165:
function reallocarray: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main11_l160}
-[eva] realloc.c:165: allocating variable __realloc_main11_l165
+[eva:malloc:new] realloc.c:165: allocating variable __realloc_main11_l165
[eva:malloc] realloc.c:165: strong free on bases: {__malloc_main11_l160}
[eva] realloc.c:167: Call to builtin reallocarray
[eva] realloc.c:167:
@@ -674,7 +674,7 @@
[eva] realloc.c:171: Warning:
reallocarray out of bounds: assert(nmemb * size <= SIZE_MAX)
[eva:malloc] bases_to_realloc: {}
-[eva] realloc.c:171: allocating variable __realloc_main11_l171
+[eva:malloc:new] realloc.c:171: allocating variable __realloc_main11_l171
[eva:malloc] realloc.c:171: strong free on bases: {}
[eva] realloc.c:172: Frama_C_show_each_p: {0}
[eva] realloc.c:172: Frama_C_show_each_p: {{ &__realloc_main11_l171 }}
diff --git a/tests/builtins/oracle/realloc2.res.oracle b/tests/builtins/oracle/realloc2.res.oracle
index c5527602cfe..7858ec9b449 100644
--- a/tests/builtins/oracle/realloc2.res.oracle
+++ b/tests/builtins/oracle/realloc2.res.oracle
@@ -9,7 +9,8 @@
[eva] realloc2.c:27: Call to builtin realloc
[eva] realloc2.c:27: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {}
-[eva] realloc2.c:27: allocating variable __realloc_test_exact_null_l27
+[eva:malloc:new] realloc2.c:27:
+ allocating variable __realloc_test_exact_null_l27
[eva:malloc] realloc2.c:27: strong free on bases: {}
[eva] computing for function fill <- test_exact_null <- main.
Called from realloc2.c:28.
@@ -22,14 +23,16 @@
[eva] realloc2.c:32: Call to builtin realloc
[eva] realloc2.c:32: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {}
-[eva] realloc2.c:32: allocating variable __realloc_test_exact_null_free_l32
+[eva:malloc:new] realloc2.c:32:
+ allocating variable __realloc_test_exact_null_free_l32
[eva:malloc] realloc2.c:32: strong free on bases: {}
[eva] Recording results for test_exact_null_free
[eva] Done for function test_exact_null_free
[eva] computing for function test_exact_nonnull_expand <- main.
Called from realloc2.c:196.
[eva] realloc2.c:36: Call to builtin malloc
-[eva] realloc2.c:36: allocating variable __malloc_test_exact_nonnull_expand_l36
+[eva:malloc:new] realloc2.c:36:
+ allocating variable __malloc_test_exact_nonnull_expand_l36
[eva] computing for function fill <- test_exact_nonnull_expand <- main.
Called from realloc2.c:37.
[eva] Recording results for fill
@@ -37,7 +40,8 @@
[eva] realloc2.c:38: Call to builtin realloc
[eva] realloc2.c:38: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_exact_nonnull_expand_l36}
-[eva] realloc2.c:38: allocating variable __realloc_test_exact_nonnull_expand_l38
+[eva:malloc:new] realloc2.c:38:
+ allocating variable __realloc_test_exact_nonnull_expand_l38
[eva:malloc] realloc2.c:38:
strong free on bases: {__malloc_test_exact_nonnull_expand_l36}
[eva] computing for function fill <- test_exact_nonnull_expand <- main.
@@ -49,7 +53,8 @@
[eva] computing for function test_exact_nonnull_shrink <- main.
Called from realloc2.c:197.
[eva] realloc2.c:44: Call to builtin malloc
-[eva] realloc2.c:44: allocating variable __malloc_test_exact_nonnull_shrink_l44
+[eva:malloc:new] realloc2.c:44:
+ allocating variable __malloc_test_exact_nonnull_shrink_l44
[eva] computing for function fill <- test_exact_nonnull_shrink <- main.
Called from realloc2.c:45.
[eva] Recording results for fill
@@ -57,7 +62,8 @@
[eva] realloc2.c:46: Call to builtin realloc
[eva] realloc2.c:46: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_exact_nonnull_shrink_l44}
-[eva] realloc2.c:46: allocating variable __realloc_test_exact_nonnull_shrink_l46
+[eva:malloc:new] realloc2.c:46:
+ allocating variable __realloc_test_exact_nonnull_shrink_l46
[eva:malloc] realloc2.c:46:
strong free on bases: {__malloc_test_exact_nonnull_shrink_l44}
[eva] computing for function fill <- test_exact_nonnull_shrink <- main.
@@ -69,7 +75,8 @@
[eva] computing for function test_exact_nonnull_free <- main.
Called from realloc2.c:198.
[eva] realloc2.c:51: Call to builtin malloc
-[eva] realloc2.c:51: allocating variable __malloc_test_exact_nonnull_free_l51
+[eva:malloc:new] realloc2.c:51:
+ allocating variable __malloc_test_exact_nonnull_free_l51
[eva] computing for function fill <- test_exact_nonnull_free <- main.
Called from realloc2.c:52.
[eva] Recording results for fill
@@ -77,7 +84,8 @@
[eva] realloc2.c:53: Call to builtin realloc
[eva] realloc2.c:53: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_exact_nonnull_free_l51}
-[eva] realloc2.c:53: allocating variable __realloc_test_exact_nonnull_free_l53
+[eva:malloc:new] realloc2.c:53:
+ allocating variable __realloc_test_exact_nonnull_free_l53
[eva:malloc] realloc2.c:53:
strong free on bases: {__malloc_test_exact_nonnull_free_l51}
[eva] Recording results for test_exact_nonnull_free
@@ -85,11 +93,13 @@
[eva] computing for function test_maybe_nonnull <- main.
Called from realloc2.c:199.
[eva] realloc2.c:57: Call to builtin malloc
-[eva] realloc2.c:57: allocating variable __malloc_test_maybe_nonnull_l57
+[eva:malloc:new] realloc2.c:57:
+ allocating variable __malloc_test_maybe_nonnull_l57
[eva] realloc2.c:58: Call to builtin realloc
[eva] realloc2.c:58: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_maybe_nonnull_l57}
-[eva] realloc2.c:58: allocating variable __realloc_test_maybe_nonnull_l58
+[eva:malloc:new] realloc2.c:58:
+ allocating variable __realloc_test_maybe_nonnull_l58
[eva:malloc] realloc2.c:58:
weak free on bases: {__malloc_test_maybe_nonnull_l57}
[eva] computing for function fill <- test_maybe_nonnull <- main.
@@ -101,7 +111,7 @@
[eva] computing for function test_same_size <- main.
Called from realloc2.c:200.
[eva] realloc2.c:63: Call to builtin malloc
-[eva] realloc2.c:63: allocating variable __malloc_test_same_size_l63
+[eva:malloc:new] realloc2.c:63: allocating variable __malloc_test_same_size_l63
[eva] computing for function fill <- test_same_size <- main.
Called from realloc2.c:64.
[eva] Recording results for fill
@@ -109,7 +119,7 @@
[eva] realloc2.c:65: Call to builtin realloc
[eva] realloc2.c:65: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_same_size_l63}
-[eva] realloc2.c:65: allocating variable __realloc_test_same_size_l65
+[eva:malloc:new] realloc2.c:65: allocating variable __realloc_test_same_size_l65
[eva:malloc] realloc2.c:65: strong free on bases: {__malloc_test_same_size_l63}
[eva] Recording results for test_same_size
[eva] Done for function test_same_size
@@ -118,7 +128,8 @@
[eva] realloc2.c:70: Call to builtin realloc
[eva] realloc2.c:70: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {}
-[eva] realloc2.c:70: allocating variable __realloc_test_imprecise_size_l70
+[eva:malloc:new] realloc2.c:70:
+ allocating variable __realloc_test_imprecise_size_l70
[eva:malloc] realloc2.c:70: strong free on bases: {}
[eva] computing for function fill <- test_imprecise_size <- main.
Called from realloc2.c:71.
@@ -132,7 +143,7 @@
[eva] realloc2.c:76: Call to builtin realloc
[eva] realloc2.c:76: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {}
-[eva] realloc2.c:76:
+[eva:malloc:new] realloc2.c:76:
allocating variable __realloc_test_imprecise_size_but_precise_fill_l76
[eva:malloc] realloc2.c:76: strong free on bases: {}
[eva] computing for function fill <- test_imprecise_size_but_precise_fill <- main.
@@ -144,7 +155,8 @@
[eva] computing for function test_imprecise_size_free <- main.
Called from realloc2.c:203.
[eva] realloc2.c:81: Call to builtin malloc
-[eva] realloc2.c:81: allocating variable __malloc_test_imprecise_size_free_l81
+[eva:malloc:new] realloc2.c:81:
+ allocating variable __malloc_test_imprecise_size_free_l81
[eva] computing for function fill <- test_imprecise_size_free <- main.
Called from realloc2.c:82.
[eva] Recording results for fill
@@ -152,7 +164,8 @@
[eva] realloc2.c:84: Call to builtin realloc
[eva] realloc2.c:84: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_imprecise_size_free_l81}
-[eva] realloc2.c:84: allocating variable __realloc_test_imprecise_size_free_l84
+[eva:malloc:new] realloc2.c:84:
+ allocating variable __realloc_test_imprecise_size_free_l84
[eva:malloc] realloc2.c:84:
strong free on bases: {__malloc_test_imprecise_size_free_l81}
[eva] computing for function fill <- test_imprecise_size_free <- main.
@@ -164,11 +177,13 @@
[eva] computing for function test_imprecise_both <- main.
Called from realloc2.c:204.
[eva] realloc2.c:89: Call to builtin malloc
-[eva] realloc2.c:89: allocating variable __malloc_test_imprecise_both_l89
+[eva:malloc:new] realloc2.c:89:
+ allocating variable __malloc_test_imprecise_both_l89
[eva] realloc2.c:91: Call to builtin realloc
[eva] realloc2.c:91: function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_imprecise_both_l89}
-[eva] realloc2.c:91: allocating variable __realloc_test_imprecise_both_l91
+[eva:malloc:new] realloc2.c:91:
+ allocating variable __realloc_test_imprecise_both_l91
[eva:malloc] realloc2.c:91:
weak free on bases: {__malloc_test_imprecise_both_l89}
[eva] computing for function fill <- test_imprecise_both <- main.
@@ -180,13 +195,13 @@
[eva] computing for function test_possibly_invalid_realloc <- main.
Called from realloc2.c:205.
[eva] realloc2.c:96: Call to builtin malloc
-[eva] realloc2.c:96:
+[eva:malloc:new] realloc2.c:96:
allocating variable __malloc_test_possibly_invalid_realloc_l96
[eva] realloc2.c:99: Call to builtin realloc
[eva:alarm] realloc2.c:99: Warning:
function realloc: precondition 'freeable' got status unknown.
[eva:malloc] bases_to_realloc: {__malloc_test_possibly_invalid_realloc_l96}
-[eva] realloc2.c:99:
+[eva:malloc:new] realloc2.c:99:
allocating variable __realloc_test_possibly_invalid_realloc_l99
[eva:malloc] realloc2.c:99:
strong free on bases: {__malloc_test_possibly_invalid_realloc_l96}
@@ -199,7 +214,8 @@
[eva] computing for function test_invalid_realloc <- main.
Called from realloc2.c:206.
[eva] realloc2.c:104: Call to builtin malloc
-[eva] realloc2.c:104: allocating variable __malloc_test_invalid_realloc_l104
+[eva:malloc:new] realloc2.c:104:
+ allocating variable __malloc_test_invalid_realloc_l104
[eva] realloc2.c:106: Call to builtin realloc
[eva:alarm] realloc2.c:106: Warning:
function realloc: precondition 'freeable' got status invalid.
@@ -215,7 +231,8 @@
[eva] computing for function test_invalid_realloc3 <- main.
Called from realloc2.c:208.
[eva] realloc2.c:116: Call to builtin malloc
-[eva] realloc2.c:116: allocating variable __malloc_test_invalid_realloc3_l116
+[eva:malloc:new] realloc2.c:116:
+ allocating variable __malloc_test_invalid_realloc3_l116
[eva] realloc2.c:119: Call to builtin realloc
[eva:alarm] realloc2.c:119: Warning:
function realloc: precondition 'freeable' got status invalid.
@@ -224,19 +241,22 @@
[eva] computing for function test_realloc_sequence <- main.
Called from realloc2.c:209.
[eva] realloc2.c:124: Call to builtin malloc
-[eva] realloc2.c:124: allocating variable __malloc_test_realloc_sequence_l124
+[eva:malloc:new] realloc2.c:124:
+ allocating variable __malloc_test_realloc_sequence_l124
[eva] realloc2.c:125: Call to builtin realloc
[eva] realloc2.c:125:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_realloc_sequence_l124}
-[eva] realloc2.c:125: allocating variable __realloc_test_realloc_sequence_l125
+[eva:malloc:new] realloc2.c:125:
+ allocating variable __realloc_test_realloc_sequence_l125
[eva:malloc] realloc2.c:125:
strong free on bases: {__malloc_test_realloc_sequence_l124}
[eva] realloc2.c:126: Call to builtin realloc
[eva] realloc2.c:126:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__realloc_test_realloc_sequence_l125}
-[eva] realloc2.c:126: allocating variable __realloc_test_realloc_sequence_l126
+[eva:malloc:new] realloc2.c:126:
+ allocating variable __realloc_test_realloc_sequence_l126
[eva:malloc] realloc2.c:126:
strong free on bases: {__realloc_test_realloc_sequence_l125}
[eva] computing for function fill <- test_realloc_sequence <- main.
@@ -248,7 +268,8 @@
[eva] computing for function test_realloc_loop <- main.
Called from realloc2.c:210.
[eva] realloc2.c:131: Call to builtin malloc
-[eva] realloc2.c:131: allocating variable __malloc_test_realloc_loop_l131
+[eva:malloc:new] realloc2.c:131:
+ allocating variable __malloc_test_realloc_loop_l131
[eva] computing for function fill <- test_realloc_loop <- main.
Called from realloc2.c:134.
[eva] Recording results for fill
@@ -257,7 +278,8 @@
[eva] realloc2.c:138:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_realloc_loop_l131}
-[eva] realloc2.c:138: allocating variable __realloc_test_realloc_loop_l138
+[eva:malloc:new] realloc2.c:138:
+ allocating variable __realloc_test_realloc_loop_l138
[eva:malloc] realloc2.c:138:
strong free on bases: {__malloc_test_realloc_loop_l131}
[eva] computing for function fill <- test_realloc_loop <- main.
@@ -314,16 +336,16 @@
[eva] computing for function test_realloc_multiple_bases <- main.
Called from realloc2.c:211.
[eva] realloc2.c:151: Call to builtin malloc
-[eva] realloc2.c:151:
+[eva:malloc:new] realloc2.c:151:
allocating variable __malloc_test_realloc_multiple_bases_l151
[eva] realloc2.c:154: Call to builtin malloc
-[eva] realloc2.c:154:
+[eva:malloc:new] realloc2.c:154:
allocating variable __malloc_test_realloc_multiple_bases_l154
[eva] realloc2.c:156: Call to builtin realloc
[eva] realloc2.c:156:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_realloc_multiple_bases_l151}
-[eva] realloc2.c:156:
+[eva:malloc:new] realloc2.c:156:
allocating variable __realloc_test_realloc_multiple_bases_l156
[eva:malloc] realloc2.c:156:
strong free on bases: {__malloc_test_realloc_multiple_bases_l151}
@@ -333,7 +355,7 @@
[eva:malloc]
bases_to_realloc: {__malloc_test_realloc_multiple_bases_l154,
__realloc_test_realloc_multiple_bases_l156}
-[eva] realloc2.c:158:
+[eva:malloc:new] realloc2.c:158:
allocating variable __realloc_test_realloc_multiple_bases_l158
[eva:malloc] realloc2.c:158:
weak free on bases: {__malloc_test_realloc_multiple_bases_l154,
@@ -347,7 +369,7 @@
[eva] computing for function test_realloc_multiple_bases2 <- main.
Called from realloc2.c:212.
[eva] realloc2.c:163: Call to builtin malloc
-[eva] realloc2.c:163:
+[eva:malloc:new] realloc2.c:163:
allocating variable __malloc_test_realloc_multiple_bases2_l163
[eva] computing for function fill <- test_realloc_multiple_bases2 <- main.
Called from realloc2.c:165.
@@ -357,12 +379,12 @@
[eva] realloc2.c:166:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_realloc_multiple_bases2_l163}
-[eva] realloc2.c:166:
+[eva:malloc:new] realloc2.c:166:
allocating variable __realloc_test_realloc_multiple_bases2_l166
[eva:malloc] realloc2.c:166:
strong free on bases: {__malloc_test_realloc_multiple_bases2_l163}
[eva] realloc2.c:166: Call to builtin malloc
-[eva] realloc2.c:166:
+[eva:malloc:new] realloc2.c:166:
allocating variable __malloc_test_realloc_multiple_bases2_l166
[eva] computing for function fill2 <- test_realloc_multiple_bases2 <- main.
Called from realloc2.c:168.
@@ -374,7 +396,7 @@
[eva:malloc]
bases_to_realloc: {__realloc_test_realloc_multiple_bases2_l166,
__malloc_test_realloc_multiple_bases2_l166}
-[eva] realloc2.c:169:
+[eva:malloc:new] realloc2.c:169:
allocating variable __realloc_test_realloc_multiple_bases2_l169
[eva:malloc] realloc2.c:169:
weak free on bases: {__realloc_test_realloc_multiple_bases2_l166,
@@ -383,7 +405,7 @@
[eva] realloc2.c:171:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__realloc_test_realloc_multiple_bases2_l169}
-[eva] realloc2.c:171:
+[eva:malloc:new] realloc2.c:171:
allocating variable __realloc_test_realloc_multiple_bases2_l171
[eva:malloc] realloc2.c:171:
strong free on bases: {__realloc_test_realloc_multiple_bases2_l169}
@@ -392,7 +414,7 @@
[eva] Recording results for fill
[eva] Done for function fill
[eva] realloc2.c:174: Call to builtin malloc
-[eva] realloc2.c:174:
+[eva:malloc:new] realloc2.c:174:
allocating variable __malloc_test_realloc_multiple_bases2_l174
[eva] computing for function fill2 <- test_realloc_multiple_bases2 <- main.
Called from realloc2.c:176.
@@ -404,7 +426,7 @@
[eva:malloc]
bases_to_realloc: {__realloc_test_realloc_multiple_bases2_l171,
__malloc_test_realloc_multiple_bases2_l174}
-[eva] realloc2.c:177:
+[eva:malloc:new] realloc2.c:177:
allocating variable __realloc_test_realloc_multiple_bases2_l177
[eva:malloc] realloc2.c:177:
weak free on bases: {__realloc_test_realloc_multiple_bases2_l171,
@@ -418,13 +440,13 @@
[eva] computing for function test_realloc_multiple_bases_loop <- main.
Called from realloc2.c:213.
[eva] realloc2.c:184: Call to builtin malloc
-[eva] realloc2.c:184:
+[eva:malloc:new] realloc2.c:184:
allocating variable __malloc_test_realloc_multiple_bases_loop_l184
[eva] realloc2.c:187: Call to builtin realloc
[eva] realloc2.c:187:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_test_realloc_multiple_bases_loop_l184}
-[eva] realloc2.c:187:
+[eva:malloc:new] realloc2.c:187:
allocating variable __realloc_test_realloc_multiple_bases_loop_l187
[eva:malloc] realloc2.c:187:
strong free on bases: {__malloc_test_realloc_multiple_bases_loop_l184}
diff --git a/tests/builtins/oracle/realloc_multiple.0.res.oracle b/tests/builtins/oracle/realloc_multiple.0.res.oracle
index fb44822b047..f03e0d480af 100644
--- a/tests/builtins/oracle/realloc_multiple.0.res.oracle
+++ b/tests/builtins/oracle/realloc_multiple.0.res.oracle
@@ -7,9 +7,9 @@
[eva] computing for function main1 <- main.
Called from realloc_multiple.c:75.
[eva] realloc_multiple.c:9: Call to builtin malloc
-[eva] realloc_multiple.c:9: allocating variable __malloc_main1_l9
+[eva:malloc:new] realloc_multiple.c:9: allocating variable __malloc_main1_l9
[eva] realloc_multiple.c:12: Call to builtin malloc
-[eva] realloc_multiple.c:12: allocating variable __malloc_main1_l12
+[eva:malloc:new] realloc_multiple.c:12: allocating variable __malloc_main1_l12
[eva] computing for function Frama_C_interval <- main1 <- main.
Called from realloc_multiple.c:16.
[eva] using specification for function Frama_C_interval
@@ -48,9 +48,10 @@
[eva] realloc_multiple.c:23:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main1_l12}
-[eva] realloc_multiple.c:23: allocating variable __realloc_main1_l23
+[eva:malloc:new] realloc_multiple.c:23: allocating variable __realloc_main1_l23
[eva:malloc] bases_to_realloc: {__malloc_main1_l9}
-[eva] realloc_multiple.c:23: allocating variable __realloc_main1_l23_0
+[eva:malloc:new] realloc_multiple.c:23:
+ allocating variable __realloc_main1_l23_0
[eva:malloc] realloc_multiple.c:23:
weak free on bases: {__malloc_main1_l9, __malloc_main1_l12}
[eva] realloc_multiple.c:25:
@@ -95,9 +96,9 @@
[eva] computing for function main2 <- main.
Called from realloc_multiple.c:76.
[eva] realloc_multiple.c:30: Call to builtin malloc
-[eva] realloc_multiple.c:30: allocating variable __malloc_main2_l30
+[eva:malloc:new] realloc_multiple.c:30: allocating variable __malloc_main2_l30
[eva] realloc_multiple.c:33: Call to builtin malloc
-[eva] realloc_multiple.c:33: allocating variable __malloc_main2_l33
+[eva:malloc:new] realloc_multiple.c:33: allocating variable __malloc_main2_l33
[eva] computing for function Frama_C_interval <- main2 <- main.
Called from realloc_multiple.c:37.
[eva] realloc_multiple.c:37:
@@ -135,11 +136,13 @@
[eva] realloc_multiple.c:45:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main2_l33}
-[eva] realloc_multiple.c:45: allocating variable __realloc_main2_l45
+[eva:malloc:new] realloc_multiple.c:45: allocating variable __realloc_main2_l45
[eva:malloc] bases_to_realloc: {__malloc_main2_l30}
-[eva] realloc_multiple.c:45: allocating variable __realloc_main2_l45_0
+[eva:malloc:new] realloc_multiple.c:45:
+ allocating variable __realloc_main2_l45_0
[eva:malloc] bases_to_realloc: {}
-[eva] realloc_multiple.c:45: allocating variable __realloc_main2_l45_1
+[eva:malloc:new] realloc_multiple.c:45:
+ allocating variable __realloc_main2_l45_1
[eva:malloc] realloc_multiple.c:45:
weak free on bases: {__malloc_main2_l30, __malloc_main2_l33}
[eva] realloc_multiple.c:47:
@@ -189,9 +192,9 @@
[eva] computing for function main3 <- main.
Called from realloc_multiple.c:77.
[eva] realloc_multiple.c:52: Call to builtin malloc
-[eva] realloc_multiple.c:52: allocating variable __malloc_main3_l52
+[eva:malloc:new] realloc_multiple.c:52: allocating variable __malloc_main3_l52
[eva] realloc_multiple.c:53: Call to builtin malloc
-[eva] realloc_multiple.c:53: allocating variable __malloc_main3_l53
+[eva:malloc:new] realloc_multiple.c:53: allocating variable __malloc_main3_l53
[eva] computing for function Frama_C_interval <- main3 <- main.
Called from realloc_multiple.c:59.
[eva] realloc_multiple.c:59:
@@ -231,11 +234,13 @@
[eva] realloc_multiple.c:65:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main3_l53}
-[eva] realloc_multiple.c:65: allocating variable __realloc_main3_l65
+[eva:malloc:new] realloc_multiple.c:65: allocating variable __realloc_main3_l65
[eva:malloc] bases_to_realloc: {__malloc_main3_l52}
-[eva] realloc_multiple.c:65: allocating variable __realloc_main3_l65_0
+[eva:malloc:new] realloc_multiple.c:65:
+ allocating variable __realloc_main3_l65_0
[eva:malloc] bases_to_realloc: {}
-[eva] realloc_multiple.c:65: allocating variable __realloc_main3_l65_1
+[eva:malloc:new] realloc_multiple.c:65:
+ allocating variable __realloc_main3_l65_1
[eva:malloc] realloc_multiple.c:65:
weak free on bases: {__malloc_main3_l52, __malloc_main3_l53}
[eva:alarm] realloc_multiple.c:66: Warning:
diff --git a/tests/builtins/oracle/realloc_multiple.1.res.oracle b/tests/builtins/oracle/realloc_multiple.1.res.oracle
index c076efb3a39..3574b221894 100644
--- a/tests/builtins/oracle/realloc_multiple.1.res.oracle
+++ b/tests/builtins/oracle/realloc_multiple.1.res.oracle
@@ -7,13 +7,13 @@
[eva] computing for function main1 <- main.
Called from realloc_multiple.c:75.
[eva] realloc_multiple.c:9: Call to builtin malloc
-[eva] realloc_multiple.c:9: allocating variable __malloc_main1_l9
+[eva:malloc:new] realloc_multiple.c:9: allocating variable __malloc_main1_l9
[eva:alarm] realloc_multiple.c:10: Warning:
out of bounds write. assert \valid(q + i);
[kernel] realloc_multiple.c:10: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] realloc_multiple.c:12: Call to builtin malloc
-[eva] realloc_multiple.c:12: allocating variable __malloc_main1_l12
+[eva:malloc:new] realloc_multiple.c:12: allocating variable __malloc_main1_l12
[eva:alarm] realloc_multiple.c:13: Warning:
out of bounds write. assert \valid(r + i_0);
[kernel] realloc_multiple.c:13: Warning:
@@ -56,9 +56,10 @@
[eva] realloc_multiple.c:23:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main1_l12}
-[eva] realloc_multiple.c:23: allocating variable __realloc_main1_l23
+[eva:malloc:new] realloc_multiple.c:23: allocating variable __realloc_main1_l23
[eva:malloc] bases_to_realloc: {__malloc_main1_l9}
-[eva] realloc_multiple.c:23: allocating variable __realloc_main1_l23_0
+[eva:malloc:new] realloc_multiple.c:23:
+ allocating variable __realloc_main1_l23_0
[eva:malloc] realloc_multiple.c:23:
weak free on bases: {__malloc_main1_l9, __malloc_main1_l12}
[eva] realloc_multiple.c:25:
@@ -133,13 +134,13 @@
[eva] computing for function main2 <- main.
Called from realloc_multiple.c:76.
[eva] realloc_multiple.c:30: Call to builtin malloc
-[eva] realloc_multiple.c:30: allocating variable __malloc_main2_l30
+[eva:malloc:new] realloc_multiple.c:30: allocating variable __malloc_main2_l30
[eva:alarm] realloc_multiple.c:31: Warning:
out of bounds write. assert \valid(q + i);
[kernel] realloc_multiple.c:31: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] realloc_multiple.c:33: Call to builtin malloc
-[eva] realloc_multiple.c:33: allocating variable __malloc_main2_l33
+[eva:malloc:new] realloc_multiple.c:33: allocating variable __malloc_main2_l33
[eva:alarm] realloc_multiple.c:34: Warning:
out of bounds write. assert \valid(r + i_0);
[kernel] realloc_multiple.c:34: Warning:
@@ -181,11 +182,13 @@
[eva] realloc_multiple.c:45:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main2_l33}
-[eva] realloc_multiple.c:45: allocating variable __realloc_main2_l45
+[eva:malloc:new] realloc_multiple.c:45: allocating variable __realloc_main2_l45
[eva:malloc] bases_to_realloc: {__malloc_main2_l30}
-[eva] realloc_multiple.c:45: allocating variable __realloc_main2_l45_0
+[eva:malloc:new] realloc_multiple.c:45:
+ allocating variable __realloc_main2_l45_0
[eva:malloc] bases_to_realloc: {}
-[eva] realloc_multiple.c:45: allocating variable __realloc_main2_l45_1
+[eva:malloc:new] realloc_multiple.c:45:
+ allocating variable __realloc_main2_l45_1
[eva:malloc] realloc_multiple.c:45:
weak free on bases: {__malloc_main2_l30, __malloc_main2_l33}
[eva] realloc_multiple.c:47:
@@ -265,11 +268,11 @@
[eva] computing for function main3 <- main.
Called from realloc_multiple.c:77.
[eva] realloc_multiple.c:52: Call to builtin malloc
-[eva] realloc_multiple.c:52: allocating variable __malloc_main3_l52
+[eva:malloc:new] realloc_multiple.c:52: allocating variable __malloc_main3_l52
[eva] realloc_multiple.c:53: Call to builtin malloc
-[eva] realloc_multiple.c:53: allocating variable __malloc_main3_l53
+[eva:malloc:new] realloc_multiple.c:53: allocating variable __malloc_main3_l53
[eva] realloc_multiple.c:53: Call to builtin malloc
-[eva] realloc_multiple.c:53: allocating variable __malloc_main3_l53_0
+[eva:malloc:new] realloc_multiple.c:53: allocating variable __malloc_main3_l53_0
[eva:alarm] realloc_multiple.c:57: Warning:
out of bounds write. assert \valid(p);
[kernel] realloc_multiple.c:57: Warning:
@@ -317,11 +320,13 @@
[eva] realloc_multiple.c:65:
function realloc: precondition 'freeable' got status valid.
[eva:malloc] bases_to_realloc: {__malloc_main3_l53}
-[eva] realloc_multiple.c:65: allocating variable __realloc_main3_l65
+[eva:malloc:new] realloc_multiple.c:65: allocating variable __realloc_main3_l65
[eva:malloc] bases_to_realloc: {__malloc_main3_l52}
-[eva] realloc_multiple.c:65: allocating variable __realloc_main3_l65_0
+[eva:malloc:new] realloc_multiple.c:65:
+ allocating variable __realloc_main3_l65_0
[eva:malloc] bases_to_realloc: {}
-[eva] realloc_multiple.c:65: allocating variable __realloc_main3_l65_1
+[eva:malloc:new] realloc_multiple.c:65:
+ allocating variable __realloc_main3_l65_1
[eva:malloc] realloc_multiple.c:65:
weak free on bases: {__malloc_main3_l52, __malloc_main3_l53}
[eva:alarm] realloc_multiple.c:66: Warning:
diff --git a/tests/builtins/oracle/str_allocated.res.oracle b/tests/builtins/oracle/str_allocated.res.oracle
index cdd369361be..4aec51e154f 100644
--- a/tests/builtins/oracle/str_allocated.res.oracle
+++ b/tests/builtins/oracle/str_allocated.res.oracle
@@ -7,7 +7,7 @@
[eva] computing for function memchr_bug <- main.
Called from str_allocated.c:19.
[eva] str_allocated.c:12: Call to builtin malloc
-[eva] str_allocated.c:12: allocating variable __malloc_memchr_bug_l12
+[eva:malloc:new] str_allocated.c:12: allocating variable __malloc_memchr_bug_l12
[eva] str_allocated.c:11: starting to merge loop iterations
[eva] str_allocated.c:12: Call to builtin malloc
[eva:malloc:weak] str_allocated.c:12:
diff --git a/tests/builtins/oracle/vla.res.oracle b/tests/builtins/oracle/vla.res.oracle
index 1757cd12649..a35b15624db 100644
--- a/tests/builtins/oracle/vla.res.oracle
+++ b/tests/builtins/oracle/vla.res.oracle
@@ -8,13 +8,13 @@
Called from vla.c:20.
[eva] vla.c:6: assertion 'alloca_bounds' got status valid.
[eva] vla.c:6: Call to builtin __fc_vla_alloc
-[eva] vla.c:6: allocating variable __malloc_f_l6
+[eva:malloc:new] vla.c:6: allocating variable __malloc_f_l6
[eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
[eva] vla.c:6: Call to builtin __fc_vla_free
[eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
[eva] Recording results for f
[eva] Done for function f
-[eva] vla.c:20: freeing automatic bases: {__malloc_f_l6}
+[eva:malloc:automatic-free] vla.c:20: freeing automatic bases: {__malloc_f_l6}
[eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
[eva] computing for function f <- main.
Called from vla.c:20.
diff --git a/tests/libc/oracle/alloca_h.res.oracle b/tests/libc/oracle/alloca_h.res.oracle
index 53701c99c81..78d3f338143 100644
--- a/tests/libc/oracle/alloca_h.res.oracle
+++ b/tests/libc/oracle/alloca_h.res.oracle
@@ -5,17 +5,17 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] alloca_h.c:30: Call to builtin alloca
-[eva] alloca_h.c:30: allocating variable __alloca_main_l30
+[eva:malloc:new] alloca_h.c:30: allocating variable __alloca_main_l30
[eva] alloca_h.c:31: assertion got status valid.
[eva] alloca_h.c:35: Call to builtin alloca
-[eva] alloca_h.c:35: allocating variable __alloca_main_l35
+[eva:malloc:new] alloca_h.c:35: allocating variable __alloca_main_l35
[eva] alloca_h.c:40: assertion got status valid.
[eva] computing for function f <- main.
Called from alloca_h.c:41.
[eva] alloca_h.c:6: Call to builtin alloca
-[eva] alloca_h.c:6: allocating variable __alloca_f_l6
+[eva:malloc:new] alloca_h.c:6: allocating variable __alloca_f_l6
[eva] alloca_h.c:7: Call to builtin malloc
-[eva] alloca_h.c:7: allocating variable __malloc_f_l7
+[eva:malloc:new] alloca_h.c:7: allocating variable __malloc_f_l7
[eva] alloca_h.c:9: Call to builtin free
[eva:alarm] alloca_h.c:9: Warning:
function free: precondition 'freeable' got status unknown.
@@ -24,12 +24,13 @@
assert ¬\dangling(&p);
[eva] Recording results for f
[eva] Done for function f
-[eva] alloca_h.c:41: freeing automatic bases: {__alloca_f_l6}
+[eva:malloc:automatic-free] alloca_h.c:41:
+ freeing automatic bases: {__alloca_f_l6}
[eva] alloca_h.c:42: assertion got status valid.
[eva] computing for function loop <- main.
Called from alloca_h.c:43.
[eva] alloca_h.c:23: Call to builtin alloca
-[eva] alloca_h.c:23: allocating variable __alloca_loop_l23
+[eva:malloc:new] alloca_h.c:23: allocating variable __alloca_loop_l23
[eva] alloca_h.c:22: starting to merge loop iterations
[eva] alloca_h.c:23: Call to builtin alloca
[eva] alloca_h.c:23: Call to builtin alloca
@@ -37,17 +38,19 @@
[eva] alloca_h.c:23: Call to builtin alloca
[eva] Recording results for loop
[eva] Done for function loop
-[eva] alloca_h.c:43: freeing automatic bases: {__alloca_w_loop_l23}
+[eva:malloc:automatic-free] alloca_h.c:43:
+ freeing automatic bases: {__alloca_w_loop_l23}
[eva:alarm] alloca_h.c:44: Warning: assertion got status unknown.
[eva] alloca_h.c:45: Call to builtin alloca
-[eva] alloca_h.c:45: allocating variable __alloca_main_l45
+[eva:malloc:new] alloca_h.c:45: allocating variable __alloca_main_l45
[eva] computing for function f2 <- main.
Called from alloca_h.c:46.
[eva] alloca_h.c:16: Call to builtin alloca
-[eva] alloca_h.c:16: allocating variable __alloca_f2_l16
+[eva:malloc:new] alloca_h.c:16: allocating variable __alloca_f2_l16
[eva] Recording results for f2
[eva] Done for function f2
-[eva] alloca_h.c:46: freeing automatic bases: {__alloca_f2_l16}
+[eva:malloc:automatic-free] alloca_h.c:46:
+ freeing automatic bases: {__alloca_f2_l16}
[eva] alloca_h.c:48: assertion got status valid.
[eva] Recording results for main
[eva] Done for function main
diff --git a/tests/libc/oracle/argz_c.res.oracle b/tests/libc/oracle/argz_c.res.oracle
index ddbc94e0adf..422ded4c991 100644
--- a/tests/libc/oracle/argz_c.res.oracle
+++ b/tests/libc/oracle/argz_c.res.oracle
@@ -75,7 +75,7 @@
[eva] FRAMAC_SHARE/libc/argz.c:246: Call to builtin strlen
[eva] FRAMAC_SHARE/libc/argz.c:246: Call to builtin strlen
[eva] FRAMAC_SHARE/libc/argz.c:251: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/argz.c:251:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:251:
allocating variable __malloc_argz_create_l251
[eva] computing for function stpcpy <- argz_create <- main.
Called from FRAMAC_SHARE/libc/argz.c:256.
@@ -100,7 +100,7 @@
[eva] FRAMAC_SHARE/libc/argz.c:202:
function strlen: precondition 'valid_string_s' got status valid.
[eva] FRAMAC_SHARE/libc/argz.c:208: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/argz.c:208:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:208:
allocating variable __malloc_argz_create_sep_l208
[eva] Recording results for argz_create_sep
[eva] Done for function argz_create_sep
@@ -134,7 +134,7 @@
[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
[eva] FRAMAC_SHARE/libc/argz.c:277:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:277:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:277:
allocating variable __realloc_argz_append_l277
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] FRAMAC_SHARE/libc/argz.c:279:
@@ -162,7 +162,7 @@
[eva] FRAMAC_SHARE/libc/argz.c:299: Call to builtin realloc
[eva] FRAMAC_SHARE/libc/argz.c:299:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:299:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:299:
allocating variable __realloc_argz_add_sep_l299
[eva] Recording results for argz_add_sep
[eva] Done for function argz_add_sep
@@ -189,7 +189,7 @@
[eva] computing for function argz_append <- main.
Called from argz_c.c:38.
[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:277:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:277:
allocating variable __realloc_argz_append_l277_0
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
@@ -205,7 +205,7 @@
[eva] computing for function argz_append <- argz_add <- main.
Called from FRAMAC_SHARE/libc/argz.c:288.
[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:277:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:277:
allocating variable __realloc_argz_append_l277_1
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
@@ -268,7 +268,8 @@
Called from FRAMAC_SHARE/libc/argz.c:85.
[eva:loop-unroll:auto] FRAMAC_SHARE/libc/string.c:347: Automatic loop unrolling.
[eva] FRAMAC_SHARE/libc/string.c:350: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/string.c:350: allocating variable __malloc_strndup_l350
+[eva:malloc:new] FRAMAC_SHARE/libc/string.c:350:
+ allocating variable __malloc_strndup_l350
[eva] FRAMAC_SHARE/libc/string.c:355: Call to builtin memcpy
[eva] FRAMAC_SHARE/libc/string.c:355:
function memcpy: precondition 'valid_dest' got status valid.
@@ -283,7 +284,8 @@
[eva] FRAMAC_SHARE/libc/argz.c:55: Call to builtin realloc
[eva] FRAMAC_SHARE/libc/argz.c:55:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:55: allocating variable __realloc_str_append_l55
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:55:
+ allocating variable __realloc_str_append_l55
[eva] computing for function mempcpy <- str_append <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:58.
[eva:loop-unroll:auto] FRAMAC_SHARE/libc/string.c:54: Automatic loop unrolling.
@@ -304,7 +306,7 @@
[eva] computing for function str_append <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:95.
[eva] FRAMAC_SHARE/libc/argz.c:55: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:55:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:55:
allocating variable __realloc_str_append_l55_0
[eva] computing for function mempcpy <- str_append <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:58.
@@ -316,7 +318,7 @@
[eva] computing for function argz_append <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:104.
[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:277:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:277:
allocating variable __realloc_argz_append_l277_2
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
@@ -327,7 +329,7 @@
[eva] computing for function argz_append <- argz_add <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:288.
[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:277:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:277:
allocating variable __realloc_argz_append_l277_3
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
@@ -354,7 +356,7 @@
[eva] computing for function argz_append <- argz_add <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:288.
[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:277:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:277:
allocating variable __realloc_argz_append_l277_4
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
@@ -376,7 +378,7 @@
[eva] computing for function argz_append <- argz_add <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:288.
[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:277:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:277:
allocating variable __realloc_argz_append_l277_5
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
@@ -398,7 +400,7 @@
[eva] computing for function argz_append <- argz_add <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:288.
[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:277:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:277:
allocating variable __realloc_argz_append_l277_6
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
@@ -417,7 +419,7 @@
[eva] computing for function strndup <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:85.
[eva] FRAMAC_SHARE/libc/string.c:350: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/string.c:350:
+[eva:malloc:new] FRAMAC_SHARE/libc/string.c:350:
allocating variable __malloc_strndup_l350_0
[eva] FRAMAC_SHARE/libc/string.c:355: Call to builtin memcpy
[eva] Recording results for strndup
@@ -425,7 +427,7 @@
[eva] computing for function str_append <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:88.
[eva] FRAMAC_SHARE/libc/argz.c:55: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:55:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:55:
allocating variable __realloc_str_append_l55_1
[eva] computing for function mempcpy <- str_append <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:58.
@@ -442,7 +444,7 @@
[eva] computing for function str_append <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:95.
[eva] FRAMAC_SHARE/libc/argz.c:55: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:55:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:55:
allocating variable __realloc_str_append_l55_2
[eva] computing for function mempcpy <- str_append <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:58.
@@ -457,7 +459,7 @@
[eva] computing for function argz_append <- argz_add <- argz_replace <- main.
Called from FRAMAC_SHARE/libc/argz.c:288.
[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:277:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:277:
allocating variable __realloc_argz_append_l277_7
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
@@ -569,7 +571,7 @@
[eva] FRAMAC_SHARE/libc/argz.c:163: Call to builtin realloc
[eva] FRAMAC_SHARE/libc/argz.c:163:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/argz.c:163:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:163:
allocating variable __realloc_argz_insert_l163
[eva] FRAMAC_SHARE/libc/argz.c:167: Call to builtin memmove
[eva] FRAMAC_SHARE/libc/argz.c:167:
@@ -596,7 +598,7 @@
[eva] computing for function argz_append <- argz_add <- argz_insert <- main.
Called from FRAMAC_SHARE/libc/argz.c:288.
[eva] FRAMAC_SHARE/libc/argz.c:277: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/argz.c:277:
+[eva:malloc:new] FRAMAC_SHARE/libc/argz.c:277:
allocating variable __realloc_argz_append_l277_8
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
diff --git a/tests/libc/oracle/glob_c.res.oracle b/tests/libc/oracle/glob_c.res.oracle
index 91eb904a9ba..0b746d9c5a8 100644
--- a/tests/libc/oracle/glob_c.res.oracle
+++ b/tests/libc/oracle/glob_c.res.oracle
@@ -15,7 +15,8 @@
[eva] FRAMAC_SHARE/libc/glob.c:66: Call to builtin realloc
[eva] FRAMAC_SHARE/libc/glob.c:66:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/glob.c:66: allocating variable __realloc_glob_l66
+[eva:malloc:new] FRAMAC_SHARE/libc/glob.c:66:
+ allocating variable __realloc_glob_l66
[eva] FRAMAC_SHARE/libc/glob.c:71: starting to merge loop iterations
[eva] FRAMAC_SHARE/libc/glob.c:73: starting to merge loop iterations
[eva:alarm] FRAMAC_SHARE/libc/glob.c:74: Warning:
@@ -60,7 +61,8 @@
Called from FRAMAC_SHARE/libc/glob.c:32.
[eva] Done for function Frama_C_interval
[eva] FRAMAC_SHARE/libc/glob.c:66: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/glob.c:66: allocating variable __realloc_glob_l66_0
+[eva:malloc:new] FRAMAC_SHARE/libc/glob.c:66:
+ allocating variable __realloc_glob_l66_0
[eva] computing for function Frama_C_nondet <- glob <- main.
Called from FRAMAC_SHARE/libc/glob.c:77.
[eva] Done for function Frama_C_nondet
@@ -89,9 +91,11 @@
[eva] FRAMAC_SHARE/libc/glob.c:50: Call to builtin realloc
[eva] FRAMAC_SHARE/libc/glob.c:50:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/glob.c:50: allocating variable __realloc_glob_l50
+[eva:malloc:new] FRAMAC_SHARE/libc/glob.c:50:
+ allocating variable __realloc_glob_l50
[eva] FRAMAC_SHARE/libc/glob.c:66: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/glob.c:66: allocating variable __realloc_glob_l66_1
+[eva:malloc:new] FRAMAC_SHARE/libc/glob.c:66:
+ allocating variable __realloc_glob_l66_1
[eva] computing for function Frama_C_nondet <- glob <- main.
Called from FRAMAC_SHARE/libc/glob.c:77.
[eva] Done for function Frama_C_nondet
@@ -118,10 +122,12 @@
Called from FRAMAC_SHARE/libc/glob.c:32.
[eva] Done for function Frama_C_interval
[eva] FRAMAC_SHARE/libc/glob.c:50: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/glob.c:50: allocating variable __realloc_glob_l50_0
+[eva:malloc:new] FRAMAC_SHARE/libc/glob.c:50:
+ allocating variable __realloc_glob_l50_0
[eva] FRAMAC_SHARE/libc/glob.c:54: starting to merge loop iterations
[eva] FRAMAC_SHARE/libc/glob.c:66: Call to builtin realloc
-[eva] FRAMAC_SHARE/libc/glob.c:66: allocating variable __realloc_glob_l66_2
+[eva:malloc:new] FRAMAC_SHARE/libc/glob.c:66:
+ allocating variable __realloc_glob_l66_2
[eva] computing for function Frama_C_nondet <- glob <- main.
Called from FRAMAC_SHARE/libc/glob.c:77.
[eva] Done for function Frama_C_nondet
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 3b729753094..6d9eacca9b2 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -85,9 +85,11 @@
[eva] computing for function getaddrinfo <- main.
Called from netdb_c.c:34.
[eva] FRAMAC_SHARE/libc/netdb.c:56: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/netdb.c:56: allocating variable __malloc_getaddrinfo_l56
+[eva:malloc:new] FRAMAC_SHARE/libc/netdb.c:56:
+ allocating variable __malloc_getaddrinfo_l56
[eva] FRAMAC_SHARE/libc/netdb.c:58: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/netdb.c:58: allocating variable __malloc_getaddrinfo_l58
+[eva:malloc:new] FRAMAC_SHARE/libc/netdb.c:58:
+ allocating variable __malloc_getaddrinfo_l58
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
Called from FRAMAC_SHARE/libc/netdb.c:60.
[eva] using specification for function Frama_C_interval
@@ -149,7 +151,8 @@
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] FRAMAC_SHARE/libc/netdb.c:72: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/netdb.c:72: allocating variable __malloc_getaddrinfo_l72
+[eva:malloc:new] FRAMAC_SHARE/libc/netdb.c:72:
+ allocating variable __malloc_getaddrinfo_l72
[eva] computing for function strcpy <- getaddrinfo <- main.
Called from FRAMAC_SHARE/libc/netdb.c:74.
[eva] using specification for function strcpy
diff --git a/tests/libc/oracle/search_h.res.oracle b/tests/libc/oracle/search_h.res.oracle
index df0333934a7..29be464b5cb 100644
--- a/tests/libc/oracle/search_h.res.oracle
+++ b/tests/libc/oracle/search_h.res.oracle
@@ -20,7 +20,7 @@
accessing uninitialized left-value.
assert \initialized(&str[(int)(length - 1)]);
[eva] search_h.c:30: Call to builtin malloc
-[eva] search_h.c:30: allocating variable __malloc_main_l30
+[eva:malloc:new] search_h.c:30: allocating variable __malloc_main_l30
[eva] computing for function strcpy <- main.
Called from search_h.c:31.
[eva] using specification for function strcpy
diff --git a/tests/libc/oracle/stdio_c.res.oracle b/tests/libc/oracle/stdio_c.res.oracle
index e848a868dcf..7d6dcd1f44c 100644
--- a/tests/libc/oracle/stdio_c.res.oracle
+++ b/tests/libc/oracle/stdio_c.res.oracle
@@ -26,7 +26,8 @@
function feof: precondition 'valid_stream' got status valid.
[eva] Done for function feof
[eva] FRAMAC_SHARE/libc/stdio.c:75: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/stdio.c:75: allocating variable __malloc_getline_l75
+[eva:malloc:new] FRAMAC_SHARE/libc/stdio.c:75:
+ allocating variable __malloc_getline_l75
[eva] computing for function ferror <- getline <- main.
Called from FRAMAC_SHARE/libc/stdio.c:84.
[eva] FRAMAC_SHARE/libc/stdio.c:84:
@@ -69,7 +70,8 @@
[eva] FRAMAC_SHARE/libc/stdio.c:106: Call to builtin realloc
[eva] FRAMAC_SHARE/libc/stdio.c:106:
function realloc: precondition 'freeable' got status valid.
-[eva] FRAMAC_SHARE/libc/stdio.c:106: allocating variable __realloc_getline_l106
+[eva:malloc:new] FRAMAC_SHARE/libc/stdio.c:106:
+ allocating variable __realloc_getline_l106
[eva] FRAMAC_SHARE/libc/stdio.c:84: starting to merge loop iterations
[eva] computing for function ferror <- getline <- main.
Called from FRAMAC_SHARE/libc/stdio.c:84.
@@ -226,7 +228,8 @@
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] FRAMAC_SHARE/libc/stdio.c:124: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/stdio.c:124: allocating variable __malloc_vasprintf_l124
+[eva:malloc:new] FRAMAC_SHARE/libc/stdio.c:124:
+ allocating variable __malloc_vasprintf_l124
[eva] computing for function Frama_C_make_unknown <- vasprintf <- asprintf <- main.
Called from FRAMAC_SHARE/libc/stdio.c:129.
[eva] using specification for function Frama_C_make_unknown
@@ -256,7 +259,8 @@
[eva] Recording results for is_valid_mode
[eva] Done for function is_valid_mode
[eva] FRAMAC_SHARE/libc/stdio.c:231: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/stdio.c:231: allocating variable __malloc_fmemopen_l231
+[eva:malloc:new] FRAMAC_SHARE/libc/stdio.c:231:
+ allocating variable __malloc_fmemopen_l231
[eva] computing for function Frama_C_interval <- fmemopen <- main.
Called from FRAMAC_SHARE/libc/stdio.c:239.
[eva] FRAMAC_SHARE/libc/stdio.c:239:
diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle
index 0d0926fd83f..f5a26937b57 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] stdlib_c.c:15: Call to builtin Frama_C_calloc for function calloc
-[eva] stdlib_c.c:15: allocating variable __calloc_main_l15
+[eva:malloc:new] stdlib_c.c:15: allocating variable __calloc_main_l15
[eva] stdlib_c.c:17: assertion got status valid.
[eva] computing for function Frama_C_size_t_interval <- main.
Called from stdlib_c.c:21.
@@ -19,7 +19,7 @@
[eva] stdlib_c.c:22: Call to builtin Frama_C_calloc for function calloc
[eva] stdlib_c.c:22: Warning:
calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
-[eva] stdlib_c.c:22: allocating variable __calloc_main_l22
+[eva:malloc:new] stdlib_c.c:22: allocating variable __calloc_main_l22
[eva] stdlib_c.c:22: Call to builtin Frama_C_calloc for function calloc
[eva] stdlib_c.c:24: assertion got status valid.
[eva] stdlib_c.c:28: Call to builtin Frama_C_calloc for function calloc
@@ -30,7 +30,7 @@
[eva] stdlib_c.c:28: Call to builtin Frama_C_calloc for function calloc
[eva] stdlib_c.c:29: assertion got status valid.
[eva] stdlib_c.c:33: Call to builtin Frama_C_calloc for function calloc
-[eva] stdlib_c.c:33: allocating variable __calloc_main_l33
+[eva:malloc:new] stdlib_c.c:33: allocating variable __calloc_main_l33
[eva] stdlib_c.c:33: Call to builtin Frama_C_calloc for function calloc
[eva] stdlib_c.c:33: Call to builtin Frama_C_calloc for function calloc
[eva] stdlib_c.c:33: Call to builtin Frama_C_calloc for function calloc
@@ -64,7 +64,7 @@
[eva] FRAMAC_SHARE/libc/stdlib.c:200:
assertion 'alignment_is_a_suitable_power_of_two' got status valid.
[eva] FRAMAC_SHARE/libc/stdlib.c:203: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:203:
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:203:
allocating variable __malloc_posix_memalign_l203
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
@@ -77,7 +77,7 @@
[eva] computing for function posix_memalign <- main.
Called from stdlib_c.c:40.
[eva] FRAMAC_SHARE/libc/stdlib.c:203: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:203:
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:203:
allocating variable __malloc_posix_memalign_l203_0
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
@@ -95,7 +95,7 @@
Called from stdlib_c.c:41.
[eva] Done for function free
[eva] stdlib_c.c:44: Call to builtin Frama_C_malloc
-[eva] stdlib_c.c:44: allocating variable __malloc_main_l44
+[eva:malloc:new] stdlib_c.c:44: allocating variable __malloc_main_l44
[eva] stdlib_c.c:44: Call to builtin Frama_C_malloc
[eva] stdlib_c.c:44: Call to builtin Frama_C_malloc
[eva] stdlib_c.c:44: Call to builtin Frama_C_malloc
@@ -169,7 +169,8 @@
Called from FRAMAC_SHARE/libc/stdlib.c:226.
[eva] Done for function Frama_C_interval
[eva] FRAMAC_SHARE/libc/stdlib.c:228: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:228: allocating variable __malloc_realpath_l228
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:228:
+ allocating variable __malloc_realpath_l228
[eva] computing for function Frama_C_make_unknown <- realpath <- main.
Called from FRAMAC_SHARE/libc/stdlib.c:234.
[eva] Done for function Frama_C_make_unknown
@@ -202,7 +203,7 @@
Called from FRAMAC_SHARE/libc/stdlib.c:226.
[eva] Done for function Frama_C_interval
[eva] FRAMAC_SHARE/libc/stdlib.c:228: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:228:
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:228:
allocating variable __malloc_realpath_l228_0
[eva] computing for function Frama_C_make_unknown <- realpath <-
canonicalize_file_name <- main.
diff --git a/tests/libc/oracle/stdlib_c.1.res.oracle b/tests/libc/oracle/stdlib_c.1.res.oracle
index 679dd08280b..134ac56939a 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] stdlib_c.c:15: Call to builtin Frama_C_calloc for function calloc
-[eva] stdlib_c.c:15: allocating variable __calloc_main_l15
+[eva:malloc:new] stdlib_c.c:15: allocating variable __calloc_main_l15
[eva] stdlib_c.c:17: assertion got status valid.
[eva] computing for function Frama_C_size_t_interval <- main.
Called from stdlib_c.c:21.
@@ -16,7 +16,7 @@
[eva] stdlib_c.c:22: Call to builtin Frama_C_calloc for function calloc
[eva] stdlib_c.c:22: Warning:
calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
-[eva] stdlib_c.c:22: allocating variable __calloc_main_l22
+[eva:malloc:new] stdlib_c.c:22: allocating variable __calloc_main_l22
[eva] stdlib_c.c:24: assertion got status valid.
[eva] stdlib_c.c:28: Call to builtin Frama_C_calloc for function calloc
[eva] stdlib_c.c:28: Warning:
@@ -24,7 +24,7 @@
[eva] stdlib_c.c:28: Call to builtin Frama_C_calloc for function calloc
[eva] stdlib_c.c:29: assertion got status valid.
[eva] stdlib_c.c:33: Call to builtin Frama_C_calloc for function calloc
-[eva] stdlib_c.c:33: allocating variable __calloc_main_l33
+[eva:malloc:new] stdlib_c.c:33: allocating variable __calloc_main_l33
[eva] stdlib_c.c:33: Call to builtin Frama_C_calloc for function calloc
[eva] stdlib_c.c:33: Call to builtin Frama_C_calloc for function calloc
[eva:malloc] stdlib_c.c:33:
@@ -80,7 +80,7 @@
[eva] FRAMAC_SHARE/libc/stdlib.c:200:
assertion 'alignment_is_a_suitable_power_of_two' got status valid.
[eva] FRAMAC_SHARE/libc/stdlib.c:203: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:203:
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:203:
allocating variable __malloc_posix_memalign_l203
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
@@ -93,7 +93,7 @@
[eva] computing for function posix_memalign <- main.
Called from stdlib_c.c:40.
[eva] FRAMAC_SHARE/libc/stdlib.c:203: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:203:
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:203:
allocating variable __malloc_posix_memalign_l203_0
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
@@ -103,7 +103,7 @@
[eva] stdlib_c.c:41: function free: precondition 'freeable' got status valid.
[eva] Done for function free
[eva] stdlib_c.c:44: Call to builtin Frama_C_malloc
-[eva] stdlib_c.c:44: allocating variable __malloc_main_l44
+[eva:malloc:new] stdlib_c.c:44: allocating variable __malloc_main_l44
[eva] computing for function realpath <- main.
Called from stdlib_c.c:46.
[eva] computing for function Frama_C_interval <- realpath <- main.
@@ -159,7 +159,8 @@
Called from FRAMAC_SHARE/libc/stdlib.c:226.
[eva] Done for function Frama_C_interval
[eva] FRAMAC_SHARE/libc/stdlib.c:228: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:228: allocating variable __malloc_realpath_l228
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:228:
+ allocating variable __malloc_realpath_l228
[eva] computing for function Frama_C_make_unknown <- realpath <- main.
Called from FRAMAC_SHARE/libc/stdlib.c:234.
[eva] Done for function Frama_C_make_unknown
@@ -220,7 +221,7 @@
Called from FRAMAC_SHARE/libc/stdlib.c:226.
[eva] Done for function Frama_C_interval
[eva] FRAMAC_SHARE/libc/stdlib.c:228: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:228:
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:228:
allocating variable __malloc_realpath_l228_0
[eva] computing for function Frama_C_make_unknown <- realpath <-
canonicalize_file_name <- main.
diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle
index 07dfdf8eecf..f0788767157 100644
--- a/tests/libc/oracle/stdlib_c.2.res.oracle
+++ b/tests/libc/oracle/stdlib_c.2.res.oracle
@@ -7,7 +7,8 @@
[eva] computing for function calloc <- main.
Called from stdlib_c.c:15.
[eva] FRAMAC_SHARE/libc/stdlib.c:72: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:72: allocating variable __malloc_calloc_l72
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:72:
+ allocating variable __malloc_calloc_l72
[eva] computing for function memset <- calloc <- main.
Called from FRAMAC_SHARE/libc/stdlib.c:73.
[eva] using specification for function memset
@@ -28,7 +29,8 @@
[eva] computing for function calloc <- main.
Called from stdlib_c.c:22.
[eva] FRAMAC_SHARE/libc/stdlib.c:72: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:72: allocating variable __malloc_calloc_l72_0
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:72:
+ allocating variable __malloc_calloc_l72_0
[eva] computing for function memset <- calloc <- main.
Called from FRAMAC_SHARE/libc/stdlib.c:73.
[eva:alarm] FRAMAC_SHARE/libc/stdlib.c:73: Warning:
@@ -45,7 +47,8 @@
[eva] computing for function calloc <- main.
Called from stdlib_c.c:33.
[eva] FRAMAC_SHARE/libc/stdlib.c:72: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:72: allocating variable __malloc_calloc_l72_1
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:72:
+ allocating variable __malloc_calloc_l72_1
[eva] computing for function memset <- calloc <- main.
Called from FRAMAC_SHARE/libc/stdlib.c:73.
[eva] Done for function memset
@@ -99,7 +102,7 @@
[eva] FRAMAC_SHARE/libc/stdlib.c:200:
assertion 'alignment_is_a_suitable_power_of_two' got status valid.
[eva] FRAMAC_SHARE/libc/stdlib.c:203: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:203:
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:203:
allocating variable __malloc_posix_memalign_l203
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
@@ -112,7 +115,7 @@
[eva] computing for function posix_memalign <- main.
Called from stdlib_c.c:40.
[eva] FRAMAC_SHARE/libc/stdlib.c:203: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:203:
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:203:
allocating variable __malloc_posix_memalign_l203_0
[eva] Recording results for posix_memalign
[eva] Done for function posix_memalign
@@ -122,7 +125,7 @@
[eva] stdlib_c.c:41: function free: precondition 'freeable' got status valid.
[eva] Done for function free
[eva] stdlib_c.c:44: Call to builtin Frama_C_malloc
-[eva] stdlib_c.c:44: allocating variable __malloc_main_l44
+[eva:malloc:new] stdlib_c.c:44: allocating variable __malloc_main_l44
[eva] computing for function realpath <- main.
Called from stdlib_c.c:46.
[eva] computing for function Frama_C_interval <- realpath <- main.
@@ -166,7 +169,8 @@
Called from FRAMAC_SHARE/libc/stdlib.c:226.
[eva] Done for function Frama_C_interval
[eva] FRAMAC_SHARE/libc/stdlib.c:228: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:228: allocating variable __malloc_realpath_l228
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:228:
+ allocating variable __malloc_realpath_l228
[eva] computing for function Frama_C_make_unknown <- realpath <- main.
Called from FRAMAC_SHARE/libc/stdlib.c:234.
[eva] Done for function Frama_C_make_unknown
@@ -185,7 +189,7 @@
Called from FRAMAC_SHARE/libc/stdlib.c:226.
[eva] Done for function Frama_C_interval
[eva] FRAMAC_SHARE/libc/stdlib.c:228: Call to builtin Frama_C_malloc
-[eva] FRAMAC_SHARE/libc/stdlib.c:228:
+[eva:malloc:new] FRAMAC_SHARE/libc/stdlib.c:228:
allocating variable __malloc_realpath_l228_0
[eva] computing for function Frama_C_make_unknown <- realpath <-
canonicalize_file_name <- main.
diff --git a/tests/libc/oracle/wchar_c_h.0.res.oracle b/tests/libc/oracle/wchar_c_h.0.res.oracle
index 1ad0e866db7..d113b492db5 100644
--- a/tests/libc/oracle/wchar_c_h.0.res.oracle
+++ b/tests/libc/oracle/wchar_c_h.0.res.oracle
@@ -188,7 +188,8 @@
[eva] FRAMAC_SHARE/libc/wchar.c:98:
function wcslen: precondition 'valid_string_s' got status valid.
[eva] FRAMAC_SHARE/libc/wchar.c:99: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/wchar.c:99: allocating variable __malloc_wcsdup_l99
+[eva:malloc:new] FRAMAC_SHARE/libc/wchar.c:99:
+ allocating variable __malloc_wcsdup_l99
[eva] computing for function wmemcpy <- wcsdup <- main.
Called from FRAMAC_SHARE/libc/wchar.c:104.
[eva] Recording results for wmemcpy
@@ -199,7 +200,8 @@
Called from wchar_c_h.c:75.
[eva] FRAMAC_SHARE/libc/wchar.c:98: Call to builtin wcslen
[eva] FRAMAC_SHARE/libc/wchar.c:99: Call to builtin malloc
-[eva] FRAMAC_SHARE/libc/wchar.c:99: allocating variable __malloc_wcsdup_l99_0
+[eva:malloc:new] FRAMAC_SHARE/libc/wchar.c:99:
+ allocating variable __malloc_wcsdup_l99_0
[eva] computing for function wmemcpy <- wcsdup <- main.
Called from FRAMAC_SHARE/libc/wchar.c:104.
[eva] Recording results for wmemcpy
diff --git a/tests/misc/oracle/array_sizeof.res.oracle b/tests/misc/oracle/array_sizeof.res.oracle
index eaf47571fe4..41a92c98b9c 100644
--- a/tests/misc/oracle/array_sizeof.res.oracle
+++ b/tests/misc/oracle/array_sizeof.res.oracle
@@ -11,7 +11,7 @@
(unsigned int)(sizeof(unsigned char [1]) + sizeof(int));
[eva] array_sizeof.i:14: assertion 'alloca_bounds' got status valid.
[eva] array_sizeof.i:14: Call to builtin __fc_vla_alloc
-[eva] array_sizeof.i:14: allocating variable __malloc_main_l14
+[eva:malloc:new] array_sizeof.i:14: allocating variable __malloc_main_l14
[eva:alarm] array_sizeof.i:15: Warning:
accessing uninitialized left-value. assert \initialized(buf_0 + x);
[eva] Recording results for main
diff --git a/tests/rte_manual/oracle/sizeof.res.oracle b/tests/rte_manual/oracle/sizeof.res.oracle
index 70fb18345d4..f7be0497677 100644
--- a/tests/rte_manual/oracle/sizeof.res.oracle
+++ b/tests/rte_manual/oracle/sizeof.res.oracle
@@ -8,11 +8,12 @@
Called from sizeof.c:14.
[eva] sizeof.c:9: assertion 'alloca_bounds' got status valid.
[eva] sizeof.c:9: Call to builtin __fc_vla_alloc
-[eva] sizeof.c:9: allocating variable __malloc_fsize3_l9
+[eva:malloc:new] sizeof.c:9: allocating variable __malloc_fsize3_l9
[eva] sizeof.c:9: Call to builtin __fc_vla_free
[eva] Recording results for fsize3
[eva] Done for function fsize3
-[eva] sizeof.c:14: freeing automatic bases: {__malloc_fsize3_l9}
+[eva:malloc:automatic-free] sizeof.c:14:
+ freeing automatic bases: {__malloc_fsize3_l9}
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/abstract_struct_1.res.oracle b/tests/value/oracle/abstract_struct_1.res.oracle
index bedc671f0e3..2701dffd874 100644
--- a/tests/value/oracle/abstract_struct_1.res.oracle
+++ b/tests/value/oracle/abstract_struct_1.res.oracle
@@ -20,7 +20,7 @@
S_data_0_S_repositories[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
S_data_1_S_repositories[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
[eva] abstract_struct_1.c:13: Call to builtin calloc
-[eva] abstract_struct_1.c:13: allocating variable __calloc_main_l13
+[eva:malloc:new] abstract_struct_1.c:13: allocating variable __calloc_main_l13
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/empty_struct.5.res.oracle b/tests/value/oracle/empty_struct.5.res.oracle
index 5fc51fa1c2f..1d42b062fb7 100644
--- a/tests/value/oracle/empty_struct.5.res.oracle
+++ b/tests/value/oracle/empty_struct.5.res.oracle
@@ -8,11 +8,11 @@
nondet ∈ [--..--]
pgs ∈ {{ &gs }}
[eva] empty_struct.c:78: Call to builtin malloc
-[eva] empty_struct.c:78: allocating variable __malloc_main3_l78
+[eva:malloc:new] empty_struct.c:78: allocating variable __malloc_main3_l78
[eva] empty_struct.c:79: Call to builtin realloc
[eva] empty_struct.c:79:
function realloc: precondition 'freeable' got status valid.
-[eva] empty_struct.c:79: allocating variable __realloc_main3_l79
+[eva:malloc:new] empty_struct.c:79: allocating variable __realloc_main3_l79
[eva] empty_struct.c:81: starting to merge loop iterations
[eva] empty_struct.c:86: Call to builtin free
[eva] empty_struct.c:86:
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index 77cb1d73a4c..05ebd53c77a 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/tests/value/oracle/gauges.res.oracle
@@ -715,7 +715,7 @@
[eva] computing for function main17 <- main.
Called from gauges.c:369.
[eva] gauges.c:343: Call to builtin malloc
-[eva] gauges.c:343: allocating variable __malloc_main17_l343
+[eva:malloc:new] gauges.c:343: allocating variable __malloc_main17_l343
[eva] gauges.c:342: starting to merge loop iterations
[eva] gauges.c:343: Call to builtin malloc
[eva] Recording results for main17
--
GitLab