From 24ddeaa9f517ec148085425d5b60401545dbabd2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 12 Jun 2024 09:58:01 +0200
Subject: [PATCH] [Eva] Adds a test of the memset builtin applied to a weak
base.
---
tests/builtins/memset.c | 23 ++++++-
tests/builtins/oracle/memset.res.oracle | 81 ++++++++++++++++++++++---
2 files changed, 93 insertions(+), 11 deletions(-)
diff --git a/tests/builtins/memset.c b/tests/builtins/memset.c
index 9c537d24550..0b42eac05f0 100644
--- a/tests/builtins/memset.c
+++ b/tests/builtins/memset.c
@@ -3,7 +3,7 @@
*/
#include "string.h"
-
+#include "stdlib.h"
int t1[100];
int t2[100];
@@ -89,7 +89,28 @@ void uninit() {
memset(x, 0, 4);
}
+typedef struct S {
+ int i;
+ char c;
+ int *ptr;
+} st;
+
+void memset_weak_base () {
+ int x;
+ /*@ eva_allocate fresh_weak; */
+ st *s = malloc(sizeof(st));
+ if (s == NULL) return;
+ s->i = 421;
+ s->c = 1;
+ s->ptr = &x;
+ memset(s, 0, sizeof(st));
+ int *q = s->ptr; /* As the base is weak, s->ptr must be 0 or &x.
+ This should not be a garbled mix. */
+ if (q != NULL) *q = 42; // This write should be valid.
+}
+
void main() {
test();
uninit();
+ memset_weak_base();
}
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index 81ad7400cbf..a6894e6df98 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -30,7 +30,7 @@
vol ∈ [--..--]
S_incomplete_type[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
[eva] computing for function test <- main.
- Called from memset.c:93.
+ Called from memset.c:113.
[eva] memset.c:33: Call to builtin memset
[eva] memset.c:33: function memset: precondition 'valid_s' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:151:
@@ -107,7 +107,7 @@
[from] Done for function test
[eva] Done for function test
[eva] computing for function uninit <- main.
- Called from memset.c:94.
+ Called from memset.c:114.
[eva:alarm] memset.c:85: Warning:
accessing uninitialized left-value. assert \initialized(&x);
[eva:alarm] memset.c:89: Warning:
@@ -118,12 +118,40 @@
[from] Computing for function uninit
[from] Done for function uninit
[eva] Done for function uninit
+[eva] computing for function memset_weak_base <- main.
+ Called from memset.c:115.
+[eva] memset.c:101: Call to builtin malloc
+[eva] memset.c:101: allocating weak variable __malloc_w_memset_weak_base_l101
+[eva] memset.c:106: Call to builtin memset
+[eva] memset.c:106: function memset: precondition 'valid_s' got status valid.
+[eva:imprecision] memset.c:106:
+ Call to builtin precise_memset(({{ (void *)&__malloc_w_memset_weak_base_l101 }},
+ {0},{12})) failed; destination is not exact
+[eva:alarm] memset.c:107: Warning:
+ accessing uninitialized left-value. assert \initialized(&s->ptr);
+[eva] Recording results for memset_weak_base
+[from] Computing for function memset_weak_base
+[from] Done for function memset_weak_base
+[eva] Done for function memset_weak_base
+[eva:locals-escaping] memset.c:115: Warning:
+ locals {x} escaping the scope of memset_weak_base through __malloc_w_memset_weak_base_l101
[eva] Recording results for main
[from] Computing for function main
[from] Done for function main
[eva] Done for function main
[eva] memset.c:85: assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function memset_weak_base:
+ __fc_heap_status ∈ [--..--]
+ x ∈ {42} or UNINITIALIZED
+ s ∈ {{ &__malloc_w_memset_weak_base_l101[0] }}
+ q ∈ {{ NULL ; &x }}
+ __malloc_w_memset_weak_base_l101[0].i ∈ {0; 421} or UNINITIALIZED
+ [0].c ∈ {0; 1} or UNINITIALIZED
+ [0].[bits 40 to 63] ∈
+ {0} or UNINITIALIZED
+ [0].ptr ∈
+ {{ NULL ; &x }} or UNINITIALIZED
[eva:final-states] Values at end of function test:
NULL[rbits 128 to 143] ∈ {66} repeated %8
[rbits 144 to 1927] ∈ [--..--]
@@ -188,6 +216,7 @@
[eva:final-states] Values at end of function main:
NULL[rbits 128 to 143] ∈ {66} repeated %8
[rbits 144 to 1927] ∈ [--..--]
+ __fc_heap_status ∈ [--..--]
t1[0..99] ∈ {286331153}
t2[0..99] ∈ {303174162}
t3[0..9] ∈ {0}
@@ -237,7 +266,19 @@
[4]{.f3; .f4[0..2]} ∈ {-16843010; 0}
S_incomplete_type[bits 0 to 7] ∈ {65}
[bits 8 to ..] ∈ [--..--] or UNINITIALIZED
+ __malloc_w_memset_weak_base_l101[0].i ∈ {0; 421} or UNINITIALIZED
+ [0].c ∈ {0; 1} or UNINITIALIZED
+ [0].[bits 40 to 63] ∈
+ {0} or UNINITIALIZED
+ [0].ptr ∈
+ {0} or UNINITIALIZED or ESCAPINGADDR
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
+[from] call to malloc at memset.c:101 (by memset_weak_base):
+ __fc_heap_status FROM __fc_heap_status; size (and SELF)
+ \result FROM __fc_heap_status; size
+[from] call to memset at memset.c:106 (by memset_weak_base):
+ __malloc_w_memset_weak_base_l101[0] FROM c (and SELF)
+ \result FROM s
[from] call to memset at memset.c:33 (by test):
t1[0..99] FROM c
\result FROM s
@@ -288,7 +329,7 @@
[from] call to memset at memset.c:89 (by uninit):
a FROM c
\result FROM s
-[from] call to test at memset.c:93 (by main):
+[from] call to test at memset.c:113 (by main):
NULL[16..17] FROM \nothing
t1[0..99] FROM \nothing
t2[0..99] FROM \nothing
@@ -306,10 +347,14 @@
t12[0..96] FROM \nothing (and SELF)
ts[0..4] FROM vol (and SELF)
S_incomplete_type[bits 0 to 7] FROM \nothing
-[from] call to uninit at memset.c:94 (by main):
+[from] call to uninit at memset.c:114 (by main):
NO EFFECTS
+[from] call to memset_weak_base at memset.c:115 (by main):
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+ __malloc_w_memset_weak_base_l101[0] FROM __fc_heap_status (and SELF)
[from] entry point:
NULL[16..17] FROM \nothing
+ __fc_heap_status FROM __fc_heap_status (and SELF)
t1[0..99] FROM \nothing
t2[0..99] FROM \nothing
t3[10..99] FROM \nothing (and SELF)
@@ -326,7 +371,19 @@
t12[0..96] FROM \nothing (and SELF)
ts[0..4] FROM vol (and SELF)
S_incomplete_type[bits 0 to 7] FROM \nothing
+ __malloc_w_memset_weak_base_l101[0] FROM __fc_heap_status (and SELF)
[from] ====== END OF CALLWISE DEPENDENCIES ======
+[inout] Out (internal) for function memset_weak_base:
+ __fc_heap_status; x; s; q; __malloc_w_memset_weak_base_l101[0]
+[inout] Inputs for function memset_weak_base:
+ __fc_heap_status; __malloc_w_memset_weak_base_l101[0].ptr
+[inout] InOut (internal) for function memset_weak_base:
+ Operational inputs:
+ __fc_heap_status; __malloc_w_memset_weak_base_l101[0].ptr
+ Operational inputs on termination:
+ __fc_heap_status; __malloc_w_memset_weak_base_l101[0].ptr
+ Sure outputs:
+ s; q
[inout] Out (internal) for function test:
NULL[16..17]; t1[0..99]; t2[0..99]; t3[10..99]; t4[1..99]; t5[0..99];
t6[10..13]; t7[0..3]; t8[0..3]; t9[20..99]; t10[4..12]; t11[2..6];
@@ -355,16 +412,20 @@
Sure outputs:
a
[inout] Out (internal) for function main:
- NULL[16..17]; t1[0..99]; t2[0..99]; t3[10..99]; t4[1..99]; t5[0..99];
- t6[10..13]; t7[0..3]; t8[0..3]; t9[20..99]; t10[4..12]; t11[2..6];
- t12[0..96]; ts[0..4]; S_incomplete_type[bits 0 to 7]
+ NULL[16..17]; __fc_heap_status; t1[0..99]; t2[0..99]; t3[10..99];
+ t4[1..99]; t5[0..99]; t6[10..13]; t7[0..3]; t8[0..3]; t9[20..99];
+ t10[4..12]; t11[2..6]; t12[0..96]; ts[0..4];
+ S_incomplete_type[bits 0 to 7]; __malloc_w_memset_weak_base_l101[0]
[inout] Inputs for function main:
- incomplete_type; vol
+ __fc_heap_status; incomplete_type; vol;
+ __malloc_w_memset_weak_base_l101[0].ptr
[inout] InOut (internal) for function main:
Operational inputs:
- incomplete_type; vol
+ __fc_heap_status; incomplete_type; vol;
+ __malloc_w_memset_weak_base_l101[0].ptr
Operational inputs on termination:
- incomplete_type; vol
+ __fc_heap_status; incomplete_type; vol;
+ __malloc_w_memset_weak_base_l101[0].ptr
Sure outputs:
NULL[16..17]; t1[0..99]; t2[0..99]; t5[0..99]; t8[0..3]; t10[4..6];
t11[3]; S_incomplete_type[bits 0 to 7]
--
GitLab