[Eva] Fixes the test of "builtins" repository with the multidim config.

tests/builtins/oracle_multidim/alloc.0.res.oracle

-32a33,34
-> [eva:alarm] alloc.c:22: Warning: out of bounds write. assert \valid(t + 9);
-> [eva:alarm] alloc.c:23: Warning: out of bounds write. assert \valid(p);
-34a37
-> [eva:alarm] alloc.c:25: Warning: out of bounds write. assert \valid(q);
-57a61
-> [eva:alarm] alloc.c:38: Warning: out of bounds write. assert \valid(v);

tests/builtins/oracle_multidim/alloc.1.res.oracle

-17a18
-> [eva:alarm] alloc.c:50: Warning: out of bounds write. assert \valid(q);

tests/builtins/oracle_multidim/alloc_weak.res.oracle

-14d13
-< [eva:malloc:weak] alloc_weak.c:23: marking variable `__malloc_main1_l23' as weak
-62d60
-< [eva:malloc:weak] alloc_weak.c:51: marking variable `__malloc_main3_l51' as weak

tests/builtins/oracle_multidim/allocated.0.res.oracle

-9c9,10
-< [eva] allocated.c:25: assertion got status valid.
----
-> [eva:alarm] allocated.c:25: Warning: assertion got status unknown.
-> [eva:alarm] allocated.c:26: Warning: out of bounds write. assert \valid(p);
-18d18
-< [eva:malloc] allocated.c:31: strong free on bases: {__malloc_main_l25}
-22c22,23
-< [eva] allocated.c:36: assertion got status valid.
----
-> [eva:alarm] allocated.c:36: Warning: assertion got status unknown.
-> [eva:alarm] allocated.c:37: Warning: out of bounds write. assert \valid(p + 0);
-28d28
-< [eva:malloc] allocated.c:43: strong free on bases: {__malloc_main_l36}
-34d33
-< [eva:malloc] allocated.c:45: strong free on bases: {__malloc_main_l36}
-42c41,42
-< [eva] allocated.c:50: assertion got status valid.
----
-> [eva:alarm] allocated.c:50: Warning: assertion got status unknown.
-> [eva:alarm] allocated.c:51: Warning: out of bounds write. assert \valid(p + 0);
-50d49
-< [eva:malloc] allocated.c:58: strong free on bases: {__malloc_main_l50}
-53a53,56
-> [eva:alarm] allocated.c:63: Warning: assertion got status unknown.
-> [eva:alarm] allocated.c:64: Warning: out of bounds write. assert \valid(p);
-> [kernel] allocated.c:64: Warning: 
->   all target addresses were invalid. This path is assumed to be dead.
-58d60
-< [eva:malloc] allocated.c:67: strong free on bases: {__malloc_main_l63}
-63d64
-< [eva:malloc] allocated.c:67: strong free on bases: {__malloc_main_l63}
-68d68
-< [eva:malloc] allocated.c:67: strong free on bases: {__malloc_main_l63}
-73d72
-< [eva:malloc] allocated.c:67: strong free on bases: {__malloc_main_l63}
-75a75
-> [eva:alarm] allocated.c:74: Warning: out of bounds write. assert \valid(p);
-80d79
-< [eva:malloc] allocated.c:77: strong free on bases: {__malloc_main_l73}
-83c82
-< [eva] allocated.c:76: Frama_C_show_each_p0: {1}
----
-> [eva] allocated.c:76: Frama_C_show_each_p0: {0; 1}
-85d83
-< [eva:malloc] allocated.c:77: strong free on bases: {__malloc_main_l73}
-89c87
-< [eva] allocated.c:76: Frama_C_show_each_p0: {1; 2}
----
-> [eva] allocated.c:76: Frama_C_show_each_p0: {0; 1; 2}
-91d88
-< [eva:malloc] allocated.c:77: strong free on bases: {__malloc_main_l73}
-94c91
-< [eva] allocated.c:76: Frama_C_show_each_p0: {1; 2; 3}
----
-> [eva] allocated.c:76: Frama_C_show_each_p0: {0; 1; 2; 3}
-96c93
-< [eva:malloc] allocated.c:77: strong free on bases: {__malloc_main_l73}
----
+96a97
 > [eva] allocated.c:73: Call to builtin malloc
