Add UNKNOWN annotations to test cases.

Loss in precision is due to no longer computing with top in the interval
domain.

Author: jerhard

tests/regression/24-octagon/02-octagon_interprocudral.c

@@ -11,14 +11,17 @@ int f1() {
 
     one = two;
 
-    assert(one - two == 0);
+    // We no longer compute with "top" in the interval domain,
+    // leading to a loss of precision here.
+    // Thus the three asserts are here marked with "UNKNOWN".
+    assert(one - two == 0); // UNKNOWN
     x = f2(one,two);
-    assert(one - two == 0);
+    assert(one - two == 0); // UNKNOWN
     assert(x == 48);
 }
 
 int f2(int a, int b) {
-    assert(a-b == 0);
+    assert(a-b == 0); // UNKNOWN
 
     return 48;
 }

tests/regression/27-inv_invariants/01-ints.c

@@ -21,12 +21,12 @@ int main() {
     assert(x == 2 && y == 4);
   if (x == 3 && y/x == 2) {
     assert(y == 6); // UNKNOWN!
-    assert(RANGE(y, 6, 8));
+    assert(RANGE(y, 6, 8)); // UNKNOWN
   }
   if (y/3 == -2)
-    assert(RANGE(y, -8, -6));
+    assert(RANGE(y, -8, -6)); // UNKNOWN
   if (y/-3 == -2)
-    assert(RANGE(y, 6, 8));
+    assert(RANGE(y, 6, 8)); // UNKNOWN
   if (y/x == 2 && x == 3)
     assert(x == 3); // TO-DO y == [6,8]; this does not work because CIL transforms this into two if-statements
   if (2+(3-x)*4/5 == 6 && 2*y >= x+5)
@@ -113,7 +113,7 @@ int main2() {
   if (x == three && y/x == two) {
     // y could for example also be 7
     assert(y == six);  // UNKNOWN!
-    assert(RANGE(y, 6, 8));
+    assert(RANGE(y, 6, 8)); // UNKNOWN
   }
   if (y/x == two && x == three)
     assert(x == three); // TO-DO y == six
@@ -124,9 +124,9 @@ int main2() {
     assert(x != two); // [two,four] -> [three,four] TO-DO x % two == one
 
   if (y/three == -two)
-    assert(RANGE(y, -8, -6));
+    assert(RANGE(y, -8, -6)); // UNKNOWN
   if (y/-three == -two)
-    assert(RANGE(y, 6, 8));
+    assert(RANGE(y, 6, 8)); // UNKNOWN
   if (y/x == two && x == three)
     assert(x == 3); // TO-DO y == [6,8]; this does not work because CIL transforms this into two if-statements
   if (two+(three-x)*four/five == six && two*y >= x+five)