58 lines · c
1// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \2// RUN: -analyzer-constraints=z3 3// RUN: %clang_analyze_cc1 -verify %s \4// RUN: -analyzer-checker=core,debug.ExprInspection \5// RUN: -analyzer-config crosscheck-with-z3=true6 7// REQUIRES: Z38//9// Previously Z3 analysis crashed when it encountered an UnarySymExpr, validate10// that this no longer happens.11//12 13int negate(int x, int y) {14 if ( ~(x && y))15 return 0;16 return 1;17}18 19// Z3 is presented with a SymExpr like this : -((reg_$0<int a>) != 0) :20// from the Z3 refutation wrapper, that it attempts to convert to a21// SMTRefExpr, then crashes inside of Z3. The "not zero" portion22// of that expression is converted to the SMTRefExpr23// "(not (= reg_$1 #x00000000))", which is a boolean result then the24// "negative" operator (unary '-', UO_Minus) is attempted to be applied which25// then causes Z3 to crash. The accompanying patch just strips the negative26// operator before submitting to Z3 to avoid the crash.27//28// TODO: Find the root cause of this and fix it in symbol manager29//30void c();31 32int z3crash(int a, int b) {33 b = a || b;34 return (-b == a) / a; // expected-warning{{Division by zero [core.DivideZero]}}35}36 37// Floats are handled specifically, and differently in the Z3 refutation layer38// Just cover that code path39int z3_nocrash(float a, float b) {40 b = a || b;41 return (-b == a) / a;42}43 44int z3_crash2(int a) {45 int *d;46 if (-(&c && a))47 return *d; // expected-warning{{Dereference of undefined pointer value}}48 return 0;49}50 51// Refer to issue 16577952void z3_crash3(long a) {53 if (~-(5 && a)) {54 long *c;55 *c; // expected-warning{{Dereference of undefined pointer value (loaded from variable 'c')}}56 }57}58