Skip to content
Snippets Groups Projects
Commit 84e5d816 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Updates alternative test oracles.

parent 96868fce
No related branches found
No related tags found
No related merge requests found
627a628,964
632a633,969
> [eva] realloc.c:152: Call to builtin realloc
> [eva:malloc] bases_to_realloc: {__realloc_w_main10_l152}
> [eva:malloc] realloc.c:152: weak free on bases: {__realloc_w_main10_l152}
......@@ -336,7 +336,7 @@
> __realloc_w_main10_l152[0] ∈ {4}
> [1] ∈ UNINITIALIZED
> ==END OF DUMP==
694a1032,1096
699a1037,1101
> [eva] realloc.c:167: Call to builtin reallocarray
> [eva] realloc.c:167: Call to builtin reallocarray
> [eva] computing for function Frama_C_interval <- main11 <- main.
......@@ -402,7 +402,7 @@
> [eva:malloc] bases_to_realloc: {}
> [eva:malloc] realloc.c:171: strong free on bases: {}
> [eva] realloc.c:172: Frama_C_show_each_p: {{ NULL ; &__realloc_w_main11_l171 }}
762,763c1164,1166
767,768c1169,1171
< p ∈ {{ NULL ; &__malloc_main11_l160 ; (int *)&__realloc_main11_l171 }}
< q ∈ {0} or UNINITIALIZED or ESCAPINGADDR
---
......
137,139c137,138
142,144c142,143
< u1{.l[bits 0 to 31]; .f; .d[bits 0 to 31]} ∈
< [-3.40282346639e+38 .. 3.40282346639e+38]
< {.l[bits 32 to 63]; .f[bits 32 to 63]; .d[bits 32 to 63]} ∈ [--..--]
......
120,121c120,121
125,126c125,126
< u1{.l[bits 0 to 31]; .f; .d[bits 0 to 31]} ∈ [-inf .. inf]
< {.l[bits 32 to 63]; .f[bits 32 to 63]; .d[bits 32 to 63]} ∈ [--..--]
---
......
25c25
26c26
< d1 ∈ [0x1.16c2000000000p-133 .. 0x1.16c3000000000p-133]
---
> d1 ∈ {0x1.16c2000000000p-133}
......@@ -6,26 +6,26 @@
< [eva] relations2.i:17: Frama_C_show_each_end: [0..4294967295], [0..64]
---
> [eva] relations2.i:17: Frama_C_show_each_end: [0..1023], [0..64]
68,70d67
69,71d68
< [eva:alarm] relations2.i:34: Warning:
< accessing out of bounds index.
< assert (unsigned int)(i - (unsigned int)(t + 1)) < 514;
123,124d119
127,128d123
< [eva:alarm] relations2.i:35: Warning:
< signed overflow. assert s + b3 ≤ 2147483647;
139c134
143c138
< len ∈ [--..--]
---
> len ∈ [0..1023]
182c177
186c181
< \result FROM a[0..513]
---
> \result FROM a[0..511]
198c193
202c197
< a[0..513]
---
> a[0..511]
202c197
206c201
< sv; a[0..513]; T[0..6]
---
> sv; a[0..511]; T[0..6]
87,92d86
89,94d88
< [eva:alarm] period.c:53: Warning:
< pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
< [eva] period.c:53:
< Assigning imprecise value to p.
< The imprecision originates from Arithmetic {period.c:53}
< [eva:alarm] period.c:54: Warning: out of bounds read. assert \valid_read(p);
97d90
99d92
< [scope:rm_asserts] removing 1 assertion(s)
......@@ -2,5 +2,5 @@
< n ∈ [0..512]
---
> n ∈ [1..512]
132d131
136d135
< [eva] relations2.i:57: Frama_C_show_each_NO2:
......@@ -10,35 +10,35 @@
< n ∈ [0..512]
---
> n ∈ [1..512]
68,70d67
69,71d68
< [eva:alarm] relations2.i:34: Warning:
< accessing out of bounds index.
< assert (unsigned int)(i - (unsigned int)(t + 1)) < 514;
79c76
80c77
< n ∈ [0..512]
---
> n ∈ [1..512]
96c93
98c95
< n ∈ [0..512]
---
> n ∈ [1..512]
113c110
116c113
< n ∈ [0..512]
---
> n ∈ [1..512]
139c136
143c140
< len ∈ [--..--]
---
> len ∈ [0..1023]
182c179
186c183
< \result FROM a[0..513]
---
> \result FROM a[0..511]
198c195
202c199
< a[0..513]
---
> a[0..511]
202c199
206c203
< sv; a[0..513]; T[0..6]
---
> sv; a[0..511]; T[0..6]
132d131
136d135
< [eva] relations2.i:57: Frama_C_show_each_NO2:
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment