I wrote:
> I'll try this on 7.3.1, since I already have that on a handy laptop.
> But if it doesn't reproduce there I think the answer is going to be
> that Debian is shipping an old buggy gcov.
Huh. 7.3.1 shows the bug. I'll install F28 and see if it's still
there. Peter, what gcc/gcov version did you test?
regards, tom lane