=?utf-8?q?Donát?= Nagy <donat.n...@ericsson.com>,
=?utf-8?q?Donát?= Nagy <donat.n...@ericsson.com>,
=?utf-8?q?Donát?= Nagy <donat.n...@ericsson.com>,
=?utf-8?q?Donát?= Nagy <donat.n...@ericsson.com>
Message-ID:
In-Reply-To: <llvm.org/llvm/llvm-project/pull/72...@github.com>


================
@@ -350,17 +383,38 @@ void ArrayBoundCheckerV2::checkLocation(SVal Location, 
bool IsLoad,
     if (ExceedsUpperBound) {
       if (!WithinUpperBound) {
         // We know that the index definitely exceeds the upper bound.
-        std::string RegName = getRegionName(Reg);
-        std::string Msg = getExceedsMsg(C.getASTContext(), RegName, ByteOffset,
-                                        *KnownSize, Location);
-        reportOOB(C, ExceedsUpperBound, OOB_Exceeds, ByteOffset, RegName, Msg);
+        if (isa<ArraySubscriptExpr>(E) && isInAddressOf(E, C.getASTContext())) 
{
+          // ...but this is within an addressof expression, so we need to check
+          // for the exceptional case that `&array[size]` is valid.
+          auto [EqualsToThreshold, NotEqualToThreshold] =
+              compareValueToThreshold(ExceedsUpperBound, ByteOffset, 
*KnownSize,
+                                      SVB, /*CheckEquality=*/true);
+          if (EqualsToThreshold && !NotEqualToThreshold) {
+            // We are definitely in the exceptional case, so return early
+            // instead of reporting a bug.
+            C.addTransition(EqualsToThreshold);
----------------
DonatNagyE wrote:

You're right that `EqualsToThreshold` does not contain new information compared 
to `State`, but I'm using it because I'm trying to follow the pattern that I'm 
always using the _most recent_ state variable.

On the other hand, the variable `State` may contain new information compared to 
the state of the node before the start of this callback: e.g. if we start with 
a range set like $[-\infty, -1] \cup \\{ 10\\}$ for the index variable, then we 
first test for underflow and update the variable `State` when we assume that 
there is no underflow.

I think it's valuable to record these assumptions with a state transition, 
because they improve the accuracy of the modeling. (Otherwise the analyzer 
could produce bug reports that rely on assumptions that contradict each other.) 
Currently the assumptions of this checker are added silently but I'll add note 
tags like "Assuming index is non-negative" for them in a followup commit.

https://github.com/llvm/llvm-project/pull/72107
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to