[cfe-dev] unsigned variable preserves signed value?

[Artem Dergachev via cfe-dev]

Yup, bug. We re-use the same symbol for 'i', 'j', and 'a'. The correct 
behavior would be to construct a SymbolCast<reg_$0<int i>, unsigned 
short> and then another SymbolCast<SymbolCast<reg_$0<int i>, unsigned 
short>, int>.

But it causes more harm than good due to RangeConstraintManager being 
unable to reason about cast symbols anyway. So, like even if we 
construct those cast symbols, we'll produce more false positives than we 
suppress, unless we also improve the constraint solver dramatically. 
Been there, seen that.

We could do this with Z3 or another full-featured SMT solver, but it 
probably won't come completely for free with cross-check, as we'll end 
up exploring more paths (RangeConstraintManager will fail to discard the 
path immediately more often) and find less bugs (as 
RangeConstraintManager will fail to discard the non-buggy state more 
often). I don't have concrete for this particular take on the problem 
though.

On 11/15/19 3:49 AM, Balázs Kéri via cfe-dev wrote:
> Hi,
>
> In the following code:
>
> void test1(int i) {
>   unsigned short j = i;
>   if (j < 0) {
>     int a = j;
>     clang_analyzer_eval(a < 0); // expected-warning{{FALSE}}
>   }
> }
>
> The condition 'a < 0' is evaluated as true by the analyzer (and 'j < 
> 0' too). Normally the branch can not be entered at all because 'j < 0' 
> can not be true. Is this the correct way of how this should work? It 
> looks like that the variable 'a' points to the same memory region as 
> 'i' that contains a signed value. The problem does not appear if 
> 'unsigned int' is used for 'j'.
>
> Balázs
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev