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

via cfe-commits cfe-commits at lists.llvm.org
Wed Jun 11 06:06:18 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]}}
----------------
vabridgers wrote:

The branch is needed (on a _BitInt), and an uninitialized d is also needed to generate a refutation request to Z3.

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


More information about the cfe-commits mailing list