On Fri, Oct 27, 2017 at 9:33 PM, Jim Meyering <j...@meyering.net> wrote: > On Mon, Oct 2, 2017 at 6:31 PM, Paul Eggert <egg...@cs.ucla.edu> wrote: >> On 10/02/2017 06:24 PM, Jim Meyering wrote: >>> >>> Given all of the comments on that function, I'd be tempted to suppress >>> this warning in that function. >> >> That would work. Another possibility would be to include verify.h and add >> something like this to the start of timespec_cmp: >> >> assume (-1 <= a.tv_nsec && a.tv_nsec <= 2 * TIMESPEC_RESOLUTION); >> >> assume (-1 <= b.tv_nsec && b.tv_nsec <= 2 * TIMESPEC_RESOLUTION); >> >> We might be able to make these 'assume' calls fancier, to exactly match the >> comments, but I'm not sure it's worth the bother. > > Thanks. I prefer that. Here's a proposed patch:
Pushed.
