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



_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to