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

[Artem Dergachev via cfe-dev]

Basically https://bugs.llvm.org/show_bug.cgi?id=40145.

On 3/25/20 4:20 PM, Balázs Benics via cfe-dev wrote:
> 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
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev