Make binary float comparison unknown result bounds more precise

Author: sim642

src/analyses/base.ml

@@ -185,7 +185,7 @@ struct
       @see C11 7.12.14, 6.5.8, 6.5.9 *)
   let fd_binary_pred = function
     | Some b -> ID.of_bool IInt b
-    | None -> ID.top_of IInt (* TODO: [0,1] interval instead? *)
+    | None -> ID.of_interval IInt (Z.zero, Z.one)
 
   let unop_ID = function
     | Neg  -> ID.neg

tests/regression/57-floats/01-base.c

@@ -25,8 +25,8 @@ int main()
 
     __goblint_check((a < 10.) == 1);
     __goblint_check((a > 10.) == 0);
-    __goblint_check((x == 2.) >= 0); // TODO
-    __goblint_check((x == 2.) <= 1); // TODO
+    __goblint_check((x == 2.) >= 0);
+    __goblint_check((x == 2.) <= 1);
 
     __goblint_check(c == 2.f); // SUCCESS
     __goblint_check(c < 10.f); // SUCCESS