-99c96
-< [eva] allocated.c:82: assertion got status valid.
----
-> [eva:alarm] allocated.c:82: Warning: assertion got status unknown.
-102d98
-< [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82}
-104,106d99
-< [eva:malloc:weak] allocated.c:82: marking variable `__malloc_main_l82' as weak
-< [eva:malloc] allocated.c:82: 
-<   resizing variable `__malloc_w_main_l82' (0..-1) to fit 0..31
-110d102
-< [eva:malloc] allocated.c:87: weak free on bases: {__malloc_w_main_l82}
-113,114d104
-< [eva:malloc] allocated.c:82: 
-<   resizing variable `__malloc_w_main_l82' (0..-1/31) to fit 0..31/63
-116d105
-< [eva:malloc] allocated.c:87: weak free on bases: {__malloc_w_main_l82}
-118,119d106
-< [eva:malloc] allocated.c:82: 
-<   resizing variable `__malloc_w_main_l82' (0..-1/63) to fit 0..31/95
-121d107
-< [eva:malloc] allocated.c:87: weak free on bases: {__malloc_w_main_l82}
-123,124d108
-< [eva:malloc] allocated.c:82: 
-<   resizing variable `__malloc_w_main_l82' (0..-1/95) to fit 0..31/95
-127c111
-< [eva] allocated.c:91: assertion got status valid.
----
-> [eva:alarm] allocated.c:91: Warning: assertion got status unknown.
-130d113
-< [eva:malloc] allocated.c:92: strong free on bases: {__malloc_main_l91}
-134c117
-< [eva] allocated.c:97: Frama_C_show_each: {{ &__malloc_main_l97 }}
----
-> [eva] allocated.c:97: Frama_C_show_each: {{ NULL ; &__malloc_main_l97 }}
-139d121
-< [eva:malloc] allocated.c:111: strong free on bases: {__malloc_main_l97}
-143c125
-< [eva] allocated.c:114: Frama_C_show_each: {{ &__malloc_main_l114 }}
----
-> [eva] allocated.c:114: Frama_C_show_each: {{ NULL ; &__malloc_main_l114 }}
-148d129
-< [eva:malloc] allocated.c:118: strong free on bases: {__malloc_main_l114}
-151c132
-< [eva] allocated.c:120: Frama_C_show_each: {{ &__malloc_main_l120 }}
----
-> [eva] allocated.c:120: Frama_C_show_each: {{ NULL ; &__malloc_main_l120 }}
-155d135
-< [eva:malloc] allocated.c:125: strong free on bases: {__malloc_main_l120}
-159,200d138
+159,200d159
 < [eva] allocated.c:131: Frama_C_show_each: {0}
 < [eva] allocated.c:127: Call to builtin __fc_vla_free
 < [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
@@ -150,7 +43,7 @@
 < [eva] allocated.c:131: Frama_C_show_each: [0..2147483647]
 < [eva] allocated.c:127: Call to builtin __fc_vla_free
 < [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
-208,217c146
+208,217c167
 <   __fc_heap_status ∈ [--..--]
 <   i ∈ {10}
 <   j ∈ [1..2147483647]
@@ -163,15 +56,15 @@
 <                      [2] ∈ [7..27] or UNINITIALIZED
 ---
 >   NON TERMINATING FUNCTION
-225,226c154
+225,226c175
 < [from] Computing for function __fc_vla_free <-main
 < [from] Done for function __fc_vla_free
 ---
 > [from] Non-terminating function main (no dependencies)
-232,233d159
+232,233d180
 < [from] Function __fc_vla_free:
 <   NO EFFECTS
-240,250c166
+240,250c187
 <   __fc_heap_status FROM __fc_heap_status; nondet (and SELF)
 <   __malloc_main_l25 FROM __fc_heap_status
 <   __malloc_main_l36[0..1] FROM __fc_heap_status; nondet
@@ -185,7 +78,7 @@
 <   \result FROM \nothing
 ---
 >   NON TERMINATING - NO EFFECTS
-254,257c170,172
+254,257c191,193
 <     __retres; __malloc_main_l25; __malloc_main_l36[0..1];
 <     __malloc_main_l50[0..2]; __malloc_main_l63; __malloc_main_l73;
 <     __malloc_w_main_l82[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
@@ -194,7 +87,7 @@
 >     __malloc_main_l25; __malloc_main_l36[0..1]; __malloc_main_l50[0..2];
 >     __malloc_main_l63; __malloc_main_l73; __malloc_w_main_l82[0..2];
 >     __malloc_main_l97[0]; __malloc_main_l114[0..3]
-261,262c176
+261,262c197
 <     __malloc_main_l97[0][bits 0 to 0]; __malloc_main_l114[0][bits 0 to 0];
 <     __malloc_main_l127[0..9]
 ---

tests/builtins/oracle_multidim/calloc.1.res.oracle

-31,35c31,35
-<   p1 ∈ {{ &__calloc_main_l14[0] }}
-<   p2 ∈ {{ &__calloc_main_l17[0] }}
-<   p3 ∈ {{ &__calloc_main_l20[0] }}
-<   p4 ∈ {{ &__calloc_main_l23 }}
-<   p5 ∈ {{ &__calloc_main_l30[0] }}
----
->   p1 ∈ {{ NULL ; &__calloc_main_l14[0] }}
->   p2 ∈ {{ NULL ; &__calloc_main_l17[0] }}
->   p3 ∈ {{ NULL ; &__calloc_main_l20[0] }}
->   p4 ∈ {{ NULL ; &__calloc_main_l23 }}
->   p5 ∈ {{ NULL ; &__calloc_main_l30[0] }}
-37c37
-<   __retres ∈ {0}
----
->   __retres ∈ {0; 1}

tests/builtins/oracle_multidim/calloc.2.res.oracle

-31,35c31,35
-<   p1 ∈ {{ &__calloc_main_l14[0] }}
-<   p2 ∈ {{ &__calloc_main_l17[0] }}
-<   p3 ∈ {{ &__calloc_main_l20[0] }}
-<   p4 ∈ {{ &__calloc_main_l23 }}
-<   p5 ∈ {{ &__calloc_main_l30[0] }}
----
->   p1 ∈ {{ NULL ; &__calloc_main_l14[0] }}
->   p2 ∈ {{ NULL ; &__calloc_main_l17[0] }}
->   p3 ∈ {{ NULL ; &__calloc_main_l20[0] }}
->   p4 ∈ {{ NULL ; &__calloc_main_l23 }}
->   p5 ∈ {{ NULL ; &__calloc_main_l30[0] }}
-37c37
-<   __retres ∈ {0}
----
->   __retres ∈ {0; 1}

tests/builtins/oracle_multidim/free.res.oracle

-10a11
-> [eva:alarm] free.c:9: Warning: out of bounds write. assert \valid(p + 1);
-12a14
-> [eva:alarm] free.c:11: Warning: out of bounds write. assert \valid(q + 2);
-44,45d45
-< [eva:malloc] free.c:14: 
-<   weak free on bases: {__malloc_main1_l8, __malloc_main1_l10}
-47a48
-> [eva:alarm] free.c:17: Warning: out of bounds write. assert \valid(u + 3);
-50d50
-< [eva:malloc] free.c:18: strong free on bases: {__malloc_main1_l16}
-53d52
-< [eva:malloc] free.c:21: strong free on bases: {}
-55a55
-> [eva:alarm] free.c:24: Warning: out of bounds write. assert \valid(s + 4);
-58d57
-< [eva:malloc] free.c:26: weak free on bases: {__malloc_main1_l23}
-67d65
-< [eva:malloc] free.c:39: strong free on bases: {__malloc_main2_l35}
-92c90
-<   p ∈ ESCAPINGADDR
----
->   p ∈ {{ NULL ; &__malloc_main2_l35 }} or ESCAPINGADDR
-93a92
->   __malloc_main2_l35 ∈ {1} or UNINITIALIZED
-104a104
->   __malloc_main2_l35 ∈ {1} or UNINITIALIZED
-130c130
-<   __malloc_main2_l35 FROM __fc_heap_status
----
->   __malloc_main2_l35 FROM __fc_heap_status (and SELF)

tests/builtins/oracle_multidim/from_result.res.oracle

-10a11
-> [eva:alarm] from_result.c:19: Warning: out of bounds write. assert \valid(ax);

tests/builtins/oracle_multidim/gcc_zero_length_array.res.oracle

-10a11,14
-> [eva:alarm] gcc_zero_length_array.c:16: Warning: 
->   out of bounds write. assert \valid(&p->len);
-> [kernel] gcc_zero_length_array.c:16: Warning: 
->   all target addresses were invalid. This path is assumed to be dead.
-16,17d19
-< [eva:malloc] gcc_zero_length_array.c:26: 
-<   strong free on bases: {__malloc_make_fam_l15}

tests/builtins/oracle_multidim/imprecise-malloc-free.res.oracle

-50d49
-< [eva:malloc] imprecise-malloc-free.c:25: weak free on bases: {__malloc_main_l14}
-56,57d54
-< [eva:malloc] imprecise-malloc-free.c:26: 
-<   weak free on bases: {__malloc_main_l15, __malloc_main_l16}

tests/builtins/oracle_multidim/linked_list.0.res.oracle

-48c48,50
-<   function malloc, behavior allocation: postcondition 'allocation' got status unknown.
----
->   function malloc, behavior allocation: postcondition 'allocation' got status unknown. (Behavior may be inactive, no reduction performed.)
-> [eva:alarm] FRAMAC_SHARE/libc/stdlib.h:399: Warning: 
->   function malloc, behavior no_allocation: postcondition 'null_result' got status invalid. (Behavior may be inactive, no reduction performed.)
-487a490,491
-> [eva] FRAMAC_SHARE/libc/stdlib.h:399: 
->   function malloc, behavior no_allocation: postcondition 'null_result' got status valid. (Behavior may be inactive, no reduction performed.)

tests/builtins/oracle_multidim/linked_list.1.res.oracle

-48c48,50
-<   function malloc, behavior allocation: postcondition 'allocation' got status unknown.
----
->   function malloc, behavior allocation: postcondition 'allocation' got status unknown. (Behavior may be inactive, no reduction performed.)
-> [eva:alarm] FRAMAC_SHARE/libc/stdlib.h:399: Warning: 
->   function malloc, behavior no_allocation: postcondition 'null_result' got status invalid. (Behavior may be inactive, no reduction performed.)
-488a491,492
-> [eva] FRAMAC_SHARE/libc/stdlib.h:399: 
->   function malloc, behavior no_allocation: postcondition 'null_result' got status valid. (Behavior may be inactive, no reduction performed.)

tests/builtins/oracle_multidim/linked_list.2.res.oracle

-48c48,50
-<   function malloc, behavior allocation: postcondition 'allocation' got status unknown.
----
->   function malloc, behavior allocation: postcondition 'allocation' got status unknown. (Behavior may be inactive, no reduction performed.)
-> [eva:alarm] FRAMAC_SHARE/libc/stdlib.h:399: Warning: 
->   function malloc, behavior no_allocation: postcondition 'null_result' got status invalid. (Behavior may be inactive, no reduction performed.)

tests/builtins/oracle_multidim/malloc-deps.res.oracle

-8a9,11
-> [eva:alarm] malloc-deps.c:13: Warning: out of bounds write. assert \valid(p);
-> [kernel] malloc-deps.c:13: Warning: 
->   all target addresses were invalid. This path is assumed to be dead.
-10a14,16
-> [eva:alarm] malloc-deps.c:18: Warning: out of bounds write. assert \valid(q);
-> [kernel] malloc-deps.c:18: Warning: 
->   all target addresses were invalid. This path is assumed to be dead.
-19a26,34
-> [eva] computing for function g <- main.
->   Called from malloc-deps.c:26.
-> [kernel] malloc-deps.c:7: Warning: 
->   all target addresses were invalid. This path is assumed to be dead.
-> [eva] Recording results for g
-> [from] Computing for function g
-> [from] Non-terminating function g (no dependencies)
-> [from] Done for function g
-> [eva] Done for function g
-21d35
-< [eva:malloc:weak] malloc-deps.c:25: marking variable `__malloc_main_l25' as weak
-31a46,52
-> [eva] computing for function g <- main.
->   Called from malloc-deps.c:26.
-> [eva] Recording results for g
-> [from] Computing for function g
-> [from] Non-terminating function g (no dependencies)
-> [from] Done for function g
-> [eva] Done for function g
-52c73
-<   resizing variable `__malloc_w_main_l25' (0..31/127) to fit 0..159
----
->   resizing variable `__malloc_w_main_l25' (0..31/127) to fit 0..127/159
-61c82
-<   resizing variable `__malloc_w_main_l25' (0..31/159) to fit 0..191
----
->   resizing variable `__malloc_w_main_l25' (0..31/159) to fit 0..127/191
-71c92
-<   resizing variable `__malloc_w_main_l25' (0..31/191) to fit 0..191/223
----
->   resizing variable `__malloc_w_main_l25' (0..31/191) to fit 0..127/223
-80c101
-<   resizing variable `__malloc_w_main_l25' (0..31/223) to fit 0..191/255
----
->   resizing variable `__malloc_w_main_l25' (0..31/223) to fit 0..127/255
-89c110
-<   resizing variable `__malloc_w_main_l25' (0..31/255) to fit 0..191/319
----
->   resizing variable `__malloc_w_main_l25' (0..31/255) to fit 0..127/319
-98c119
-<   resizing variable `__malloc_w_main_l25' (0..31/319) to fit 0..191/319
----
->   resizing variable `__malloc_w_main_l25' (0..31/319) to fit 0..127/319

