[analyzer] Demonstrate superfluous unsigned >= 0 assumption (#78442)

This commit adds a testcase which highlights the current incorrect
behavior of the CSA diagnostic generation: it produces a note which says
"Assuming 'arg' is >= 0" in a situation where this is not a fresh
assumption because 'arg' is an unsigned integer.

I also created ticket 78440 to track this bug.

Author: NagyDonat

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

@@ -2883,6 +2883,16 @@ ConditionBRVisitor::VisitTrueTest(const Expr *Cond, BugReporterContext &BRC,
   // previous program state we assuming the newly seen constraint information.
   // If we cannot evaluate the condition (and the constraints are the same)
   // the analyzer has no information about the value and just assuming it.
+  // FIXME: This logic is not entirely correct, because e.g. in code like
+  //   void f(unsigned arg) {
+  //     if (arg >= 0) {
+  //       // ...
+  //     }
+  //   }
+  // it will say that the "arg >= 0" check is _assuming_ something new because
+  // the constraint that "$arg >= 0" is 1 was added to the list of known
+  // constraints. However, the unsigned value is always >= 0 so semantically
+  // this is not a "real" assumption.
   bool IsAssuming =
       !BRC.getStateManager().haveEqualConstraints(CurrentState, PrevState) ||
       CurrentState->getSVal(Cond, LCtx).isUnknownOrUndef();

clang/test/Analysis/assuming-unsigned-ge-0.c

@@ -0,0 +1,19 @@
+// RUN: %clang_analyze_cc1 -analyzer-output=text        \
+// RUN:     -analyzer-checker=core -verify %s
+
+int assuming_unsigned_ge_0(unsigned arg) {
+  // TODO This testcase demonstrates the current incorrect behavior of Clang
+  // Static Analyzer: here 'arg' is unsigned, so "arg >= 0" is not a fresh
+  // assumption, but it still appears in the diagnostics as if it's fresh:
+  // expected-note@+2 {{Assuming 'arg' is >= 0}}
+  // expected-note@+1 {{Taking false branch}}
+  if (arg < 0)
+    return 0;
+  // expected-note@+2 {{Assuming 'arg' is <= 0}}
+  // expected-note@+1 {{Taking false branch}}
+  if (arg > 0)
+    return 0;
+  // expected-note@+2 {{Division by zero}}
+  // expected-warning@+1 {{Division by zero}}
+  return 100 / arg;
+}