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 "assume that X is true". > These are two very different different things. > I have some qualms about colliding with a C naming convention > that has been used for over three decades, even if the C > name is "wrong" from a static analysis point of view. > > 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)"? I disagree here. "assert (X)" is written from the perspective of the programmer, and "assume (X)" represents the perspective of the static analysis tool. IMO, all such macros need to represent the thinking of the programmer, otherwise it will be too confusing. And for both macros, in the thinking of the programmer, it's an assertion: the programmer asserts (that is, guarantees) a certain condition. The difference is only to whom he does the assertion: to the runtime execution in one case, to the static analysis tool in the other case. Therefore I find that Eric's original naming 'sa_assert' is just perfect. Paul writes: > the expressions in question are often not invariants. They might > be preconditions or postconditions, for example. Yes, or it might be used on arguments upon entry to a function. Eric asked: > Should we create a gnulib module that defines sa_assert() automatically? Yes, this would be useful. > so the real fix is to 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]: It gets tedious to check every invocation of ENSURE_ALLOCATION. I'll prefer to add a single sa_assert invocation at the end of the ENSURE_ALLOCATION macro. Bruno -- In memoriam Giordano Bruno <http://en.wikipedia.org/wiki/Giordano_Bruno>
