[cfe-dev] [StaticAnalyzer] I think ExplodedGraph is wrong

[Aleksei Sidorin via cfe-dev]

Hm, seems like there is no difference between versions.

There is my understanding of the problem.
We don't handle sym-sym comparisons well. The result of comparison 
between two symbols is an UnknownVal.
First, analyzer renders "b >= Min" branch and assumes it false. Then, it 
renders operator '&&', then makes a cleanup which results in a new node 
with an empty state (1). It proceeds with false branch to operator! and 
then - to ReturnStmt.

Then, it renders branch where (b >= Min) is true. It assigns another 
UnknownVal to b < Max, cleanups ... and tries to create another 
empty-stated node before entering operator!. But there is already a node 
with an empty state and in the ProgramPoint. So, two execution paths are 
merged unexpectedly. And the analysis finishes since 'operator!' was 
rendered already for this merged branch.

I tried a quick solution which is the conjuring a symbolic value for 
comparisons instead of leaving it Unknown. It seems to work but I'm not 
sure if it is exactly what we need here. Anna, Artem, what is your 
opinion? Should we proceed with review or it is a bad idea in general?



09.09.2016 12:05, Aleksei Sidorin via cfe-dev пишет:
> Hello Daniel,
>
> Thank you for report! Yes, I can confirm this bug. However, I cannot 
> see this behaviour with an old version of clang: with clang-3.4.1 
> 'b++' is still reachable. Will investigate.
>
>
>
> 08.09.2016 18:06, Daniel Marjamäki via cfe-dev пишет:
>> Hello!
>>
>> When I analyze this code:
>>
>>      extern int Min,Max;
>>           void dfsd(int b) {
>>          if (!(b >= Min && b < Max))
>>            return;
>>          b++;
>>      }
>>
>> It says that "b++;" is unreachable. When I look at the ExplodedGraph 
>> it seems to me that there is no node below the return. I would like 
>> to debug this. But I don't know where I should look. Do you have some 
>> idea?
>>
>> Best regards,
>> Daniel Marjamäki
>>
>> .................................................................................................................. 
>>
>> Daniel Marjamäki Senior Engineer
>> Evidente ES East AB  Warfvinges väg 34  SE-112 51 Stockholm Sweden
>>
>> Mobile:                 +46 (0)709 12 42 62
>> E-mail:                 Daniel.Marjamaki at evidente.se
>>
>> www.evidente.se
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev at lists.llvm.org
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
>


-- 
Best regards,
Aleksei Sidorin
Software Engineer,
IMSWL-IMCG, SRR, Samsung Electronics