[Eva] Adds tests for the backward logical operators LAnd and LOr.

tests/value/backward_arith.i

 /* 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;
 }

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: