From da5b382e3e895bd2c231e4b58a38ce680dfd187f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 21 Jan 2021 09:41:16 +0100
Subject: [PATCH] [Eva] Adds tests for the backward logical operators LAnd and
LOr.
---
tests/value/backward_arith.i | 45 +++++++++++++++
tests/value/oracle/backward_arith.res.oracle | 59 +++++++++++++++++---
2 files changed, 95 insertions(+), 9 deletions(-)
diff --git a/tests/value/backward_arith.i b/tests/value/backward_arith.i
index a26120d37e8..afe946261c3 100644
--- a/tests/value/backward_arith.i
+++ b/tests/value/backward_arith.i
@@ -1,4 +1,5 @@
/* run.config*
+ STDOPT: +"-keep-logical-operators"
*/
/* Test the soundness of arithmetic backward propagators. */
@@ -26,8 +27,52 @@ void unsigned_neg () {
Frama_C_show_each_smaller_than_minus_ten_but_zero(x); /* <= 4294967286 but 0 */
}
+void logical_operators () {
+ unsigned int x = nondet;
+ unsigned int y = nondet;
+ unsigned int a = x % 10;
+ unsigned int b = x % 10;
+
+ // Logical conjunction LAnd.
+ if (x < 11 && y < 21)
+ Frama_C_show_each("0..10", x, "0..20", y);
+ else
+ Frama_C_show_each("top", x, "top", y);
+ if (a < 10 && y < 10)
+ Frama_C_show_each("0..9", a, "0..9", y);
+ else
+ Frama_C_show_each("0..9", a, "10..max", y);
+ if (a > 10 && y < 10)
+ Frama_C_show_each("bottom", a, y);
+ else
+ Frama_C_show_each("0..9", a, "top", y);
+ if (a > 10 && b > 10)
+ Frama_C_show_each("bottom", a, b);
+ else
+ Frama_C_show_each("0..9", a, "0..9", b);
+
+ // Logical disjunction LOr.
+ if (x > 10 || y > 20)
+ Frama_C_show_each("top", x, "top", y);
+ else
+ Frama_C_show_each("0..10", x, "0..20", y);
+ if (a > 10 || y > 10)
+ Frama_C_show_each("0..9", a, "11..max", y);
+ else
+ Frama_C_show_each("0..9", a, "0..10", y);
+ if (a < 10 || y > 10)
+ Frama_C_show_each("0..9", a, "top", y);
+ else
+ Frama_C_show_each("bottom", a, y);
+ if (a > 10 || b > 10)
+ Frama_C_show_each("bottom", a, b);
+ else
+ Frama_C_show_each("0..9", a, "0..9", b);
+}
+
int main () {
unsigned_neg ();
+ logical_operators ();
return 0;
}
diff --git a/tests/value/oracle/backward_arith.res.oracle b/tests/value/oracle/backward_arith.res.oracle
index af34524c922..91015a23c5f 100644
--- a/tests/value/oracle/backward_arith.res.oracle
+++ b/tests/value/oracle/backward_arith.res.oracle
@@ -5,42 +5,83 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] computing for function unsigned_neg <- main.
- Called from tests/value/backward_arith.i:31.
-[eva] tests/value/backward_arith.i:12: Frama_C_show_each_ten: {10}
-[eva] tests/value/backward_arith.i:14:
+ Called from tests/value/backward_arith.i:75.
+[eva] tests/value/backward_arith.i:13: Frama_C_show_each_ten: {10}
+[eva] tests/value/backward_arith.i:15:
Frama_C_show_each_not_ten: [0..4294967295]
-[eva] tests/value/backward_arith.i:16:
+[eva] tests/value/backward_arith.i:17:
Frama_C_show_each_greater_than_ten_or_zero: [0..4294967295]
-[eva] tests/value/backward_arith.i:18:
+[eva] tests/value/backward_arith.i:19:
Frama_C_show_each_smaller_than_ten_but_zero: [1..10]
-[eva] tests/value/backward_arith.i:20: Frama_C_show_each_minus_ten: {4294967286}
-[eva] tests/value/backward_arith.i:22:
+[eva] tests/value/backward_arith.i:21: Frama_C_show_each_minus_ten: {4294967286}
+[eva] tests/value/backward_arith.i:23:
Frama_C_show_each_not_minus_ten: [0..4294967295]
-[eva] tests/value/backward_arith.i:24:
+[eva] tests/value/backward_arith.i:25:
Frama_C_show_each_greater_than_minus_ten_or_zero: [0..4294967295]
-[eva] tests/value/backward_arith.i:26:
+[eva] tests/value/backward_arith.i:27:
Frama_C_show_each_smaller_than_minus_ten_but_zero: [1..4294967286]
[eva] Recording results for unsigned_neg
[eva] Done for function unsigned_neg
+[eva] computing for function logical_operators <- main.
+ Called from tests/value/backward_arith.i:76.
+[eva] tests/value/backward_arith.i:38:
+ Frama_C_show_each: {{ "0..10" }}, [0..10], {{ "0..20" }}, [0..20]
+[eva] tests/value/backward_arith.i:40:
+ Frama_C_show_each: {{ "top" }}, [0..4294967295], {{ "top" }}, [0..4294967295]
+[eva] tests/value/backward_arith.i:42:
+ Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "0..9" }}, [0..9]
+[eva] tests/value/backward_arith.i:44:
+ Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "10..max" }}, [10..4294967295]
+[eva] tests/value/backward_arith.i:48:
+ Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "top" }}, [0..4294967295]
+[eva] tests/value/backward_arith.i:52:
+ Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "0..9" }}, [0..9]
+[eva] tests/value/backward_arith.i:56:
+ Frama_C_show_each: {{ "top" }}, [0..4294967295], {{ "top" }}, [0..4294967295]
+[eva] tests/value/backward_arith.i:58:
+ Frama_C_show_each: {{ "0..10" }}, [0..10], {{ "0..20" }}, [0..20]
+[eva] tests/value/backward_arith.i:60:
+ Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "11..max" }}, [11..4294967295]
+[eva] tests/value/backward_arith.i:62:
+ Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "0..10" }}, [0..10]
+[eva] tests/value/backward_arith.i:64:
+ Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "top" }}, [0..4294967295]
+[eva] tests/value/backward_arith.i:70:
+ Frama_C_show_each: {{ "0..9" }}, [0..9], {{ "0..9" }}, [0..9]
+[eva] Recording results for logical_operators
+[eva] Done for function logical_operators
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function logical_operators:
+ x ∈ [--..--]
+ y ∈ [--..--]
+ a ∈ [0..9]
+ b ∈ [0..9]
[eva:final-states] Values at end of function unsigned_neg:
x ∈ [--..--]
minus_ten ∈ {4294967286}
[eva:final-states] Values at end of function main:
__retres ∈ {0}
+[from] Computing for function logical_operators
+[from] Done for function logical_operators
[from] Computing for function unsigned_neg
[from] Done for function unsigned_neg
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
+[from] Function logical_operators:
+ NO EFFECTS
[from] Function unsigned_neg:
NO EFFECTS
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function logical_operators:
+ x; y; a; b
+[inout] Inputs for function logical_operators:
+ nondet
[inout] Out (internal) for function unsigned_neg:
x; minus_ten
[inout] Inputs for function unsigned_neg:
--
GitLab