mirror of
https://github.com/llvm/llvm-project.git
synced 2025-04-17 05:26:47 +00:00
9ca62c5302
Random testing found that the Z3 wrapper does not support UnarySymExpr, which was added recently and not included in the original Z3 wrapper. For now, just avoid submitting expressions to Z3 to avoid compiler crashes. Some crash context ... clang -cc1 -analyze -analyzer-checker=core z3-unarysymexpr.c -analyzer-constraints=z3 Unsupported expression to reason about! UNREACHABLE executed at clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:297! Stack dump: 3. <root>/clang/test/Analysis/z3-unarysymexpr.c:13:7: Error evaluating branch #0 <addr> llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) #1 <addr> llvm::sys::RunSignalHandlers() #8 <addr> clang::ento::SimpleConstraintManager::assumeAux( llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::NonLoc, bool) #9 <addr> clang::ento::SimpleConstraintManager::assume( llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::NonLoc, bool) Co-authored-by: einvbri <vince.a.bridgers@ericsson.com>
16 lines
355 B
C
16 lines
355 B
C
// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \
|
|
// RUN: -analyzer-constraints=z3
|
|
|
|
// REQUIRES: Z3
|
|
//
|
|
// Previously Z3 analysis crashed when it encountered an UnarySymExpr, validate
|
|
// that this no longer happens.
|
|
//
|
|
|
|
// expected-no-diagnostics
|
|
int negate(int x, int y) {
|
|
if ( ~(x && y))
|
|
return 0;
|
|
return 1;
|
|
}
|