<div dir="ltr">Thank you Artem! Another observation: If I re-assign "pxy" as follows, it detects division by zero.<br><br><font face="courier new, monospace">pxy = malloc(sizeof(struct xy)); // <- dected if add this line<br>val.x = 10;<br>val.y = val.x;<br>*pxy = val;</font><div><font face="courier new, monospace"><br></font><div><span style="font-family:"courier new",monospace">int res = intdiv(pxy->x, pxy->y);</span> <font face="courier new, monospace"><br></font></div></div><div><span style="font-family:"courier new",monospace">printf("Result is %d\n", res);</span> <br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 29 Jul 2019 at 17:34, Artem Dergachev <<a href="mailto:noqnoqneo@gmail.com">noqnoqneo@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
  
    
  
  <div 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="gmail-m_-1962262696740764075moz-cite-prefix">On 7/29/19 2:29 PM, Torry Chen via
      cfe-dev wrote:<br>
    </div>
    <blockquote type="cite">
      
      <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="gmail-m_-1962262696740764075mimeAttachmentHeader"></fieldset>
      <pre class="gmail-m_-1962262696740764075moz-quote-pre">_______________________________________________
cfe-dev mailing list
<a class="gmail-m_-1962262696740764075moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>
<a class="gmail-m_-1962262696740764075moz-txt-link-freetext" href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
    </blockquote>
    <br>
  </div>

</blockquote></div>