Skip to content

Commit 3881526

Browse files
author
einvbri
committed
[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.
1 parent 6b3d2b6 commit 3881526

File tree

4 files changed

+9
-9
lines changed

4 files changed

+9
-9
lines changed

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -598,6 +598,9 @@ class SMTConv {
598598
if (APSIntBitwidth == 1 && Ty.isNull())
599599
return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
600600
getAPSIntType(Ctx, NewInt)};
601+
else if (APSIntBitwidth == 1 && !Ty.isNull())
602+
return {Int.extend(Ctx.getTypeSize(getAPSIntType(Ctx, Int))),
603+
getAPSIntType(Ctx, NewInt)};
601604
if (llvm::isPowerOf2_32(APSIntBitwidth) || Ty.isNull())
602605
return {Int, Ty};
603606
return {Int.extend(Ctx.getTypeSize(Ty)), Ty};

clang/test/Analysis/PR37855.c

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,23 +2,21 @@
22
// RUN: %clang_analyze_cc1 -analyzer-checker=core -w -analyzer-config crosscheck-with-z3=true -verify %s
33
// REQUIRES: z3
44

5-
// XFAIL: *
6-
75
typedef struct o p;
86
struct o {
97
struct {
108
} s;
119
};
1210

13-
void q(*r, p2) { r < p2; }
11+
void q(int *r, int p2) { r < p2; }
1412

15-
void k(l, node) {
13+
void k(int l, int node) {
1614
struct {
1715
p *node;
1816
} * n, *nodep, path[sizeof(void)];
19-
path->node = l;
17+
path->node = (p*) l;
2018
for (n = path; node != l;) {
21-
q(node, n->node);
19+
q((int *)&node, (int)n->node);
2220
nodep = n;
2321
}
2422
if (nodep) // expected-warning {{Branch condition evaluates to a garbage value}}

clang/test/Analysis/z3-crosscheck.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,6 @@
22
// 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
33
// REQUIRES: z3
44

5-
// XFAIL: *
6-
75
void clang_analyzer_dump(float);
86

97
int foo(int x)

llvm/lib/Support/Z3Solver.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -932,7 +932,8 @@ class Z3Statistics final : public SMTSolverStatistics {
932932
};
933933
unsigned getUnsigned(StringRef Key) const override {
934934
auto It = UnsignedValues.find(Key.str());
935-
assert(It != UnsignedValues.end());
935+
if (It == UnsignedValues.end())
936+
return 0;
936937
return It->second;
937938
};
938939

0 commit comments

Comments
 (0)