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

[via cfe-commits]

llvmbot wrote:


<!--LLVM PR SUMMARY COMMENT-->

@llvm/pr-subscribers-clang

Author: None (NagyDonat)

<details>
<summary>Changes</summary>

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.

---
Full diff: https://github.com/llvm/llvm-project/pull/78442.diff


1 Files Affected:

- (added) clang/test/Analysis/assuming-unsigned-ge-0.c (+19) 


``````````diff
diff --git a/clang/test/Analysis/assuming-unsigned-ge-0.c b/clang/test/Analysis/assuming-unsigned-ge-0.c
new file mode 100644
index 00000000000000..553e68cb96c6bd
--- /dev/null
+++ b/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 at +2 {{Assuming 'arg' is >= 0}}
+  // expected-note at +1 {{Taking false branch}}
+  if (arg < 0)
+    return 0;
+  // expected-note at +2 {{Assuming 'arg' is <= 0}}
+  // expected-note at +1 {{Taking false branch}}
+  if (arg > 0)
+    return 0;
+  // expected-note at +2 {{Division by zero}}
+  // expected-warning at +1 {{Division by zero}}
+  return 100 / arg;
+}

``````````

</details>


https://github.com/llvm/llvm-project/pull/78442