From 210d963ee84c8d01701ff95d14db70a9d7395861 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 2 Apr 2020 12:33:57 +0200
Subject: [PATCH] [Eva] In the malloc test, tests that the base for the
imprecise builtin is weak.
---
tests/builtins/malloc.c | 2 +-
tests/builtins/oracle/malloc.res.oracle | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index af7f6c2470d..af2dbc58d5b 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 b9dd7712077..6bfbf908188 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
--
GitLab