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

[Eva] In the malloc test, tests that the base for the imprecise builtin is weak.

parent 83bf91d9
No related branches found
No related tags found
No related merge requests found
...@@ -33,7 +33,7 @@ void main(int c) { ...@@ -33,7 +33,7 @@ void main(int c) {
int *mw = Frama_C_malloc_imprecise(42); int *mw = Frama_C_malloc_imprecise(42);
*mw = 1; *mw = 1;
int *mw2 = Frama_C_malloc_imprecise(42); int *mw2 = Frama_C_malloc_imprecise(42);
*mw2 = 1; *mw2 = 2;
// *s = 1; // *s = 1;
} }
...@@ -72,5 +72,5 @@ ...@@ -72,5 +72,5 @@
[1] ∈ UNINITIALIZED [1] ∈ UNINITIALIZED
[2] ∈ {3} [2] ∈ {3}
[3..24] ∈ UNINITIALIZED [3..24] ∈ UNINITIALIZED
__alloc_w_main[bits 0 to 31] ∈ {1} or UNINITIALIZED __alloc_w_main[bits 0 to 31] ∈ {1; 2} or UNINITIALIZED
[4..4294967295] ∈ UNINITIALIZED [4..4294967295] ∈ UNINITIALIZED
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