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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
