🔊 div by zero should not lead to bot, but top and a warning about UB

jerhard · Jul 2, 2019 · cfbad0d · cfbad0d
1 parent bd9e16e
commit cfbad0d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
@@ -279,7 +279,7 @@ struct
     | None, _ | _, None -> bot ()
     | Some (x1,x2), Some (y1,y2) ->
       begin match y1, y2 with
-        | 0L, 0L       -> bot ()
+        | 0L, 0L       -> top () (* TODO warn about undefined behavior *)
         | 0L, _        -> div (Some (x1,x2)) (Some (1L,y2))
         | _      , 0L  -> div (Some (x1,x2)) (Some (y1,(-1L)))
         | _ when leq (of_int 0L) (Some (y1,y2)) -> top ()