tests/builtins/oracle_multidim/malloc-optimistic.res.oracle

-14,15d13
-< [eva:malloc] malloc-optimistic.c:17: 
-<   resizing variable `__malloc_main1_l17' (0..31) to fit 0..63
-19a18,19
-> [kernel] malloc-optimistic.c:19: Warning: 
->   all target addresses were invalid. This path is assumed to be dead.
-22,3402d21
+16,19d15
+< [eva] malloc-optimistic.c:18: Frama_C_show_each_1_2: {0}
+< [eva] malloc-optimistic.c:18: Frama_C_show_each_1_2: {1}
+< [eva:alarm] malloc-optimistic.c:19: Warning: 
+<   out of bounds write. assert \valid(p + i);
+22,3402d17
 < [eva] malloc-optimistic.c:136: Call to builtin free
 < [eva:malloc] malloc-optimistic.c:136: strong free on bases: {__malloc_main1_l17}
 < [eva] computing for function main2 <- main.
@@ -3386,13 +3385,10 @@
 <   Frama_C_show_each: [30..99], {{ &__malloc_w_main9_l119 }}
 < [eva] Recording results for main9
 < [eva] Done for function main9
-3404a24,25
-> [eva] malloc-optimistic.c:19: 
->   assertion 'Eva,mem_access' got final status invalid.
-3406,3407d26
+3406,3407d20
 < [eva:final-states] Values at end of function main9_aux:
 <   __malloc_w_main9_l119 ∈ [-20..99] or UNINITIALIZED
-3409,3492c28
+3409,3492c22
 <   i ∈ {0; 1}
 <   p ∈ {{ &__malloc_main1_l17[0] }}
 <   __retres ∈ {{ (void *)&__malloc_main1_l17 }}
@@ -3479,7 +3475,7 @@
 <                          [2] ∈ {2}
 ---
 >   NON TERMINATING FUNCTION
-3494,3525c30
+3494,3525c24
 <   p ∈ ESCAPINGADDR
 <   __malloc_w_main6_l77[0] ∈ UNINITIALIZED
 <                       [1] ∈ {0; 1} or UNINITIALIZED
@@ -3514,9 +3510,9 @@
 < [from] Done for function main9_aux
 ---
 >   NON TERMINATING FUNCTION
-3528a34
+3528a28
 > [from] Non-terminating function main1 (no dependencies)
-3530,3551d35
+3530,3551d29
 < [from] Computing for function main2
 < [from] Done for function main2
 < [from] Computing for function main5
@@ -3539,14 +3535,14 @@
 < [from] Done for function main_4_aux
 < [from] Computing for function main4
 < [from] Done for function main4
-3552a37
+3552a31
 > [from] Non-terminating function main (no dependencies)
-3556,3559d40
+3556,3559d34
 < [from] Function free:
 <   NO EFFECTS
 < [from] Function main9_aux:
 <   __malloc_w_main9_l119 FROM p (and SELF)
-3563,3594c44
+3563,3594c38
 <   __malloc_main1_l17[0..1] FROM v (and SELF)
 <   \result FROM \nothing
 < [from] Function main2:
@@ -3581,7 +3577,7 @@
 <   \result FROM \nothing
 ---
 >   NON TERMINATING - NO EFFECTS
-3596,3604c46
+3596,3604c40
 <   __malloc_main1_l17[0..1] FROM v (and SELF)
 <   __malloc_main2_l27[1..2] FROM v (and SELF)
 <   __malloc_main_3_aux_l34[0..1] FROM v (and SELF)
@@ -3593,16 +3589,16 @@
 <   __malloc_w_main9_l119 FROM \nothing (and SELF)
 ---
 >   NON TERMINATING - NO EFFECTS
-3606,3609d47
+3606,3609d41
 < [inout] Out (internal) for function main9_aux:
 <     __malloc_w_main9_l119
 < [inout] Inputs for function main9_aux:
 <     \nothing
-3611c49
+3611c43
 <     i; p; __retres; __malloc_main1_l17[0..1]
 ---
 >     i; p
-3614,3653d51
+3614,3653d45
 < [inout] Out (internal) for function main2:
 <     i; p; __retres; __malloc_main2_l27[1..2]
 < [inout] Inputs for function main2:
@@ -3643,7 +3639,7 @@
 <     i; p; __retres; __malloc_main_4_aux_l40[1..2]
 < [inout] Inputs for function main4:
 <     v
-3655,3659c53
+3655,3659c47
 <     p; __malloc_main1_l17[0..1]; __malloc_main2_l27[1..2];
 <     __malloc_main_3_aux_l34[0..1]; __malloc_main_4_aux_l40[1..2];
 <     __malloc_main5_l64[0..10]; __malloc_w_main6_l77[0..10];
@@ -3651,7 +3647,7 @@
 <     __malloc_w_main9_l119
 ---
 >     p
-3661,3663c55
+3661,3663c49
 <     v; __malloc_main5_l64[0..10]; __malloc_w_main6_l77[0..10];
 <     __malloc_main7_l90[0..100]; __malloc_w_main8_l103[0..100];
 <     __malloc_w_main9_l119

tests/builtins/oracle_multidim/malloc-size-zero.0.res.oracle

-12a13
-> [eva] malloc-size-zero.c:17: Frama_C_show_each_NULL_p1:
-13a15
-> [eva] malloc-size-zero.c:22: Frama_C_show_each_NULL_p1:
-44,45d45
-< [eva:malloc:weak] malloc-size-zero.c:10: 
-<   marking variable `__malloc_my_calloc_l10_3' as weak
-64c64
-<   p1 ∈ {{ &__malloc_my_calloc_l10[0] }}
----
->   p1 ∈ {{ NULL ; &__malloc_my_calloc_l10[0] }}
-66c66
-<     {{ &__malloc_my_calloc_l10_0[0] ; &__malloc_my_calloc_l10_1[0] ;
----
->     {{ NULL ; &__malloc_my_calloc_l10_0[0] ; &__malloc_my_calloc_l10_1[0] ;
-83,84d82
-< [eva:malloc] malloc-size-zero.c:37: 
-<   strong free on bases: {__malloc_my_calloc_l10}
-87c85
-<   {{ &__malloc_my_calloc_l10_0 ; &__malloc_my_calloc_l10_1 ;
----
->   {{ NULL ; &__malloc_my_calloc_l10_0 ; &__malloc_my_calloc_l10_1 ;
-101,103d98
-< [eva:malloc] malloc-size-zero.c:44: 
-<   weak free on bases: {__malloc_my_calloc_l10_0, __malloc_my_calloc_l10_1,
-<                        __malloc_my_calloc_l10_2, __malloc_w_my_calloc_l10_3}
-115c110
-<   p1 ∈ ESCAPINGADDR
----
->   p1 ∈ {{ NULL ; &__malloc_my_calloc_l10[0] }} or ESCAPINGADDR
-117c112
-<     {{ &__malloc_my_calloc_l10_0[0] ; &__malloc_my_calloc_l10_1[0] ;
----
->     {{ NULL ; &__malloc_my_calloc_l10_0[0] ; &__malloc_my_calloc_l10_1[0] ;

tests/builtins/oracle_multidim/malloc-size-zero.1.res.oracle

-12a13
-> [eva] malloc-size-zero.c:17: Frama_C_show_each_NULL_p1:
-13a15
-> [eva] malloc-size-zero.c:22: Frama_C_show_each_NULL_p1:
-26,27d27
-< [eva:malloc:weak] malloc-size-zero.c:10: 
-<   marking variable `__malloc_main_l29' as weak
-46,47c46,47
-<   p1 ∈ {{ &__malloc_main_l16[0] }}
-<   q1 ∈ {{ &__malloc_w_main_l29[0] }} or UNINITIALIZED
----
->   p1 ∈ {{ NULL ; &__malloc_main_l16[0] }}
->   q1 ∈ {{ NULL ; &__malloc_w_main_l29[0] }} or UNINITIALIZED
-60,61c60,61
-< [eva:malloc] malloc-size-zero.c:37: strong free on bases: {__malloc_main_l16}
-< [eva] malloc-size-zero.c:39: Frama_C_show_each: {{ &__malloc_w_main_l29 }}
----
-> [eva] malloc-size-zero.c:39: 
->   Frama_C_show_each: {{ NULL ; &__malloc_w_main_l29 }}
-74d73
-< [eva:malloc] malloc-size-zero.c:44: weak free on bases: {__malloc_w_main_l29}
-86,87c85,86
-<   p1 ∈ ESCAPINGADDR
-<   q1 ∈ {{ &__malloc_w_main_l29[0] }} or ESCAPINGADDR
----
->   p1 ∈ {{ NULL ; &__malloc_main_l16[0] }} or ESCAPINGADDR
->   q1 ∈ {{ NULL ; &__malloc_w_main_l29[0] }} or ESCAPINGADDR

tests/builtins/oracle_multidim/malloc.res.oracle

-12,13c12
-< [eva:malloc] malloc.c:17: 
-<   resizing variable `__malloc_main_l17' (0..-1/34359738359) to fit 0..-1
----
-> [eva] malloc.c:17: Call to builtin malloc
-16a16,19
-> [eva] malloc.c:18: Call to builtin malloc
-> [eva] malloc.c:18: Call to builtin malloc
-> [eva] malloc.c:18: Call to builtin malloc
-> [eva] malloc.c:18: Call to builtin malloc
-19,20d21
-< [eva] malloc.c:20: Call to builtin malloc
-< [eva] malloc.c:20: allocating variable __malloc_main_l20_0
-23a25
-> [eva:alarm] malloc.c:25: Warning: out of bounds write. assert \valid(q);
-25a28,30
-> [eva:alarm] malloc.c:29: Warning: out of bounds write. assert \valid(r);
-> [kernel] malloc.c:29: Warning: 
->   all target addresses were invalid. This path is assumed to be dead.
-29d33
-< [eva] malloc.c:33: Call to builtin malloc
-31c35,36
-< [eva] malloc.c:36: Call to builtin malloc
----
-> [kernel] malloc.c:34: Warning: 
->   all target addresses were invalid. This path is assumed to be dead.
-33a39,40
-> [kernel] malloc.c:37: Warning: 
->   all target addresses were invalid. This path is assumed to be dead.
-43c50
-<   r ∈ {{ &__malloc_main_l20[0] ; &__malloc_main_l20_0[0] }}
----
->   r ∈ {{ &__malloc_main_l20[0] }}
-59,62d65
-<   __malloc_main_l20_0[0] ∈ {1}
-<                      [1] ∈ UNINITIALIZED
-<                      [2] ∈ {3}
-<                      [3..24] ∈ UNINITIALIZED

tests/builtins/oracle_multidim/malloc_bug_tr.res.oracle

-16,17c16,17
-< [eva] malloc_bug_tr.c:13: 
-<   function memcpy: precondition 'valid_dest' got status valid.
----
-> [eva:alarm] malloc_bug_tr.c:13: Warning: 
->   function memcpy: precondition 'valid_dest' got status unknown.
-32,33c32,33
-< [eva] malloc_bug_tr.c:15: 
-<   function memcpy: precondition 'valid_dest' got status valid.
----
-> [eva:alarm] malloc_bug_tr.c:15: Warning: 
->   function memcpy: precondition 'valid_dest' got status unknown.
-45d44
-< [eva:malloc] malloc_bug_tr.c:18: strong free on bases: {__malloc_main_l12}