From f587fe2b84d80d638b7bb3544e1b4f10d859e401 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 9 Apr 2020 18:05:58 +0200
Subject: [PATCH] [Eva] Add test case on logic inputs for memexec.
---
tests/value/memexec.c | 16 ++++++-
tests/value/oracle/memexec.res.oracle | 63 ++++++++++++++++++++++-----
2 files changed, 65 insertions(+), 14 deletions(-)
diff --git a/tests/value/memexec.c b/tests/value/memexec.c
index 092a4180c8d..e68abd5fbbd 100644
--- a/tests/value/memexec.c
+++ b/tests/value/memexec.c
@@ -2,7 +2,7 @@
STDOPT: #" -no-eva -rte-select fbug -rte -then -eva"
*/
-int x1, y1, z1; volatile int c;
+int x1, y1, z1, z2; volatile int c, nondet;
void f11() {
x1 = 1;
@@ -111,7 +111,7 @@ void f5() {
g_f5_2 = c;
arg = c;
f5_aux(arg);
- Frama_C_show_each_f5(arg, g_f5_1, g_f5_2); // Cache, but reduce g_f5_* and arg after the call. Currently does not work for g_f5_1, because dependencies are not taken into account
+ Frama_C_show_each_f5(arg, g_f5_1, g_f5_2); // Cache, but reduce g_f5_* and arg after the call.
}
struct two_fields { int x; int y; } two_fields;
@@ -150,6 +150,17 @@ void f8() {
f8_1(&x);
}
+void f9_1() {
+ /*@ assert z2 == 0; */
+}
+
+void f9() {
+ z2 = 1;
+ if (nondet) f9_1();
+ z2 = 0;
+ f9_1();
+}
+
void main () {
f1 ();
f2 ();
@@ -160,4 +171,5 @@ void main () {
f6();
f7();
f8();
+ f9();
}
diff --git a/tests/value/oracle/memexec.res.oracle b/tests/value/oracle/memexec.res.oracle
index f24a2a45c79..8390c51eeb4 100644
--- a/tests/value/oracle/memexec.res.oracle
+++ b/tests/value/oracle/memexec.res.oracle
@@ -7,7 +7,9 @@
x1 ∈ {0}
y1 ∈ {0}
z1 ∈ {0}
+ z2 ∈ {0}
c ∈ [--..--]
+ nondet ∈ [--..--]
p ∈ {0}
i ∈ {0}
t[0..9] ∈ {0}
@@ -17,7 +19,7 @@
g_f5_2 ∈ {0}
two_fields ∈ {0}
[eva] computing for function f1 <- main.
- Called from tests/value/memexec.c:154.
+ Called from tests/value/memexec.c:165.
[eva] computing for function f11 <- f1 <- main.
Called from tests/value/memexec.c:12.
[eva] Recording results for f11
@@ -31,15 +33,15 @@
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
- Called from tests/value/memexec.c:155.
+ Called from tests/value/memexec.c:166.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
- Called from tests/value/memexec.c:156.
+ Called from tests/value/memexec.c:167.
[eva] Recording results for f3
[eva] Done for function f3
[eva] computing for function bug <- main.
- Called from tests/value/memexec.c:157.
+ Called from tests/value/memexec.c:168.
[eva] computing for function fbug <- bug <- main.
Called from tests/value/memexec.c:40.
[eva:alarm] tests/value/memexec.c:33: Warning:
@@ -53,10 +55,10 @@
[eva] Done for function fbug
[eva] Recording results for bug
[eva] Done for function bug
-[eva:locals-escaping] tests/value/memexec.c:157: Warning:
+[eva:locals-escaping] tests/value/memexec.c:168: Warning:
locals {x} escaping the scope of bug through p
[eva] computing for function f4 <- main.
- Called from tests/value/memexec.c:158.
+ Called from tests/value/memexec.c:169.
[eva] computing for function f4_2 <- f4 <- main.
Called from tests/value/memexec.c:84.
[eva] computing for function f4_11 <- f4_2 <- f4 <- main.
@@ -92,7 +94,7 @@
[eva] Recording results for f4
[eva] Done for function f4
[eva] computing for function f5 <- main.
- Called from tests/value/memexec.c:159.
+ Called from tests/value/memexec.c:170.
[eva] computing for function f5_aux <- f5 <- main.
Called from tests/value/memexec.c:107.
[eva:alarm] tests/value/memexec.c:94: Warning: assertion got status unknown.
@@ -107,7 +109,7 @@
[eva] Recording results for f5
[eva] Done for function f5
[eva] computing for function f6 <- main.
- Called from tests/value/memexec.c:160.
+ Called from tests/value/memexec.c:171.
[eva] computing for function f6_1 <- f6 <- main.
Called from tests/value/memexec.c:123.
[eva] Recording results for f6_1
@@ -119,7 +121,7 @@
[eva] Recording results for f6
[eva] Done for function f6
[eva] computing for function f7 <- main.
- Called from tests/value/memexec.c:161.
+ Called from tests/value/memexec.c:172.
[eva] computing for function f7_1 <- f7 <- main.
Called from tests/value/memexec.c:136.
[eva] Recording results for f7_1
@@ -128,7 +130,7 @@
[eva] Recording results for f7
[eva] Done for function f7
[eva] computing for function f8 <- main.
- Called from tests/value/memexec.c:162.
+ Called from tests/value/memexec.c:173.
[eva] computing for function f8_1 <- f8 <- main.
Called from tests/value/memexec.c:147.
[eva:alarm] tests/value/memexec.c:141: Warning:
@@ -142,6 +144,21 @@
[eva] tests/value/memexec.c:150: Reusing old results for call to f8_1
[eva] Recording results for f8
[eva] Done for function f8
+[eva] computing for function f9 <- main.
+ Called from tests/value/memexec.c:174.
+[eva] computing for function f9_1 <- f9 <- main.
+ Called from tests/value/memexec.c:159.
+[eva:alarm] tests/value/memexec.c:154: Warning:
+ assertion got status invalid (stopping propagation).
+[eva] Recording results for f9_1
+[eva] Done for function f9_1
+[eva] computing for function f9_1 <- f9 <- main.
+ Called from tests/value/memexec.c:161.
+[eva] tests/value/memexec.c:154: assertion got status valid.
+[eva] Recording results for f9_1
+[eva] Done for function f9_1
+[eva] Recording results for f9
+[eva] Done for function f9
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -208,6 +225,10 @@
q ∈ {0}
[eva:final-states] Values at end of function f8:
x ∈ {1}
+[eva:final-states] Values at end of function f9_1:
+
+[eva:final-states] Values at end of function f9:
+ z2 ∈ {0}
[eva:final-states] Values at end of function fbug:
__retres ∈ {1}
[eva:final-states] Values at end of function bug:
@@ -215,6 +236,7 @@
x ∈ {1}
[eva:final-states] Values at end of function main:
x1 ∈ {1}
+ z2 ∈ {0}
p ∈ ESCAPINGADDR
i ∈ {0; 5}
t[0..1] ∈ {0}
@@ -263,6 +285,10 @@
[from] Done for function f8_1
[from] Computing for function f8
[from] Done for function f8
+[from] Computing for function f9_1
+[from] Done for function f9_1
+[from] Computing for function f9
+[from] Done for function f9
[from] Computing for function fbug
[from] Done for function fbug
[from] Computing for function bug
@@ -310,12 +336,17 @@
NO EFFECTS
[from] Function f8:
NO EFFECTS
+[from] Function f9_1:
+ NO EFFECTS
+[from] Function f9:
+ z2 FROM \nothing
[from] Function fbug:
\result FROM p; x
[from] Function bug:
p FROM \nothing
[from] Function main:
x1 FROM \nothing
+ z2 FROM \nothing
p FROM \nothing
i FROM c (and SELF)
t{[2]; [5..6]} FROM c (and SELF)
@@ -389,6 +420,14 @@
x
[inout] Inputs for function f8:
c
+[inout] Out (internal) for function f9_1:
+ \nothing
+[inout] Inputs for function f9_1:
+ \nothing
+[inout] Out (internal) for function f9:
+ z2
+[inout] Inputs for function f9:
+ nondet
[inout] Out (internal) for function fbug:
__retres
[inout] Inputs for function fbug:
@@ -398,6 +437,6 @@
[inout] Inputs for function bug:
c; p
[inout] Out (internal) for function main:
- x1; p; i; t{[2]; [5..6]}; ps; S[8]; g_f5_1; g_f5_2; two_fields
+ x1; z2; p; i; t{[2]; [5..6]}; ps; S[8]; g_f5_1; g_f5_2; two_fields
[inout] Inputs for function main:
- c; p; i; ps; S[8]; g_f5_1; g_f5_2
+ c; nondet; p; i; ps; S[8]; g_f5_1; g_f5_2
--
GitLab