From c23684abfcf531b32d2dbeb7f6aa34e871c90c5e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 17 Apr 2019 17:03:10 +0200
Subject: [PATCH] [Eva] Adds a test of the bitwise domain.
---
tests/value/bitwise.i | 12 +++++++++
tests/value/diff_bitwise | 8 ++++++
tests/value/oracle/bitwise.res.oracle | 35 +++++++++++++++++++--------
3 files changed, 45 insertions(+), 10 deletions(-)
diff --git a/tests/value/bitwise.i b/tests/value/bitwise.i
index 7803ea7f36d..10db311b22c 100644
--- a/tests/value/bitwise.i
+++ b/tests/value/bitwise.i
@@ -134,6 +134,17 @@ void bug4() {
}
}
+/* See issue #639 and merge request #2230 on the bitwise domain. */
+void bug5() {
+ int x = v;
+ x = x | 2;
+ if (x == 8) {
+ x = x & 2; /* This branch is dead, but the bitwise domain leads to bottom
+ only after the operation x&2 and not before. */
+ Frama_C_show_each_dead(x);
+ }
+}
+
void main(void) {
test1();
test2();
@@ -145,4 +156,5 @@ void main(void) {
bug2();
bug3();
bug4();
+ bug5();
}
diff --git a/tests/value/diff_bitwise b/tests/value/diff_bitwise
index be860471315..fbafb12ebb8 100644
--- a/tests/value/diff_bitwise
+++ b/tests/value/diff_bitwise
@@ -23,6 +23,14 @@ diff tests/value/oracle/addition.res.oracle tests/value/oracle_bitwise/addition.
< (origin: Arithmetic {tests/value/addition.i:52}) }}
---
> p10 ∈ {{ garbled mix of &{p1} }}
+diff tests/value/oracle/bitwise.res.oracle tests/value/oracle_bitwise/bitwise.res.oracle
+79c79,82
+< [eva] tests/value/bitwise.i:144: Frama_C_show_each_dead: {0}
+---
+> [eva] tests/value/bitwise.i:142:
+> The evaluation of the expression x & 2
+> led to bottom without alarms:
+> at this point the product of states has no possible concretization.
diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_bitwise/bitwise_pointer.res.oracle
32,34c32
< [eva] tests/value/bitwise_pointer.i:18:
diff --git a/tests/value/oracle/bitwise.res.oracle b/tests/value/oracle/bitwise.res.oracle
index 29d9bbe2322..3ec23cec4bf 100644
--- a/tests/value/oracle/bitwise.res.oracle
+++ b/tests/value/oracle/bitwise.res.oracle
@@ -7,7 +7,7 @@
input[0..2] ∈ [--..--]
s ∈ [--..--]
[eva] computing for function test1 <- main.
- Called from tests/value/bitwise.i:138.
+ Called from tests/value/bitwise.i:149.
[eva] computing for function Frama_C_interval <- test1 <- main.
Called from tests/value/bitwise.i:23.
[eva] using specification for function Frama_C_interval
@@ -21,18 +21,18 @@
[eva] Recording results for test1
[eva] Done for function test1
[eva] computing for function test2 <- main.
- Called from tests/value/bitwise.i:139.
+ Called from tests/value/bitwise.i:150.
[eva] computing for function Frama_C_interval <- test2 <- main.
Called from tests/value/bitwise.i:50.
[eva] Done for function Frama_C_interval
[eva] Recording results for test2
[eva] Done for function test2
[eva] computing for function test3 <- main.
- Called from tests/value/bitwise.i:140.
+ Called from tests/value/bitwise.i:151.
[eva] Recording results for test3
[eva] Done for function test3
[eva] computing for function test4 <- main.
- Called from tests/value/bitwise.i:141.
+ Called from tests/value/bitwise.i:152.
[eva] tests/value/bitwise.i:62: assertion got status valid.
[eva] tests/value/bitwise.i:64: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
[eva] tests/value/bitwise.i:64:
@@ -45,35 +45,40 @@
[eva] Recording results for test4
[eva] Done for function test4
[eva] computing for function and_or_rel <- main.
- Called from tests/value/bitwise.i:142.
+ Called from tests/value/bitwise.i:153.
[eva:alarm] tests/value/bitwise.i:87: Warning: assertion got status unknown.
[eva] Recording results for and_or_rel
[eva] Done for function and_or_rel
[eva] computing for function double_neg <- main.
- Called from tests/value/bitwise.i:143.
+ Called from tests/value/bitwise.i:154.
[eva] Recording results for double_neg
[eva] Done for function double_neg
[eva] computing for function bug1 <- main.
- Called from tests/value/bitwise.i:144.
+ Called from tests/value/bitwise.i:155.
[eva] Recording results for bug1
[eva] Done for function bug1
[eva] computing for function bug2 <- main.
- Called from tests/value/bitwise.i:145.
+ Called from tests/value/bitwise.i:156.
[eva] tests/value/bitwise.i:114: Frama_C_show_each_then:
[eva] tests/value/bitwise.i:114: Frama_C_show_each_else:
[eva] Recording results for bug2
[eva] Done for function bug2
[eva] computing for function bug3 <- main.
- Called from tests/value/bitwise.i:146.
+ Called from tests/value/bitwise.i:157.
[eva] tests/value/bitwise.i:121: Frama_C_show_each: {0x41F656F}, {0xFBE09A91}
[eva] Recording results for bug3
[eva] Done for function bug3
[eva] computing for function bug4 <- main.
- Called from tests/value/bitwise.i:147.
+ Called from tests/value/bitwise.i:158.
[eva] tests/value/bitwise.i:131: Frama_C_show_each_then:
[eva] tests/value/bitwise.i:133: Frama_C_show_each_else:
[eva] Recording results for bug4
[eva] Done for function bug4
+[eva] computing for function bug5 <- main.
+ Called from tests/value/bitwise.i:159.
+[eva] tests/value/bitwise.i:144: Frama_C_show_each_dead: {0}
+[eva] Recording results for bug5
+[eva] Done for function bug5
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -96,6 +101,8 @@
[eva:final-states] Values at end of function bug4:
g_2 ∈ {-1; 0}
tmp_0 ∈ {-0x1578}
+[eva:final-states] Values at end of function bug5:
+ x ∈ [-0x7FFFFFFE..0x7FFFFFFF]
[eva:final-states] Values at end of function double_neg:
i ∈ {5}
j ∈ {0xFFFFFFFA}
@@ -141,6 +148,8 @@
[from] Done for function bug3
[from] Computing for function bug4
[from] Done for function bug4
+[from] Computing for function bug5
+[from] Done for function bug5
[from] Computing for function double_neg
[from] Done for function double_neg
[from] Computing for function test1
@@ -169,6 +178,8 @@
NO EFFECTS
[from] Function bug4:
NO EFFECTS
+[from] Function bug5:
+ NO EFFECTS
[from] Function double_neg:
NO EFFECTS
[from] Function test1:
@@ -202,6 +213,10 @@
g_2; tmp; tmp_0
[inout] Inputs for function bug4:
v
+[inout] Out (internal) for function bug5:
+ x
+[inout] Inputs for function bug5:
+ v
[inout] Out (internal) for function double_neg:
i; j; k
[inout] Inputs for function double_neg:
--
GitLab