<div dir="ltr"><font face="arial, helvetica, sans-serif" color="#000000">Hi Jonathan, </font><div><font face="arial, helvetica, sans-serif" color="#000000"><br></font></div><div><font face="arial, helvetica, sans-serif" color="#000000">Thanks for helping me out with this. My question pointed to whether the analyzer can learn (or not) that the only way the program executes the free statement in the method 'walkthrough' is when the list passed on as a parameter has at least one even number. But in the caller, we are making sure that if the list indeed has even numbers, the if condition (in loopExample method) should have taken us to the false branch</font><span style="color:rgb(0,0,0);font-family:arial,helvetica,sans-serif">.</span><div><div><font face="arial, helvetica, sans-serif"><font color="#000000">If <i>hasEvenNumbers</i> returns false, it means there is no even number on the list, does the analyzer not store that constraints on the symbols associated to the element of the list? If this information is available in </font><font color="#000000"><i>walkthrough</i> we could invalidate those paths that make the "<i>number % 2 == 0</i>" condition true, which takes us to the free statement.</font></font></div></div></div><div><font face="arial, helvetica, sans-serif" color="#000000"><br></font></div><div><font face="arial, helvetica, sans-serif" color="#000000">Am I doing anything wrong here? Makes sense?</font></div></div><div class="gmail_extra"><br><div class="gmail_quote">2015-11-30 21:42 GMT-06:00 Jonathan Roelofs <span dir="ltr"><<a href="mailto:jonathan@codesourcery.com" target="_blank">jonathan@codesourcery.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><br>
<br>
On 11/30/15 6:18 PM, Francisco Chiotta via cfe-dev wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi guys,<br>
<br>
<br>
Does this chunk of code represent a false positive? it warns a double<br>
free. I'm being too ambitious?<br>
<br>
<br>
// Does a walk through the list looking for even numbers. If any,<br>
<br>
// it frees obj parameter.<br>
<br>
static void walkthrough(IntegerList list, char* obj) {<br>
<br>
for (int i = 0; i<list.getSize(); i++) {<br>
<br>
int number = <a href="http://list.at" rel="noreferrer" target="_blank">list.at</a>(i);<br>
<br>
if (number % 2 == 0){<br>
<br>
free(obj);  <- Attempt to release free memory<br>
</blockquote>
<br></span>
If execution ever reaches here ^,<span class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
     }<br>
<br>
   }<br>
<br>
}<br>
<br>
// Tell if the list has at least one even number.<br>
<br>
bool hasEvenNumbers(IntegerList list) {<br>
<br>
for (int i = 0; i<list.getSize(); i++) {<br>
<br>
int number = <a href="http://list.at" rel="noreferrer" target="_blank">list.at</a>(i);<br>
<br>
if (number % 2 == 0){<br>
<br>
returntrue;<br>
<br>
     }<br>
<br>
   }<br>
<br>
returnfalse;<br>
<br>
}<br>
<br>
void loopExample(IntegerList list){<br>
<br>
char* obj = (char*)malloc(sizeof(char));<br>
<br>
free(obj); <- First free statement.<br>
</blockquote>
<br></span>
it must have passed through here ^... Meaning, if the second statement is ever executed, it is always a double free.<br>
<br>
<br>
Jon<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
if(!hasEvenNumbers(list)){<span class=""><br>
<br>
walkthrough(list, obj);<br>
<br>
   }<br>
<br>
else {<br>
<br>
std::cout<< "The list has at least one even number!"<< std::endl;<br>
<br>
   }<br>
<br>
}<br>
<br>
<br>
Thanks!<br>
<br>
<br>
<br>
<br></span>
_______________________________________________<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>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
-- <br>
Jon Roelofs<br>
<a href="mailto:jonathan@codesourcery.com" target="_blank">jonathan@codesourcery.com</a><br>
CodeSourcery / Mentor Embedded<br>
</font></span></blockquote></div><br></div>