[PATCH] D39049: [analyzer] Fix wrong calculation of offset in ArrayBoundsV2

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

I checked what happens:

The checker would like to solve the following (I inspect the branch when x == 0 ):
`((reg_$1<unsigned long long y>) + 1) * 4   <= 0`
The `getSimplifiedOffsets` function kicks in and simplifies the expression above to the following:
`(reg_$1<unsigned long long y>)   <= -1`

The analyzer also know that the value of `y` is within `[1,98]`.

The source of the problem is that the simplified expression is evaluated after the right-hand side is converted to an unsigned value which will be greater than the max value of `y`.

I think we did not regress after omitting some of the computation because the analyzer's default constraint manager handles the case when there is a constant addition/subtraction next to the symbol. So if we lose something with this modification, we could probably observe that using multidimensional arrays.

Do you mind writing some tests with multidimensional arrays to check what do we lose if we remove that code?
Also, how hard would it be to correct the calculation for unsigned values?


Repository:
  rL LLVM

https://reviews.llvm.org/D39049