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