Skip to content
Snippets Groups Projects
Commit bd5f3d57 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Splits test memcpy in two runs with different absolute valid range. 

The first run has no absolute valid range.
The second run only tests function copy_0 with absolute valid range.
parent e4231482
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/builtins/memcpy.c
+ 2
− 2
View file @ bd5f3d57
/* run.config*
PLUGIN: @PTEST_PLUGIN@ report
STDOPT: +"-calldeps -eva-msg-key imprecision -eva-plevel 150 -inout -no-deps -absolute-valid-range 100000-100001 -then -report"
STDOPT: +"-calldeps -eva-msg-key imprecision -eva-plevel 150 -inout -no-deps -then -report"
STDOPT: +"-absolute-valid-range 100000-100001 -main copy_0"
*/
#include "string.h"
volatile int i;
......
tests/builtins/oracle/memcpy.res.oracle → tests/builtins/oracle/memcpy.0.res.oracle
+ 18
− 64
View file @ bd5f3d57
......@@ -3,7 +3,6 @@
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
NULL[rbits 800000 to 800015] ∈ [--..--]
i ∈ [--..--]
src[0..19] ∈ {0}
dst1[0..19] ∈ {0}
......@@ -320,7 +319,6 @@
[eva] memcpy.c:216:
Frama_C_dump_each:
# cvalue:
NULL[rbits 800000 to 800015] ∈ [--..--]
__fc_heap_status ∈ [--..--]
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
......@@ -355,17 +353,14 @@
Called from memcpy.c:230.
[eva] memcpy.c:221: Call to builtin memcpy
[eva:alarm] memcpy.c:221: Warning:
function memcpy: precondition 'valid_dest' got status invalid.
[eva] memcpy.c:221:
function memcpy: no state left, precondition 'valid_src' got status valid.
[eva] memcpy.c:221:
function memcpy: no state left, precondition 'separation' got status valid.
function memcpy: precondition 'valid_dest' got status unknown.
[eva] memcpy.c:221: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:221: function memcpy: precondition 'separation' got status valid.
[eva] memcpy.c:222: Call to builtin memcpy
[eva] memcpy.c:222: function memcpy: precondition 'valid_dest' got status valid.
[eva:alarm] memcpy.c:222: Warning:
function memcpy: precondition 'valid_src' got status invalid.
[eva] memcpy.c:222:
function memcpy: no state left, precondition 'separation' got status valid.
function memcpy: precondition 'valid_src' got status unknown.
[eva] memcpy.c:222: function memcpy: precondition 'separation' got status valid.
[eva] Recording results for copy_0
[from] Computing for function copy_0
[from] Done for function copy_0
......@@ -861,8 +856,8 @@
ptop2[2..749]; ptop3[2..797]; ptop4[2..798]; garbledsize[10..99];
pgarbledsize; dstmaybesize1[0..14]; dstmaybesize2[0..5]; maybesize
[inout] Inputs for function test:
NULL[100000..100001]; i; src[0..19]; maybe; v1; v2;
v4{.x; .y; .p; .padding[0..3]}; t[0..3]; "d"[bits 0 to 7]
i; src[0..19]; maybe; v1; v2; v4{.x; .y; .p; .padding[0..3]}; t[0..3];
"d"[bits 0 to 7]
[inout] InOut (internal) for function test:
Operational inputs:
i; src[0..19]; maybe; v1{.p; .padding[0..23]}; v2;
......@@ -900,8 +895,8 @@
dst5[0..99]; tm[0..999]; um{[0..998]; [999][bits 0 to 15]}; ttyp[0..999];
v1{.x; .y}; v2; v3; v4; v5; t[1..3]
[inout] Inputs for function main:
NULL[100000..100001]; i; src[0..19]; maybe; v1; v2;
v4{.x; .y; .p; .padding[0..3]}; t[0..3]; "d"[bits 0 to 7]
i; src[0..19]; maybe; v1; v2; v4{.x; .y; .p; .padding[0..3]}; t[0..3];
"d"[bits 0 to 7]
[inout] InOut (internal) for function main:
Operational inputs:
i; src[0..19]; maybe; v1{.p; .padding[0..23]}; v2;
......@@ -1075,48 +1070,10 @@
--- Properties of Function 'memcpy'
--------------------------------------------------------------------------------
[ Alarm ] Pre-condition 'valid_dest'
By Call Preconditions, with pending:
- Unreachable call 'memcpy' (file memcpy.c, line 221)
- Instance of 'Pre-condition 'valid_dest'' of 'buggy' at call 'memcpy' (file memcpy.c, line 32)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 74)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 79)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 93)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 95)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 100)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 118)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 126)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 135)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 144)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 149)
- Instance of 'Pre-condition 'valid_dest'' of 'test' at call 'memcpy' (file memcpy.c, line 155)
[ Alarm ] Pre-condition 'valid_src'
By Call Preconditions, with pending:
- Unreachable call 'memcpy' (file memcpy.c, line 222)
- Instance of 'Pre-condition 'valid_src'' of 'test' at call 'memcpy' (file memcpy.c, line 74)
- Instance of 'Pre-condition 'valid_src'' of 'test' at call 'memcpy' (file memcpy.c, line 79)
- Instance of 'Pre-condition 'valid_src'' of 'test' at call 'memcpy' (file memcpy.c, line 91)
- Instance of 'Pre-condition 'valid_src'' of 'test' at call 'memcpy' (file memcpy.c, line 100)
- Instance of 'Pre-condition 'valid_src'' of 'test' at call 'memcpy' (file memcpy.c, line 149)
- Instance of 'Pre-condition 'valid_src'' of 'test' at call 'memcpy' (file memcpy.c, line 155)
[ - ] Pre-condition 'valid_dest'
tried with Call Preconditions.
[ - ] Pre-condition 'valid_src'
tried with Call Preconditions.
[ - ] Pre-condition 'separation'
tried with Call Preconditions.
[ Extern ] Post-condition 'copied_contents'
......@@ -2228,10 +2185,9 @@
--- Properties of Function 'copy_0'
--------------------------------------------------------------------------------
[ Alarm ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 221)
[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 221)
By Eva, with pending:
- Unreachable call 'memcpy' (file memcpy.c, line 221)
tried with Eva.
[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 221)
by Eva.
......@@ -2241,10 +2197,9 @@
[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 222)
by Eva.
[ Alarm ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 222)
[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 222)
By Eva, with pending:
- Unreachable call 'memcpy' (file memcpy.c, line 222)
tried with Eva.
[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 222)
by Eva.
......@@ -2255,7 +2210,6 @@
169 Completely validated
1 Locally validated
267 Considered valid
32 To be validated
4 Alarms emitted
36 To be validated
473 Total
--------------------------------------------------------------------------------
tests/builtins/oracle/memcpy.1.res.oracle 0 → 100644
+ 56
− 0
View file @ bd5f3d57
[kernel] Parsing memcpy.c (with preprocessing)
[eva] Analyzing a complete application starting at copy_0
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
NULL[rbits 800000 to 800015] ∈ [--..--]
i ∈ [--..--]
src[0..19] ∈ {0}
dst1[0..19] ∈ {0}
dst2[0..19] ∈ {0}
dst3[0..19] ∈ {0}
dst4[0..19] ∈ {0}
dst5[0..99] ∈ {0}
maybe ∈ [--..--]
tm[0..999] ∈ {0}
um[0..999] ∈ {0}
ttyp[0..999] ∈ {0}
v1 ∈ {0}
v2 ∈ {0}
v3 ∈ {0}
v4 ∈ {0}
v5 ∈ {0}
t[0..3] ∈ {0}
[eva] memcpy.c:221: Call to builtin memcpy
[eva:alarm] memcpy.c:221: Warning:
function memcpy: precondition 'valid_dest' got status invalid.
[eva] memcpy.c:221:
function memcpy: no state left, precondition 'valid_src' got status valid.
[eva] memcpy.c:221:
function memcpy: no state left, precondition 'separation' got status valid.
[eva] memcpy.c:222: Call to builtin memcpy
[eva] memcpy.c:222: function memcpy: precondition 'valid_dest' got status valid.
[eva:alarm] memcpy.c:222: Warning:
function memcpy: precondition 'valid_src' got status invalid.
[eva] memcpy.c:222:
function memcpy: no state left, precondition 'separation' got status valid.
[eva] Recording results for copy_0
[eva] Done for function copy_0
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function copy_0:
[from] Computing for function copy_0
[from] Computing for function memcpy <-copy_0
[from] Done for function memcpy
[from] Done for function copy_0
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function memcpy:
\result FROM dest
[from] Function copy_0:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function copy_0:
\nothing
[inout] Inputs for function copy_0:
i
tests/builtins/oracle_gauges/memcpy.res.oracle → tests/builtins/oracle_gauges/memcpy.0.res.oracle
+ 2
− 2
View file @ bd5f3d57
146a147,148
145a146,147
> [eva] memcpy.c:100: Call to builtin memcpy
> [eva] memcpy.c:100: Call to builtin memcpy
372a375
367a370
> [eva] memcpy.c:231: starting to merge loop iterations
tests/value/oracle_multidim/strings_logic.res.oracle deleted 100644 → 0
+ 0
− 0
View file @ e4231482
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment