78 lines · cpp
1// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \2// RUN: -analyzer-config crosscheck-with-z3=true -verify %s3//4// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \5// RUN: -verify %s6//7// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \8// RUN: -analyzer-config support-symbolic-integer-casts=true -verify=symbolic %s9//10// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \11// RUN: -analyzer-config support-symbolic-integer-casts=false -verify %s12//13// REQUIRES: asserts, z314//15// Requires z3 only for refutation. Works with both constraint managers.16 17void clang_analyzer_dump(int);18 19using sugar_t = unsigned char;20 21// Enum types22enum class ScopedSugared : sugar_t {};23enum class ScopedPrimitive : unsigned char {};24enum UnscopedSugared : sugar_t {};25enum UnscopedPrimitive : unsigned char {};26 27template <typename T>28T conjure();29 30void test_enum_types() {31 // Let's construct a 'binop(sym, int)', where the binop will trigger an32 // integral promotion to int. Note that we need to first explicit cast33 // the scoped-enum to an integral, to make it compile. We could have choosen34 // any other binary operator.35 int sym1 = static_cast<unsigned char>(conjure<ScopedSugared>()) & 0x0F;36 int sym2 = static_cast<unsigned char>(conjure<ScopedPrimitive>()) & 0x0F;37 int sym3 = static_cast<unsigned char>(conjure<UnscopedSugared>()) & 0x0F;38 int sym4 = static_cast<unsigned char>(conjure<UnscopedPrimitive>()) & 0x0F;39 40 // We need to introduce a constraint referring to the binop, to get it41 // serialized during the z3-refutation.42 if (sym1 && sym2 && sym3 && sym4) {43 // no-crash on these dumps44 //45 // The 'clang_analyzer_dump' will construct a bugreport, which in turn will46 // trigger a z3-refutation. Refutation will walk the bugpath, collect and47 // serialize the path-constraints into z3 expressions. The binop will48 // operate over 'int' type, but the symbolic operand might have a different49 // type - surprisingly.50 // Historically, the static analyzer did not emit symbolic casts in a lot51 // of cases, not even when the c++ standard mandated it, like for casting52 // a scoped enum to its underlying type. Hence, during the z3 constraint53 // serialization, it made up these 'missing' integral casts - for the54 // implicit cases at least.55 // However, it would still not emit the cast for missing explicit casts,56 // hence 8-bit wide symbol would be bitwise 'and'-ed with a 32-bit wide57 // int, violating an assertion stating that the operands should have the58 // same bitwidths.59 60 clang_analyzer_dump(sym1);61 // expected-warning-re@-1 {{((unsigned char) (conj_${{[0-9]+}}{enum ScopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}62 // symbolic-warning-re@-2 {{((int) (conj_${{[0-9]+}}{enum ScopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}63 64 clang_analyzer_dump(sym2);65 // expected-warning-re@-1 {{((unsigned char) (conj_${{[0-9]+}}{enum ScopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}66 // symbolic-warning-re@-2 {{((int) (conj_${{[0-9]+}}{enum ScopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}67 68 clang_analyzer_dump(sym3);69 // expected-warning-re@-1 {{(conj_${{[0-9]+}}{enum UnscopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}}) & 15}}70 // symbolic-warning-re@-2 {{((int) (conj_${{[0-9]+}}{enum UnscopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}71 72 clang_analyzer_dump(sym4);73 // expected-warning-re@-1 {{(conj_${{[0-9]+}}{enum UnscopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}}) & 15}}74 // symbolic-warning-re@-2 {{((int) (conj_${{[0-9]+}}{enum UnscopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}75 }76}77 78