False positive and false negative from -Wformat-truncation

[Mason <slash dot tmp at free dot fr>]

Hello,

I do note that the documentation for -Wformat-truncation states:
"While enabling optimization will in most cases improve the accuracy of the warning, it may also result in false positives."


However, consider the following test cases:

$ cat testcase.c
#include <stdio.h>
typedef unsigned long long u64;
void foo(u64 arg, char *buf)
{
	u64 u = arg / 1000000000;
	if (u >= 1000) return;
	snprintf(buf, 16, "%llu.XXXZZZ", u);
}

$ gcc-7 -O3 -Wall -S testcase.c 
testcase.c: In function 'foo':
testcase.c:7:20: warning: '.XXXZZZ' directive output may be truncated writing 7 bytes into a region of size between 5 and 15 [-Wformat-truncation=]
  snprintf(buf, 16, "%llu.XXXZZZ", u);
                    ^~~~~~~~~~~~~
In file included from /usr/include/stdio.h:937:0,
                 from testcase.c:1:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:64:10: note: '__builtin___snprintf_chk' output between 9 and 19 bytes into a destination of size 16
   return __builtin___snprintf_chk (__s, __n, __USE_FORTIFY_LEVEL - 1,
          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
        __bos (__s), __fmt, __va_arg_pack ());
        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


Because we only call snprintf when u < 1000, it is obvious to a human
reader that the output cannot overflow the buffer.


Strangely, the following test case does not warn.

$ cat testcase2.c 
#include <stdio.h>
typedef unsigned long long u64;
void foo(u64 arg, char *buf)
{
	snprintf(buf, 16, "%llu.XXXZZZ", arg);
}

Here, a warning would be quite useful... But none is given.


And this tweak of testcase.c makes the warning go away:

$ cat testcase3.c 
#include <stdio.h>
typedef unsigned long long u64;
void foo(u64 arg, char *buf)
{
	if (arg >= 1000000000000ULL) return;
	u64 u = arg / 1000000000;
	snprintf(buf, 16, "%llu.XXXZZZ", u);
}


Maybe the bounds-tracking code has a few blind spots?
NB: Computing 'u' *before* testing arg retriggers the warning.


Regards.