Skip to content

Commit df5edaa

Browse files
authored
Merge pull request #1892 from goblint/div-by-zero-invariant
Remove division by zero error message during base `invariant`
2 parents fa7b637 + 8688982 commit df5edaa

1 file changed

Lines changed: 3 additions & 6 deletions

File tree

src/analyses/baseInvariant.ml

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -293,12 +293,9 @@ struct
293293
let inv_bin_int (a, b) ikind c op =
294294
let warn_and_top_on_zero x =
295295
if ID.equal_to Z.zero x = `Eq then
296-
(M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
297-
Checks.error Checks.Category.DivisionByZero "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
298-
ID.top_of ikind)
299-
else (
300-
Checks.safe Checks.Category.DivisionByZero;
301-
x)
296+
ID.top_of ikind
297+
else
298+
x
302299
in
303300
let meet_bin a' b' = id_meet_down ~old:a ~c:a', id_meet_down ~old:b ~c:b' in
304301
let meet_com oi = (* commutative *)

0 commit comments

Comments
 (0)