[cfe-dev] [Analyzer] Stores to symbolic region

[Torry Chen via cfe-dev]

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

But if I assign to pxy's fields as in the commented part, the division by
zero bug can be detected.

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.

struct xy {
  int x;
  int y;
}

int intdiv(int x, int y) { return 100 / (x - y); }

void divxy(struct xy *pxy)
{
  struct xy val;

  val.x = 10;
  val.y = val.x;
  *pxy = val;

  // Division by zero can be detected if assign to individual fields.
  // pxy->x = val.x;
  // pxy->y = val.y;

  int res = intdiv(pxy->x, pxy->y);

  printf("Result is %d\n", res);
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20190729/748b3e55/attachment.html>