Re: [PATCH] vasnprintf: silence some clang false positives

2011-02-17 Thread Paul Eggert
>> > Ordinary C "assert (X)" means "crash if X is false". >> > But sa_assert (X) means "assume that X is true". >> > These are two very different different things. > ... for both macros, in the thinking of the programmer, it's an > assertion: the programmer asserts (that is, guarantees) a certain

Re: [PATCH] vasnprintf: silence some clang false positives

2011-02-17 Thread Bruno Haible
Hi Paul, Eric, Jim, Ben, Paul Eggert wrote: > It doesn't feel right that sa_assert uses assert. > They should be more independent. I agree with that. > I think part of the problem here is the naming convention. > Ordinary C "assert (X)" means "crash if X is false". > But sa_assert (X) means "ass

static analysis assumption (was: Re: [PATCH] vasnprintf: silence some clang false positives)

2011-02-15 Thread Bruce Korb
On 02/15/11 12:38, Paul Eggert wrote: >>> invariant (X)? gl_assume(X) seems like a good choice to me. "invariant" doesn't imply that "X" is either true or false and, as Paul said, the expression need not be constructed of invariant components. Yes, the result should be invariant (invariant-true

Re: [PATCH] vasnprintf: silence some clang false positives

2011-02-15 Thread Jim Meyering
Paul Eggert wrote: >>> invariant (X)? > > I'm not a big fan of that name, since the expressions in > question are often not invariants. They might be preconditions > or postconditions, for example. True. So gl_assume (X) ? Hmm... or gl_veritas (X) But that's probably too obscure. Which makes m

Re: [PATCH] vasnprintf: silence some clang false positives

2011-02-15 Thread Paul Eggert
invariant (X)? I'm not a big fan of that name, since the expressions in question are often not invariants. They might be preconditions or postconditions, for example.

Re: [PATCH] vasnprintf: silence some clang false positives

2011-02-15 Thread Jim Meyering
Ben Pfaff wrote: > Paul Eggert writes: > >> If we want to do this sort of thing, I suggest using a different >> name for the static analysis macro, a name that more >> obviously differs from "assert (X)". How about "assume (X)"? > > invariant (X)? I like that. Though we should probably name it

Re: [PATCH] vasnprintf: silence some clang false positives

2011-02-15 Thread Ben Pfaff
Paul Eggert writes: > If we want to do this sort of thing, I suggest using a different > name for the static analysis macro, a name that more > obviously differs from "assert (X)". How about "assume (X)"? invariant (X)? -- Ben Pfaff http://benpfaff.org

Re: [PATCH] vasnprintf: silence some clang false positives

2011-02-15 Thread Paul Eggert
On 02/15/2011 07:40 AM, Eric Blake wrote: > # if STATIC_ANALYSIS > # undef NDEBUG /* Don't let a prior NDEBUG definition cause trouble. */ > # include > # define sa_assert(expr) assert (expr) > # else > # define sa_assert(expr) /* empty */ > # endif It doesn't feel right that sa_assert uses

Re: [PATCH] vasnprintf: silence some clang false positives

2011-02-15 Thread Eric Blake
o add annotations at the three places that clang flagged as potential NULL dereferences, rather than changing ENSURE_ALLOCATION [shown here using abort, but see below]: From 7501dd6520b2fd639286004e63ce1d0f84523798 Mon Sep 17 00:00:00 2001 From: Eric Blake Date: Mon, 14 Feb 2011 15:51:58 -0700 Subject:

Re: [PATCH] vasnprintf: silence some clang false positives

2011-02-14 Thread Bruno Haible
Hi Eric, > Bruno, would you be okay with this patch? > + * lib/vasnprintf.c (VASNPRINTF) [ENSURE_ALLOCATION]: Teach clang > + that ENSURE_ALLOCATION guarantees a non-null result. > +else if (!result) > \ > + abort () No, t

[PATCH] vasnprintf: silence some clang false positives

2011-02-14 Thread Eric Blake
Clang does not realize that result can only ever be NULL when allocated==0, or that (needed) is always positive so that the true branch will always be taken when result starts life as NULL. Adding a false branch fixes the analysis, even though the false branch will never be taken. * lib/vasnprint