Incorrect constant bounds on function parameter

[john-h-kastner]

The bounds for the parameter of b should no wider than the parameter of c, but both parameters are given constant bounds based only of the respective arguments in d.

void a(_Array_ptr<char> y);
void b(char *p) { a(p); }
void c(char *x) { b(x); }

void d(void) {
  b("test");
  c("");
}

void a(_Array_ptr<char> y);
void b(_Array_ptr<char> p : count(4)) { a(p); }
void c(_Array_ptr<char> x : count(0)) { b(x); }

void d(void) {
  b("test");
  c("");
}

[kyleheadley]

What commit and flags are you using? I'm at current main (128c8b8...) using -output-postfix=checked -alltypes -debug-solver -warn-root-cause and no counts are generated. I can get:

void a(_Array_ptr<char> y);
void b(char *p) { a(p); }
void c(char *x) { b(x); }

void d(void) {
  char t[] = "test";
  char n[] = "";
  b(t);
  c(n);
}

converting to

void a(_Array_ptr<char> y);
void b(_Array_ptr<char> p : count(5)) { a(p); }
void c(_Array_ptr<char> x : count(1)) { b(x); }

void d(void) {
  char t _Checked[5] = "test";
  char n _Checked[1] = "";
  b(t);
  c(n);
}

which I think still has the bug with count that you are describing.

[john-h-kastner]

Yes, that's same bug. It looks like I had PR #395 checked out when I found this bug.