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

[Aleksei Sidorin via cfe-dev]

A very initial version of patch for this issue is here: 
https://reviews.llvm.org/D24384


09.09.2016 14:25, 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