[cfe-dev] [analyzer] Question about ProgramState::assumeInBound

[Balázs Benics via cfe-dev]

Why cannot prove analyzer that only the true case is feasible for the
following example?
```
ProgramStateRef StInBound  = state->assumeInBound(Idx, Size, true);
ProgramStateRef StOutBound = state->assumeInBound(Idx, Size, false);
```

Given that we know:
SVals:
  Idx.dump():  (conj_$8{int, LC1, S2294, #1}) - 1U
  Size.dump(): extent_$5{SymRegion{reg_$4<char * dst>}}

Range constraints according to the exploded graph nodes:
  extent_$5{SymRegion{reg_$4<char * dst>}}  {[10,18446...]}
  conj_$8{int, LC1, S2294, #1}              {[1,9]}

Does the `Idx < Size` hold for all possible values of `Idx` and `Size`?
IMO yes, since [0-8] < [10,18446...], but the analyzer returns *non-null*
states for both of the `assumeInBound` calls, but why?

Balazs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200325/547d24f6/attachment.html>