[clang] [clang][analyzer] Correct SMT Layer for _BitInt cases refutations (PR #143310)

Balazs Benics via cfe-commits cfe-commits at lists.llvm.org
Wed Jun 11 06:20:38 PDT 2025


================
@@ -0,0 +1,22 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -w \
+// RUN:   -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+// Previously these tests were crashing because the SMTConv layer did not
+// comprehend the _BitInt types.
+
+void clang_analyzer_warnIfReached();
+
+void c(int b, _BitInt(35) a) {
+  int d;
+  if (a)
+    b = d; // expected-warning{{Assigned value is uninitialized [core.uninitialized.Assign]}}
----------------
steakhal wrote:

This wasn't addressed.
> [...] If we need this branch, maybe we could at least initialize d to zero or something.

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


More information about the cfe-commits mailing list