Division by zero messages

src/analyses/base.ml

@@ -200,8 +200,24 @@ struct
     | PlusA -> ID.add
     | MinusA -> ID.sub
     | Mult -> ID.mul
-    | Div -> ID.div
-    | Mod -> ID.rem
+    | Div -> 
+      fun x y ->
+        (match ID.equal_to Z.zero y with
+         | `Eq ->
+           M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division is zero"
+         | `Top ->
+           M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division might be zero"
+         | `Neq -> ());
+        ID.div x y
+    | Mod -> 
+      fun x y ->
+        (match ID.equal_to Z.zero y with
+         | `Eq ->
+           M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo is zero"
+         | `Top ->
+           M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo might be zero"
+         | `Neq -> ());
+        ID.rem x y
     | Lt -> ID.lt
     | Gt -> ID.gt
     | Le -> ID.le

src/cdomain/value/cdomains/int/intervalDomain.ml

@@ -296,7 +296,7 @@ struct
       begin
         let is_zero v = Ints_t.compare v Ints_t.zero = 0 in
         match y1, y2 with
-        | l, u when is_zero l && is_zero u -> (top_of ik,{underflow=false; overflow=false}) (* TODO warn about undefined behavior *)
+        | l, u when is_zero l && is_zero u -> (top_of ik,{underflow=false; overflow=false})
         | l, _ when is_zero l              -> div ik (Some (x1,x2)) (Some (Ints_t.one,y2))
         | _, u when is_zero u              -> div ik (Some (x1,x2)) (Some (y1, Ints_t.(neg one)))
         | _ when leq (of_int ik (Ints_t.zero) |> fst) (Some (y1,y2)) -> (top_of ik,{underflow=false; overflow=false})

src/cdomain/value/cdomains/int/intervalSetDomain.ml

@@ -362,7 +362,7 @@ struct
       let top_of ik = top_of ik |> List.hd in
       let is_zero v = v =. Ints_t.zero in
       match y1, y2 with
-      | l, u when is_zero l && is_zero u -> top_of ik (* TODO warn about undefined behavior *)
+      | l, u when is_zero l && is_zero u -> top_of ik
       | l, _ when is_zero l              -> interval_div x (Ints_t.one,y2)
       | _, u when is_zero u              -> interval_div x (y1, Ints_t.(neg one))
       | _ when leq (of_int ik (Ints_t.zero) |> fst) ([(y1,y2)]) -> top_of ik

tests/regression/01-cpa/78-divbyzero.c

@@ -0,0 +1,13 @@
+// PARAM: --enable ana.int.interval
+
+int main(void) {
+
+	int a = 0;
+	for (int i = 0; i < 5; i++) {
+		a += 100/i; //WARN
+	}
+	a = 5;
+	a /= 0; //WARN
+
+	return 0;
+}