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

Bal√°zs Benics via cfe-dev cfe-dev at lists.llvm.org
Wed Mar 25 06:20:08 PDT 2020

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:
  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?

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

More information about the cfe-dev mailing list