https://github.com/vabridgers created
https://github.com/llvm/llvm-project/pull/146597
PR145731 corrected the analyzer test runner to consider use of z3 when used by
testcases, which exposed problems in test cases PR37855.c and crashes in
z3-crosscheck.c This change fixes those crashes and re-enables the test cases
that were "XFAIL"'d out.
>From 38815260293ce0ebb729311706b6c984c9f3efc5 Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridg...@ericsson.com>
Date: Tue, 1 Jul 2025 21:48:10 +0200
Subject: [PATCH] [analyzer] Correct Z3 test cases, fix exposed crashes
PR145731 corrected the analyzer test runner to consider use of
z3 when used by testcases, which exposed problems in test cases
PR37855.c and crashes in z3-crosscheck.c This change fixes those
crashes and re-enables the test cases that were "XFAIL"'d out.
---
.../clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h | 3 +++
clang/test/Analysis/PR37855.c | 10 ++++------
clang/test/Analysis/z3-crosscheck.c | 2 --
llvm/lib/Support/Z3Solver.cpp | 3 ++-
4 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 70a7953918ace..a6cb6c0f12a8c 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -598,6 +598,9 @@ class SMTConv {
if (APSIntBitwidth == 1 && Ty.isNull())
return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
getAPSIntType(Ctx, NewInt)};
+ else if (APSIntBitwidth == 1 && !Ty.isNull())
+ return {Int.extend(Ctx.getTypeSize(getAPSIntType(Ctx, Int))),
+ getAPSIntType(Ctx, NewInt)};
if (llvm::isPowerOf2_32(APSIntBitwidth) || Ty.isNull())
return {Int, Ty};
return {Int.extend(Ctx.getTypeSize(Ty)), Ty};
diff --git a/clang/test/Analysis/PR37855.c b/clang/test/Analysis/PR37855.c
index 434df576e8ece..92ed9ffe69a7d 100644
--- a/clang/test/Analysis/PR37855.c
+++ b/clang/test/Analysis/PR37855.c
@@ -2,23 +2,21 @@
// RUN: %clang_analyze_cc1 -analyzer-checker=core -w -analyzer-config
crosscheck-with-z3=true -verify %s
// REQUIRES: z3
-// XFAIL: *
-
typedef struct o p;
struct o {
struct {
} s;
};
-void q(*r, p2) { r < p2; }
+void q(int *r, int p2) { r < p2; }
-void k(l, node) {
+void k(int l, int node) {
struct {
p *node;
} * n, *nodep, path[sizeof(void)];
- path->node = l;
+ path->node = (p*) l;
for (n = path; node != l;) {
- q(node, n->node);
+ q((int *)&node, (int)n->node);
nodep = n;
}
if (nodep) // expected-warning {{Branch condition evaluates to a garbage
value}}
diff --git a/clang/test/Analysis/z3-crosscheck.c
b/clang/test/Analysis/z3-crosscheck.c
index ca20cd6a879f1..8cbe7dd2975d0 100644
--- a/clang/test/Analysis/z3-crosscheck.c
+++ b/clang/test/Analysis/z3-crosscheck.c
@@ -2,8 +2,6 @@
// RUN: %clang_analyze_cc1 -triple x86_64-pc-linux-gnu
-analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config
crosscheck-with-z3=true -verify %s
// REQUIRES: z3
-// XFAIL: *
-
void clang_analyzer_dump(float);
int foo(int x)
diff --git a/llvm/lib/Support/Z3Solver.cpp b/llvm/lib/Support/Z3Solver.cpp
index 27027093a0c6f..056a17ad80123 100644
--- a/llvm/lib/Support/Z3Solver.cpp
+++ b/llvm/lib/Support/Z3Solver.cpp
@@ -932,7 +932,8 @@ class Z3Statistics final : public SMTSolverStatistics {
};
unsigned getUnsigned(StringRef Key) const override {
auto It = UnsignedValues.find(Key.str());
- assert(It != UnsignedValues.end());
+ if (It == UnsignedValues.end())
+ return 0;
return It->second;
};
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
