[Eva] Adds a test of the memset builtin applied to a weak base.

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();
 }

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]