mon: Division by zero in PGMapDigest::dump_pool_stats_full()

Fixes The Coverity Scan Report:
CID 1412577 (#1 of 1): Division or modulo by float zero (DIVIDE_BY_ZERO)
35. divide_by_zero: In expression (float)mk / k, division by expression k which may be zero has undefined behavior.

Signed-off-by: Jos Collin <jcollin@redhat.com>

diff --git a/src/mon/PGMap.cc b/src/mon/PGMap.cc
index 91e06fb99e6c5ec355f2a3c666283ad6b3193d32..1ab34f253cb46ed8750aa08815866f25b0ac86a8 100644 (file)
--- a/src/mon/PGMap.cc
+++ b/src/mon/PGMap.cc
@@ -683,6 +683,7 @@ void PGMapDigest::dump_pool_stats_full(
        int mk = m + k;
        assert(mk != 0);
        avail = avail * k / mk;
+       assert(k != 0);
        raw_used_rate = (float)mk / k;
       } else {
        raw_used_rate = 0.0;