dcoughlin added a comment.

In https://reviews.llvm.org/D20811#544981, @NoQ wrote:

> Hmm, what about
>     ARGUMENT_VALUE(0, WithinRange)
>       RANGE('0', '9')
>       RANGE('A', 'Z')
>       RANGE('a', 'z')
>     RETURN_VALUE(OutOfRange)
>       VALUE(0)
> ?

"CONSTRAIN" is a verb. What is the direct object here? It seems to me that the 
thing being constrained is the return value, so it seems odd to have 
'CONSTRAIN' around the conditions on the arguments.

> Something i don't like here is that the word "value" is overloaded. Maybe 
> rename the inner `VALUE` back to `POINT`?

I don't think the geometric metaphor of 'POINT' makes sense here, especially 
with 'RANGE' (which I think is very good). What is the analog of a range that 
has only a single element?

Comment at: lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:547
@@ +546,3 @@
+            RANGE {
+              RET_VAL, RANGE_KIND(OutOfRange),
+              SET { POINT(0) }
NoQ wrote:
> dcoughlin wrote:
> > Is it ever the case that this final 'RANGE" constrains anything other than 
> > the return value? If not, can 'RET_VAL' be elided?
> Some summaries only have pre-conditions: "for this argument constraint, any 
> return value is possible". We should also be able to support void functions, 
> which have no return values.
What does a postcondition on a void function mean in this context? Can you 
refer to argument values? Such as "If the the function terminates then it must 
have been the case that the first argument was in the rangy x..z even though we 
didn't know that going in? Is this useful?


cfe-commits mailing list

Reply via email to