diff --git a/tests/builtins/memset.c b/tests/builtins/memset.c
index 82180e3f7d88b373b894aaa2523f79442aafe547..9c537d24550636043bb34e9e7001e9820bcf01ea 100644
--- a/tests/builtins/memset.c
+++ b/tests/builtins/memset.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-calldeps -eva-msg-key imprecision -eva-plevel 500" +"-inout -no-deps"
+ STDOPT: #"-calldeps -eva-msg-key imprecision -eva-plevel 500 -absolute-valid-range 0x10-0xf0" +"-inout -no-deps"
*/
#include "string.h"
@@ -26,7 +26,7 @@ struct s {
};
struct s ts[5];
-
+extern struct incomplete *incomplete_type;
volatile int vol;
void test() {
@@ -70,6 +70,11 @@ void test() {
unsigned k = vol;
//@ assert Assume: k <= 12;
memset(t12+k*8, 1, 4); // Imprecise, because of double congruences
+
+ memset(t1, 1, 0); // size is negative or null
+ memset(incomplete_type, 'A', 1); // destination type and size differ
+ char *absolute_valid_range = (char*)0x10;
+ memset(absolute_valid_range, 'B', 2); // destination has an unknown form
}
/* Should not crash and emit uninitialization alarms.
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index e84b5ca2b9125c6efbc99d87ce1fc28430633b12..f8bbb7519d819bd62c5c137bd158eadb4393d62a 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -4,8 +4,15 @@
'char' and 'int')
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
+[eva:initial-state]
+ creating variable S_incomplete_type with imprecise size (type struct incomplete [2])
+[eva:unknown-size] memset.c:29: Warning:
+ during initialization of variable 'incomplete_type', size of
+ type 'struct incomplete' cannot be computed
+ (abstract type 'struct incomplete')
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
+ NULL[rbits 128 to 1927] ∈ [--..--]
t1[0..99] ∈ {0}
t2[0..99] ∈ {0}
t3[0..99] ∈ {0}
@@ -19,9 +26,11 @@
t11[0..99] ∈ {0}
t12[0..99] ∈ {0}
ts[0..4] ∈ {0}
+ incomplete_type ∈ {{ NULL ; (struct incomplete *)&S_incomplete_type }}
vol ∈ [--..--]
+ S_incomplete_type[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
[eva] computing for function test <- main.
- Called from memset.c:88.
+ Called from memset.c:93.
[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:134:
@@ -79,18 +88,32 @@
[eva] memset.c:72: function memset: precondition 'valid_s' got status valid.
[eva:imprecision] memset.c:72:
Call to builtin precise_memset(({{ &t12 + [0..384],0%32 }},{1},{4})) failed; destination is not exact
+[eva] memset.c:74: Call to builtin memset
+[eva] memset.c:74: function memset: precondition 'valid_s' got status valid.
+[eva:imprecision] memset.c:74:
+ Call to builtin precise_memset(({{ (void *)&t1 }},{1},{0})) failed; size is negative or null
+[eva] memset.c:75: Call to builtin memset
+[eva:alarm] memset.c:75: Warning:
+ function memset: precondition 'valid_s' got status unknown.
+[eva:imprecision] memset.c:75:
+ Call to builtin precise_memset(({{ NULL ; (void *)&S_incomplete_type }},
+ {65},{1})) failed; destination type and size differ
+[eva] memset.c:77: Call to builtin memset
+[eva] memset.c:77: function memset: precondition 'valid_s' got status valid.
+[eva:imprecision] memset.c:77:
+ Call to builtin precise_memset(({16},{66},{2})) failed; destination has an unknown form
[eva] Recording results for test
[from] Computing for function test
[from] Done for function test
[eva] Done for function test
[eva] computing for function uninit <- main.
- Called from memset.c:89.
-[eva:alarm] memset.c:80: Warning:
+ Called from memset.c:94.
+[eva:alarm] memset.c:85: Warning:
accessing uninitialized left-value. assert \initialized(&x);
-[eva:alarm] memset.c:84: Warning:
+[eva:alarm] memset.c:89: Warning:
accessing uninitialized left-value. assert \initialized(&x);
-[eva] memset.c:84: Call to builtin memset
-[eva] memset.c:84: function memset: precondition 'valid_s' got status valid.
+[eva] memset.c:89: Call to builtin memset
+[eva] memset.c:89: function memset: precondition 'valid_s' got status valid.
[eva] Recording results for uninit
[from] Computing for function uninit
[from] Done for function uninit
@@ -99,9 +122,11 @@
[from] Computing for function main
[from] Done for function main
[eva] Done for function main
-[eva] memset.c:80: assertion 'Eva,initialization' got final status invalid.
+[eva] memset.c:85: assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function test:
+ NULL[rbits 128 to 143] ∈ {66} repeated %8
+ [rbits 144 to 1927] ∈ [--..--]
t1[0..99] ∈ {286331153}
t2[0..99] ∈ {303174162}
t3[0..9] ∈ {0}
@@ -154,10 +179,15 @@
s ∈ {12; 36}
s1 ∈ {8; 16}
k ∈ [0..12]
+ absolute_valid_range ∈ {16}
+ S_incomplete_type[bits 0 to 7] ∈ {65}
+ [bits 8 to ..] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function uninit:
x ∈ {{ (void *)&a }}
a ∈ {0}
[eva:final-states] Values at end of function main:
+ NULL[rbits 128 to 143] ∈ {66} repeated %8
+ [rbits 144 to 1927] ∈ [--..--]
t1[0..99] ∈ {286331153}
t2[0..99] ∈ {303174162}
t3[0..9] ∈ {0}
@@ -205,6 +235,8 @@
[4].[bits 8 to 15] ∈ {0; 254}
[4].f2 ∈ {-258; 0}
[4]{.f3; .f4[0..2]} ∈ {-16843010; 0}
+ S_incomplete_type[bits 0 to 7] ∈ {65}
+ [bits 8 to ..] ∈ [--..--] or UNINITIALIZED
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to memset at memset.c:33 (by test):
t1[0..99] FROM c
@@ -245,10 +277,19 @@
[from] call to memset at memset.c:72 (by test):
t12[0..96] FROM c (and SELF)
\result FROM s
-[from] call to memset at memset.c:84 (by uninit):
+[from] call to memset at memset.c:74 (by test):
+ \result FROM s
+[from] call to memset at memset.c:75 (by test):
+ S_incomplete_type[bits 0 to 7] FROM c
+ \result FROM s
+[from] call to memset at memset.c:77 (by test):
+ NULL[16..17] FROM c
+ \result FROM s
+[from] call to memset at memset.c:89 (by uninit):
a FROM c
\result FROM s
-[from] call to test at memset.c:88 (by main):
+[from] call to test at memset.c:93 (by main):
+ NULL[16..17] FROM \nothing
t1[0..99] FROM \nothing
t2[0..99] FROM \nothing
t3[10..99] FROM \nothing (and SELF)
@@ -264,9 +305,11 @@
[3] FROM \nothing
t12[0..96] FROM \nothing (and SELF)
ts[0..4] FROM vol (and SELF)
-[from] call to uninit at memset.c:89 (by main):
+ S_incomplete_type[bits 0 to 7] FROM \nothing
+[from] call to uninit at memset.c:94 (by main):
NO EFFECTS
[from] entry point:
+ NULL[16..17] FROM \nothing
t1[0..99] FROM \nothing
t2[0..99] FROM \nothing
t3[10..99] FROM \nothing (and SELF)
@@ -282,21 +325,24 @@
[3] FROM \nothing
t12[0..96] FROM \nothing (and SELF)
ts[0..4] FROM vol (and SELF)
+ S_incomplete_type[bits 0 to 7] FROM \nothing
[from] ====== END OF CALLWISE DEPENDENCIES ======
[inout] Out (internal) for function test:
- 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]; dst; p; tmp_0; s; s1; k
+ 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]; dst; p; tmp_0; s; s1; k; absolute_valid_range;
+ S_incomplete_type[bits 0 to 7]
[inout] Inputs for function test:
- vol
+ incomplete_type; vol
[inout] InOut (internal) for function test:
Operational inputs:
- vol
+ incomplete_type; vol
Operational inputs on termination:
- vol
+ incomplete_type; vol
Sure outputs:
- t1[0..99]; t2[0..99]; t5[0..99]; t8[0..3]; t10[4..6]; t11[3]; dst;
- p; tmp_0; s; s1; k
+ NULL[16..17]; t1[0..99]; t2[0..99]; t5[0..99]; t8[0..3]; t10[4..6];
+ t11[3]; dst; p; tmp_0; s; s1; k; absolute_valid_range;
+ S_incomplete_type[bits 0 to 7]
[inout] Out (internal) for function uninit:
x; a
[inout] Inputs for function uninit:
@@ -309,15 +355,16 @@
Sure outputs:
a
[inout] Out (internal) for function main:
- 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]
+ 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]
[inout] Inputs for function main:
- vol
+ incomplete_type; vol
[inout] InOut (internal) for function main:
Operational inputs:
- vol
+ incomplete_type; vol
Operational inputs on termination:
- vol
+ incomplete_type; vol
Sure outputs:
- t1[0..99]; t2[0..99]; t5[0..99]; t8[0..3]; t10[4..6]; t11[3]
+ 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]