<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
Ugh, this looks like a bug. The values are there:<br>
<br>
(SymRegion{reg_$0<struct xy * pxy>},
0, direct):
lazyCompoundVal{0x7fb05e8ac060,val}<br>
<br>
Where Store 0x7fb05e8ac060 has the contents that we're looking for:<br>
<br>
(val, 0, direct): 10 S32b<br>
(val, 32, direct): 10 S32b<br>
<br>
But we don't *load* them correctly.<br>
<br>
I suspect that this is happening because the lazyCompoundVal binding
is direct even though normally it should be a default binding. I'll
take a look. This sounds pretty bad, but also it's not as bad as it
sounds because it's a combination of specific kinds of values when
classified by their origin rather than by their structure. Normally
assigning structures into each other works correctly.<br>
<br>
<div class="moz-cite-prefix">On 7/29/19 2:29 PM, Torry Chen via
cfe-dev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CADmWND9wZbg21f5tx2FenqaDHZztDDL+smnXjddCwEzZyB5+=w@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">I noticed the static analyzer cannot detect a
division by zero problem as shown in the "divxy" function, if it
is analyzed without a caller context. The value assigned to
variable "res" looks like "100 / ((reg_$2<int x>) -
(reg_$1<int SymRegion{reg_$0<struct xy *
pxy>}->y>))"<br>
<br>
But if I assign to pxy's fields as in the commented part, the
division by zero bug can be detected.<br>
<br>
What is the reason behind this and how can I make the analyzer
detect the division by zero bug in this case? I suspect this is
related to handling stores to symbolic region but I haven't
figured out.<br>
<br>
<font face="courier new, monospace">struct xy {<br>
int x;<br>
int y;<br>
}<br>
<br>
int intdiv(int x, int y) { return 100 / (x - y); }<br>
<br>
void divxy(struct xy *pxy)<br>
{<br>
struct xy val;<br>
<br>
val.x = 10;<br>
val.y = val.x;<br>
*pxy = val;<br>
<br>
// Division by zero can be detected if assign to individual
fields.<br>
// pxy->x = val.x;<br>
// pxy->y = val.y;<br>
<br>
int res = intdiv(pxy->x, pxy->y);<br>
<br>
printf("Result is %d\n", res);<br>
}</font><br>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
cfe-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>