Bug: if (C){...} else if (C) {} pattern is found. The second one cannot be reached.

[ustchcs-bugfinder]

z3/src/smt/theory_str_regex.cpp

Line 842 in 7fc4653

} else if (u.re.is_complement(re)) {

        } else if (u.re.is_range(re)) {
            return true;
        } else if (u.re.is_full_char(re)) {
            return true;
        } else if (u.re.is_full_seq(re)) {
            return true;
        } else if (u.re.is_complement(re)) { // line 842
            // TODO can we do better?
            return false;
        } else if (u.re.is_intersection(re)) {
            return false;
        } else if (u.re.is_complement(re)) {    // Same as the condition on line 842
            return false;
        } 

Reported by: USTCHCS Analysis Toolsuite Bugfinder
(bugfinder-2.3: The use of if (C) {…} else if (C) {…} pattern should not be used.)

[mtrberzi]

Opened #4629

@ustchcs-bugfinder may we have some more information about your tool please and how to contact the authors?

[ustchcs-bugfinder]

Opened #4629

@ustchcs-bugfinder may we have some more information about your tool please and how to contact the authors?

Hi, mtrberzi. We are a startup company with a team from Software Safety Lab. of University of Science and Technology of China. So our tool is quite "new". But we are glad you are interested in the result our tool reported.

Last week, we also did an analysis on LLVM/Clang code. Here is a bug list we reported.