[PATCH] D81061: [Analyzer][VLASizeChecker] Fix problem with zero index assumption.

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Checkers/VLASizeChecker.cpp:127-129
+        // Despite the previous assumptions for non-zero and positiveness,
+        // this value might be zero or negative.
+        // At least check for zero again.
----------------
If we aim for a better fix, can we reduce the number of assumptions we make from 2 to 1? Like, it's ok if it's imperfect; 1 imperfect assumption is better than 2 imperfect assumptions.

The mental model i'm following here is that every path-sensitive bug can be thought of as a single formula over symbolic expressions. Eg., division by zero is the formula `"$denominator == 0" is definitely true`, double close is `"is_closed($file_being_closed)"`, division by tainted value is `"$denominator == 0" is possibly true AND "is_tainted($denominator)"`. I'd like you to write down the single formula that represents your bug and perform a single assume() over that and use the result of such assume as an ultimate source of truth. If such assume is not working correctly, let's think how to fix the assume rather than pile up more assumes in every checker to manually cross-check each other.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D81061/new/

https://reviews.llvm.org/D81061