[Bug c/77690] New: -Wformat-length %s false positive after strlen check

["nsz at gcc dot gnu.org" <gcc-bugzilla at gcc dot gnu dot org>]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=77690

            Bug ID: 77690
           Summary: -Wformat-length %s false positive after strlen check
           Product: gcc
           Version: 7.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: c
          Assignee: unassigned at gcc dot gnu.org
          Reporter: nsz at gcc dot gnu.org
  Target Milestone: ---

there is no obvious way to silence the sprintf %s warning.
(this currently breaks the gdb build)

$ cat a.c
int sprintf (char*, const char*, ...);

struct { char buf[12]; } s;

void f(void)
{
  char foo[7];
  if (__builtin_strlen(s.buf) > 3) // this check does not help
    return;
  sprintf(foo, "zz%s", s.buf);
}

$ gcc -Wall -c a.c
a.c: In function 'f':
a.c:10:19: warning: '%s' directive writing between 0 and 11 bytes into a region
of size 5 [-Wformat-length=]
   sprintf(foo, "zz%s", s.buf);
                   ^~   ~
a.c:10:3: note: format output between 3 and 14 bytes into a destination of size
7
   sprintf(foo, "zz%s", s.buf);
   ^~~~~~~~~~~~~~~~~~~~~~~~~~~