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

[Artem Dergachev via cfe-commits]

NoQ marked 9 inline comments as done.
NoQ added a comment.

I thought to give it a pause to take a fresh look at how to arrange the macro-hints in the summaries.

Maybe something like that:

  CASE
    ARGUMENT_CONDITION(ARG_NO(0), OutOfRange)
      RANGE('0', '9')
      RANGE('A', 'Z')
      RANGE('a', 'z')
      RANGE(128, 255)
    END_ARGUMENT_CONDITION
    RETURN_VALUE_CONDITION(WithinRange)
      SINGLE_VALUE(0)
    END_RETURN_VALUE_CONDITION
  END_CASE



================
Comment at: lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:547
+            RANGE {
+              RET_VAL, RANGE_KIND(OutOfRange),
+              SET { POINT(0) }
----------------
dcoughlin wrote:
> 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?
No, i don't think this is useful. There are just timeless immutable symbols about which we learn something new on every branch.

If the function doesn't terminate on certain pre-conditons, then we can model it by never mentioning these pre-conditions in any of the branches (we don't use this trick anywhere yet - all functions listed here shall terminate in all cases).

This would have been useful if we start referring to the heap shape (eg. "if the value behind the pointer passed as second argument to the call was in range [1,10] before the call, then it would be equal to 42 after the call"), but we don't do that yet.


https://reviews.llvm.org/D20811