llvmbot wrote:
<!--LLVM PR SUMMARY COMMENT--> @llvm/pr-subscribers-clang @llvm/pr-subscribers-llvm-support Author: None (vabridgers) <details> <summary>Changes</summary> 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. --- Full diff: https://github.com/llvm/llvm-project/pull/146597.diff 4 Files Affected: - (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h (+3) - (modified) clang/test/Analysis/PR37855.c (+4-6) - (modified) clang/test/Analysis/z3-crosscheck.c (-2) - (modified) llvm/lib/Support/Z3Solver.cpp (+2-1) ``````````diff 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; }; `````````` </details> https://github.com/llvm/llvm-project/pull/146597 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
