Clang static analyzer misses division by zero

I'm experimenting with clang static analyzer, and I found the following example where it misses a possible division by zero:

    #include <stdio.h>
    
    int k = 300;
    
    char *parse_mailpath_spec (char *str)
    {
        char *s;
        int pass_next;
    
        for (s = str, pass_next = 0; s && *s; s++)
        {
            if (pass_next == 4)
            {
                int j = 0;
                k = 5 / j;
            }
            if (*s == '\\')
            {
                pass_next++;
                continue;
            }
            if (*s == '?' || *s == '%')
            {
                return s;
            }
        }
        return ((char *)NULL);
    }
    
    int main(int argc, char **argv)
    {
        if (parse_mailpath_spec(argv[1])) return 0;
        else return -1;
    }

If I change if (pass_next == 4) to if (pass_next == 3) then the analyzer finds the bug, and reports the division by zero. I guess I was too naive thinking that the analyzer will not stop unless it can prove the program is safe (?)

The question seems to be, "does Clang static analyzer attempt to prove the program is safe?"

The answer is no.

Why not?

Clang Static Analysis (SA) is a static analyzer, not a verifier. That means it tries to find bugs. It stops when it cannot find any more bugs, not when the program is proven correct.

Why does it miss this bug?

I have not confirmed this, but most likely, Clang SA's internal abstract state converged before it explored the path containing the bug. That means it thought it had explored all of the possible different behaviors of the loop to within the limits of its program state approximations. As a consequence of the undecidability of static program analysis, any static analysis must make approximations, and those approximations can cause it to miss bugs. In this case, evidently Clang SA is willing to explore four iterations of the loop but not five.

Can other tools find it?

Yes. In a comment, Andrey says that PVS-Studio finds it, and I have no reason to doubt that claim. I'm sure it's not the only tool that can.

But beware: this cuts both ways. Some tools simply report more results, often including not just more but a greater proportion of false positives.

The ideal static analysis tool finds enough real bugs to justify the cost of using it (plus the cost of licensing it, if commercial), while reporting few enough false positives that people don't lose confidence and stop using it. It's a difficult balance to strike, and it would usually be a mistake to dismiss a tool on the basis of missing one bug.