diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h @@ -454,7 +454,9 @@ llvm::SMTExprRef OperandExp = getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison); llvm::SMTExprRef UnaryExp = - fromUnOp(Solver, USE->getOpcode(), OperandExp); + OperandTy->isRealFloatingType() + ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp) + : fromUnOp(Solver, USE->getOpcode(), OperandExp); // Currently, without the `support-symbolic-integer-casts=true` option, // we do not emit `SymbolCast`s for implicit casts. diff --git a/clang/test/Analysis/z3-crosscheck.c b/clang/test/Analysis/z3-crosscheck.c --- a/clang/test/Analysis/z3-crosscheck.c +++ b/clang/test/Analysis/z3-crosscheck.c @@ -1,7 +1,9 @@ -// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s -// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s +// RUN: %clang_cc1 -triple x86_64-pc-linux-gnu -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s +// RUN: %clang_cc1 -triple x86_64-pc-linux-gnu -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s // REQUIRES: z3 +void clang_analyzer_dump(float); + int foo(int x) { int *z = 0; @@ -55,3 +57,23 @@ h(2); } } + +void floatUnaryNegInEq(int h, int l) { + int j; + clang_analyzer_dump(-(float)h); // expected-warning-re{{-(float) (reg_${{[0-9]+}})}} + clang_analyzer_dump((float)l); // expected-warning-re {{(float) (reg_${{[0-9]+}})}} + if (-(float)h != (float)l) { // should not crash + j += 10; + // expected-warning@-1{{garbage}} + } +} + +void floatUnaryLNotInEq(int h, int l) { + int j; + clang_analyzer_dump(!(float)h); // expected-warning{{Unknown}} + clang_analyzer_dump((float)l); // expected-warning-re {{(float) (reg_${{[0-9]+}})}} + if ((!(float)h) != (float)l) { // should not crash + j += 10; + // expected-warning@-1{{garbage}} + } +}