Right now due to a missing brace error the assumptions that an index is inbound in case we are under constrained is not added.

# Details

# Diff Detail

### Event Timeline

Nice catch!

Now, this needs a test. How about this one:

// enable the debug.ExprInspection checker? void clang_analyzer_eval(int); void test_asume_after_access(unsigned long x) { char buf[100]; buf[x] = 1; clang_analyzer_eval(x <= 99); // expected-warning{{TRUE}} }

By the way, if we replace `char` with `int`, this test fails even with your patch. The reason is, the assumption is added on `(4 * x)` rather than on `x`, and the constraint manager explodes. Does anybody volunteer to fix this (eg. on the checker side - throw easier equations at the solver)?

I am not sure that the checker is the appropriate way to fix the remaining issue with this checker. I think generating simpler constraints without loosing any generality is non trivial.

test/Analysis/out-of-bounds.c | ||
---|---|---|

153 | Yay, there already was a test for this. /asume/assume/ here and below? |

Whoops, forgot to answer:

Yeah, there are anyway more problems that require this functionality in the `RangeConstraintManager` (the code throws complicated equations into it anyway, and there are false positives reported), so i think we should try to fix it there anyway, some day.

I added a (proof of concept?) implementation to simplify the constraints in the checker. I wonder what do you think.

On second thought, in `RangeConstraintManager` we need a different functionality. In particular, from `4 * x < 1000` it does not follow that `x < 250` in the general case (due to possible overflows). But in the case of this checker, it doesn't matter - we are always sure that any valid array address is never overflowing even when converted to bytes.

That said, it is still boilerplate. Some day i wish to consider adding the non-overflowing versions of common operations into the `SValBuilder`'s `evalBinOp()`, so that it could help checkers simplify various symbolic expressions. In my opinion, `evalBinOp()` should be as user-friendly as possible.

But that's another story, your approach looks good to me!