C++: Only consider the maximum buffer size for badly bounded write

[jketema]

New attempt at fixing #13913.

The original attempt is here: #13929, which was backed out here: #13996, because of a bug found in monotonic aggregates, which has since been fixed.

Currently running DCA and MRVA on this, will report on the results when they're ready.

[MathiasVP]

The changes LGTM (but I also said that last time 😅). Let's see what DCA brings 🤞

[jketema]

MRVA query:

import cpp
import semmle.code.cpp.security.BufferWrite

module before {
  predicate p(BufferWrite bw, int destSize) {
    bw.hasExplicitLimit() and // has an explicit size limit
    destSize = getBufferSize(bw.getDest(), _) and
    bw.getExplicitLimit() > destSize // but it's larger than the destination
  }
}

module after {
  predicate p(BufferWrite bw, int destSize) {
    bw.hasExplicitLimit() and // has an explicit size limit
    destSize = max(getBufferSize(bw.getDest(), _)) and
    bw.getExplicitLimit() > destSize // but it's larger than the destination
  }
}

from BufferWrite bw, int destSize
where
  before::p(bw, destSize) and
  not after::p(bw, destSize)
select bw, destSize

[jketema]

DCA looks good. MRVA shows 8 results before these changes, and those are all unaffected by this change.