<div dir="ltr">Anton, thanks for taking the time to review the code and answer.<div>I ran a few more tests and noticed that the analyzer never reaches the if statement.<br><div>Here's a refined example to illustrate this:</div>
<div><br></div><div>void use(int);</div><div>void checkchecker(char *s) {</div><div>    int i=0;</div><div>    int j;</div><div>    int k;</div><div>    while(*(s++)!=0) {</div><div>        i++;</div><div>                k = 0;</div>
<div><span class="" style="white-space:pre">            </span>use(j);</div><div>    }</div><div><span class="" style="white-space:pre">        </span>if(i>0)</div><div>           use(k);</div><div>}</div><div><br></div><div><div>pathtest.c:9:5: warning: Function call argument is an uninitialized value</div>
<div>                                use(j);</div><div>                                ^   ~</div><div><br></div></div><div style>As you can see, the analyzer does indeed walks through the while loop (therefore increments i), but never reaches into the if statement.</div>
<div style>So as I understand , not all paths are covered. Am I missing something here?<br></div></div><div style><br></div><div style>Thanks again,</div><div style>Yuval</div><div style><br></div></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Thu, Apr 18, 2013 at 9:56 PM, Anton Yartsev <span dir="ltr"><<a href="mailto:anton.yartsev@gmail.com" target="_blank">anton.yartsev@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On 18.04.2013 10:51, YuvalShahar wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
yes, sorry for this mistake.<br>
I was trying to build a small program to understand why not all paths are<br>
covered.<br>
How about this example:<br>
<br>
void use(int);<br>
void checkchecker(char *s) {<br>
        int i=0;<br>
        int j;<br>
        while(*(s++)!=0) {<br>
                i++;<br>
        }<br>
        if(i>4) {<br>
                use(j);   //no report - if predicate is changed to i<4 there is a report<br>
        }<br>
}<br>
<br>
I see in the code that loops are covered 4 times,<br>
</blockquote></div>
Hi, Yuval.<br>
<br>
There is an analyzer option -analyzer-max-loop <value> that establishes how many times the analyzer iterates the loop.<br>
In your example if the contents of 's' is unknown the loop will iterate up to this value.<div class="im"><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
but I'd like to add<br>
another path and remove all constraints on variables that are changed in the<br>
loop (in the style of a widening operation). Any ideas on how to do this?<br>
Thanks, Yuval<br>
</blockquote></div>
As I understand the analyzer tries to cover all possible paths. In your example the first paths is when the while condition is considered false at the very beginning and the loop iterates 0 times; the following code illustrates this:<div class="im">
<br>
<br>
void use(int);<br>
void checkchecker(char *s) {<br>
    int i=0;<br>
    int j;<br></div>
    int k;<br>
    while(*(s++)!=0) {<br>
        i++;<br>
                k = 0;<br>
    }<br>
        use(k);<br>
}<br>
<br>
z_zzz.cpp:11:9: warning: Function call argument is an uninitialized value<br>
        use(k);<br>
        ^   ~<br>
<br>
Here no constrains from the loop are applied.<br>
Does it help?<div class="HOEnZb"><div class="h5"><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
<br>
--<br>
View this message in context: <a href="http://clang-developers.42468.n3.nabble.com/uncovered-path-wrong-constraint-tp4031492p4031559.html" target="_blank">http://clang-developers.42468.<u></u>n3.nabble.com/uncovered-path-<u></u>wrong-constraint-<u></u>tp4031492p4031559.html</a><br>

Sent from the Clang Developers mailing list archive at Nabble.com.<br>
______________________________<u></u>_________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@cs.uiuc.edu" target="_blank">cfe-dev@cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev" target="_blank">http://lists.cs.uiuc.edu/<u></u>mailman/listinfo/cfe-dev</a><br>
</blockquote>
<br>
<br></div></div><span class="HOEnZb"><font color="#888888">
-- <br>
Anton<br>
<br>
</font></span></blockquote></div><br></div>