ec8d68b59f
Since _BitInt was added later, ASTContext did not comprehend getting a
type by bitwidth that's not a power of 2, and the SMT layer also did not
comprehend this. This led to unexpected crashes using Z3 refutation
during randomized testing. The assertion and redacted and summarized
crash stack is shown here.
clang:
../../clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:103:
static llvm::SMTExprRef
clang::ento::SMTConv::fromBinOp(llvm::SMTSolverRef &,
const llvm::SMTExprRef &, const BinaryOperator::Opcode, const
llvm::SMTExprRef &, bool):
Assertion `*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must
have the same sort!"' failed.
...
<address>
clang::ento::SMTConv::fromBinOp(std::shared_ptr<llvm::SMTSolver>&,
llvm::SMTExpr const* const&, clang::BinaryOperatorKind, llvm::SMTExpr
const* const&,
bool) SMTConstraintManager.cpp
clang::ASTContext&, llvm::SMTExpr const* const&, clang::QualType,
clang::BinaryOperatorKind, llvm::SMTExpr const* const&, clang::QualType,
clang::QualType*) SMTConstraintManager.cpp
clang::ASTContext&, clang::ento::SymExpr const*, llvm::APSInt const&,
llvm::APSInt const&, bool) SMTConstraintManager.cpp
clang::ento::ExplodedNode const*, clang::ento::PathSensitiveBugReport&)
---------
Co-authored-by: Vince Bridgers <vince.a.bridgers@ericsson.com>
23 lines
564 B
C
23 lines
564 B
C
// 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 = 0;
|
|
if (a)
|
|
b = d;
|
|
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
|
|
}
|
|
|
|
void f(int *d, _BitInt(3) e) {
|
|
int g;
|
|
d = &g;
|
|
e ?: 0;
|
|
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
|
|
}
|