diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c index af7f6c2470d0dc1c90b316f0d8651271e0adf45d..af2dbc58d5b2eff3d0a49890a02bf98bbfc295c7 100644 --- a/tests/builtins/malloc.c +++ b/tests/builtins/malloc.c @@ -33,7 +33,7 @@ void main(int c) { int *mw = Frama_C_malloc_imprecise(42); *mw = 1; int *mw2 = Frama_C_malloc_imprecise(42); - *mw2 = 1; + *mw2 = 2; // *s = 1; } diff --git a/tests/builtins/oracle/malloc.res.oracle b/tests/builtins/oracle/malloc.res.oracle index b9dd7712077beb3d1ae0d7c36f6fca349eab835d..6bfbf908188b5a5853ee19749c30e75bcd07d56f 100644 --- a/tests/builtins/oracle/malloc.res.oracle +++ b/tests/builtins/oracle/malloc.res.oracle @@ -72,5 +72,5 @@ [1] ∈ UNINITIALIZED [2] ∈ {3} [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