<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>