diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 9388a770ff..9ae487fc52 100644 --- a/src/analyses/base.ml +++ b/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 diff --git a/src/cdomain/value/cdomains/int/intervalDomain.ml b/src/cdomain/value/cdomains/int/intervalDomain.ml index 78dcec85ca..93d2d034b8 100644 --- a/src/cdomain/value/cdomains/int/intervalDomain.ml +++ b/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}) diff --git a/src/cdomain/value/cdomains/int/intervalSetDomain.ml b/src/cdomain/value/cdomains/int/intervalSetDomain.ml index e4f74b0f7a..151d875c84 100644 --- a/src/cdomain/value/cdomains/int/intervalSetDomain.ml +++ b/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 diff --git a/tests/regression/01-cpa/78-divbyzero.c b/tests/regression/01-cpa/78-divbyzero.c new file mode 100644 index 0000000000..961174c437 --- /dev/null +++ b/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; +}