From bd5f3d578f4dc84ed05bf29ebd166bc8aec491f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 20 Jun 2024 11:43:42 +0200
Subject: [PATCH] [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.
---
tests/builtins/memcpy.c | 4 +-
...{memcpy.res.oracle => memcpy.0.res.oracle} | 82 ++++---------------
tests/builtins/oracle/memcpy.1.res.oracle | 56 +++++++++++++
...{memcpy.res.oracle => memcpy.0.res.oracle} | 4 +-
.../oracle_multidim/strings_logic.res.oracle | 0
5 files changed, 78 insertions(+), 68 deletions(-)
rename tests/builtins/oracle/{memcpy.res.oracle => memcpy.0.res.oracle} (96%)
create mode 100644 tests/builtins/oracle/memcpy.1.res.oracle
rename tests/builtins/oracle_gauges/{memcpy.res.oracle => memcpy.0.res.oracle} (87%)
delete mode 100644 tests/value/oracle_multidim/strings_logic.res.oracle
diff --git a/tests/builtins/memcpy.c b/tests/builtins/memcpy.c
index 86d8e5e99e4..1eee41ee76b 100644
--- a/tests/builtins/memcpy.c
+++ b/tests/builtins/memcpy.c
@@ -1,9 +1,9 @@
/* 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;
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.0.res.oracle
similarity index 96%
rename from tests/builtins/oracle/memcpy.res.oracle
rename to tests/builtins/oracle/memcpy.0.res.oracle
index 081d95dc470..774d89fc40d 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.0.res.oracle
@@ -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
--------------------------------------------------------------------------------
diff --git a/tests/builtins/oracle/memcpy.1.res.oracle b/tests/builtins/oracle/memcpy.1.res.oracle
new file mode 100644
index 00000000000..ebc79e7b2b7
--- /dev/null
+++ b/tests/builtins/oracle/memcpy.1.res.oracle
@@ -0,0 +1,56 @@
+[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
diff --git a/tests/builtins/oracle_gauges/memcpy.res.oracle b/tests/builtins/oracle_gauges/memcpy.0.res.oracle
similarity index 87%
rename from tests/builtins/oracle_gauges/memcpy.res.oracle
rename to tests/builtins/oracle_gauges/memcpy.0.res.oracle
index 53b9be93013..5e4fbca1c4a 100644
--- a/tests/builtins/oracle_gauges/memcpy.res.oracle
+++ b/tests/builtins/oracle_gauges/memcpy.0.res.oracle
@@ -1,5 +1,5 @@
-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
diff --git a/tests/value/oracle_multidim/strings_logic.res.oracle b/tests/value/oracle_multidim/strings_logic.res.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
--
GitLab