================
@@ -1,15 +1,49 @@
// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify
%s \
// RUN: -analyzer-constraints=z3
+// RUN: %clang_analyze_cc1 -verify %s \
+// RUN: -analyzer-checker=core,debug.ExprInspection \
+// RUN: -analyzer-config crosscheck-with-z3=true
// 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;
}
+
+// Z3 is presented with a SymExpr like this : -((reg_$0<int a>) != 0) :
+// from the Z3 refutation wrapper, that it attempts to convert to a
+// SMTRefExpr, then crashes inside of Z3. The "not zero" portion
+// of that expression is converted to the SMTRefExpr
+// "(not (= reg_$1 #x00000000))", which is a boolean result then the
+// "negative" operator is attempted to be applied which then causes
+// Z3 to crash. The accompanying patch just strips the negative operator
+// before submitting to Z3 to avoid the crash.
----------------
NagyDonat wrote:
```suggestion
// "negative" operator (unary '-', UO_Minus) is attempted to be applied which
// then causes Z3 to crash. The accompanying patch just strips the negative
// operator before submitting to Z3 to avoid the crash.
```
Referencing this operator as the "negative" operator seems to be correct (the
standard also uses this word), but it was a bit strange for me at first, so I
suggest adding this claification.
https://github.com/llvm/llvm-project/pull/158276
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
