[PATCH] D20811: [analyzer] Model some library functions

[Devin Coughlin via cfe-commits]

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