dcoughlin added a comment.
In https://reviews.llvm.org/D20811#544981, @NoQ wrote:
> Hmm, what about
>
> CONSTRAIN
> ARGUMENT_VALUE(0, WithinRange)
> RANGE('0', '9')
> RANGE('A', 'Z')
> RANGE('a', 'z')
> END_ARGUMENT_VALUE
> RETURN_VALUE(OutOfRange)
> VALUE(0)
> END_RETURN_VALUE
> END_CONSTRAIN
>
>
> ?
"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?
https://reviews.llvm.org/D20811
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
