<div dir="ltr"><span style="color:rgb(0,0,0);font-family:arial,helvetica,sans-serif">Hi Artem, </span><br><div class="gmail_quote"><div dir="ltr"><div><font color="#000000" face="arial, helvetica, sans-serif"><br></font></div><div><font color="#000000" face="arial, helvetica, sans-serif">Thank you for your help. The definition of the list is available in the current translation unit, but I was able to turn off the warning changing the variable list to be a pointer, and using concrete values for the condition of the iteration instead of </font><span style="color:rgb(0,0,0);font-family:arial,helvetica,sans-serif">"</span><i style="color:rgb(0,0,0);font-family:arial,helvetica,sans-serif">i < <span style="font-size:14px">list.</span><span style="font-size:14px">getSize</span></i><span style="color:rgb(0,0,0);font-family:arial,helvetica,sans-serif;font-size:14px"><i>()</i>"</span><span style="color:rgb(0,0,0);font-family:arial,helvetica,sans-serif;font-size:14px">. As I understand, loops, by default, unroll a fixed amount of times when the condition is symbolic, defining like a symbolic offset. Do we keep any reasoning about this symbolic offset? if the iteration unroll say 4 times, and the condition is </span><i><span style="font-family:arial,helvetica,sans-serif;font-size:14px">"</span><span style="font-family:Menlo;font-size:14px;color:rgb(187,44,162)">int</span><span style="font-family:Menlo;font-size:14px"> i = </span><span style="font-family:Menlo;font-size:14px;color:rgb(39,42,216)">0</span><span style="font-family:Menlo;font-size:14px">; i<list.</span><span style="font-family:Menlo;font-size:14px">getSize()</span></i><span style="font-family:Menlo;font-size:14px"><i>; i++"</i>, </span><span style="font-size:14px"><font face="arial, helvetica, sans-serif" color="#000000">maybe I will expected the variable i to have the concrete values 0, 1, 2 and 3 at a time. Is this thought wrong?</font></span></div><div><span style="font-size:14px"><font color="#000000" face="arial, helvetica, sans-serif"><br></font></span></div><div><span style="font-size:14px"><font color="#000000" face="arial, helvetica, sans-serif">When the list is passed on by value, even when using concrete values for the condition, the analyzer reports the bug. Why could it be happening? Maybe because of the same thing happening in the symbolic iteration of the copy constructor.</font></span></div><div><span style="font-size:14px"><font color="#000000" face="arial, helvetica, sans-serif"><br></font></span></div><div><span style="font-size:14px"><font color="#000000" face="arial, helvetica, sans-serif">The list definition is pretty simple:</font></span></div><div><span style="font-family:Menlo;font-size:14px"><font color="#000000"><br></font></span></div><div><p style="margin:0px;font-size:14px;font-family:Menlo"><span style="color:rgb(187,44,162)">class</span> IntegerList {</p>
<p style="margin:0px;font-size:14px;font-family:Menlo;color:rgb(187,44,162)">private<span style="color:rgb(0,0,0)">:</span></p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(187,44,162)">int</span>* ptr;</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(187,44,162)">int</span> size;</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(187,44,162)">int</span> maxCapacity;</p>
<p style="margin:0px;font-size:14px;font-family:Menlo;color:rgb(187,44,162)">public<span style="color:rgb(0,0,0)">:</span></p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> IntegerList(<span style="color:rgb(187,44,162)">int</span> maxCapacity){</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(79,129,135)">ptr</span> = <span style="color:rgb(187,44,162)">new</span> <span style="color:rgb(187,44,162)">int</span>[maxCapacity];</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(187,44,162)">this</span>-><span style="color:rgb(79,129,135)">maxCapacity</span> = maxCapacity;</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(187,44,162)">this</span>-><span style="color:rgb(79,129,135)">size</span> = <span style="color:rgb(39,42,216)">0</span>;</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> }</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> </p><p style="margin:0px;font-size:14px;font-family:Menlo"> ~IntegerList(){<span style="color:rgb(61,29,129)">free</span>(<span style="color:rgb(79,129,135)">ptr</span>);}</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> </p><p style="margin:0px;font-size:14px;font-family:Menlo"> IntegerList(<span style="color:rgb(187,44,162)">const</span> <span style="color:rgb(79,129,135)">IntegerList</span>& IL){</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(79,129,135)">ptr</span> = <span style="color:rgb(187,44,162)">new</span> <span style="color:rgb(187,44,162)">int</span>[IL.<span style="color:rgb(79,129,135)">size</span>];</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(187,44,162)">for</span> (<span style="color:rgb(187,44,162)">int</span> i = <span style="color:rgb(39,42,216)">0</span> ; i < IL.<span style="color:rgb(79,129,135)">size</span>; i++){</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(79,129,135)">ptr</span>[i] = IL.<span style="color:rgb(49,89,93)">at</span>(i);</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> }</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(79,129,135)">size</span> = IL.<span style="color:rgb(79,129,135)">size</span>;</p>
<p style="margin:0px;font-size:14px;font-family:Menlo;color:rgb(79,129,135)"><span style="color:rgb(0,0,0)"> </span>maxCapacity<span style="color:rgb(0,0,0)"> = IL.</span>maxCapacity<span style="color:rgb(0,0,0)">;</span></p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> }</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> </p><p style="margin:0px;font-size:14px;font-family:Menlo"><span style="color:rgb(187,44,162)"> int</span> getSize() <span style="color:rgb(187,44,162)">const</span> {<span style="color:rgb(187,44,162)">return</span> <span style="color:rgb(79,129,135)">size</span>;}</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> </p><p style="margin:0px;font-size:14px;font-family:Menlo"><span style="color:rgb(187,44,162)"> int</span> at(<span style="color:rgb(187,44,162)">int</span> pos) <span style="color:rgb(187,44,162)">const</span> {<span style="color:rgb(187,44,162)">return</span> (pos>=<span style="color:rgb(39,42,216)">0</span> && pos<<span style="color:rgb(79,129,135)">size</span>)?<span style="color:rgb(79,129,135)">ptr</span>[pos]:-<span style="color:rgb(39,42,216)">1</span>;}</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> </p><p style="margin:0px;font-size:14px;font-family:Menlo"><span style="color:rgb(187,44,162)"> void</span> add(<span style="color:rgb(187,44,162)">int</span> elem){</p>
<p style="margin:0px;font-size:14px;font-family:Menlo;color:rgb(79,129,135)"><span style="color:rgb(0,0,0)"> </span><span style="color:rgb(187,44,162)">if</span><span style="color:rgb(0,0,0)"> (</span>size<span style="color:rgb(0,0,0)"> < </span>maxCapacity<span style="color:rgb(0,0,0)">){</span></p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(79,129,135)">ptr</span>[<span style="color:rgb(79,129,135)">size</span>]=elem;</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> <span style="color:rgb(79,129,135)">size</span>++;</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> }</p>
<p style="margin:0px;font-size:14px;font-family:Menlo"> }</p>
<p style="margin:0px;font-size:14px;font-family:Menlo">};</p></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">2015-12-03 7:09 GMT-03:00 Artem Dergachev via cfe-dev <span dir="ltr"><<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I think this case is of an actual false positive:<br>
<br>
(1) Our constraint solver (RangeConstraintManager) is very simple and doesn't yet handle constraints like "x is odd" properly. Not quite sure, in fact maybe at least adding a "== 0" range on the SymIntExpr "x % 2" should have helped, why don't we do at least that? I'd have had a look.<br>
<br>
(2) If IntegerList::at() is not inlined properly (doesn't have its body available for analysis), then the analyzer would not realize that the symbol checked in hasEvenNumbers() is the same symbol that is checked in walkthrough(); at() may return a different value, and blindly assuming this value to be the same (eg. assuming all unknown functions to be pure) would make things a lot worse. This is a more complicated work of supporting (evalCall'ing or BodyFarm'ing) STL containers, assuming IntegerList is a typedef for some std::list<int>, or if you use custom containers, then you need to have a checker to support them, or inter-unit analysis may be of use if the body of container methods is in fact available, just in another translation unit.<div><div><br>
_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
</div></div></blockquote></div><br></div>
</div></div></div><br></div>