Sure, but this one doesn’t pass the sniff test. I’ve written plenty of static analysis tools (including ones that do symbolic execution), and one of the first things you do to ensure that your results are valid is create some model of tainting/reachability. Even an analysis that’s 1-callsite sensitive would have caught this and discarded it as a false positive.

(In case it isn’t clear, I’m saying this is slop that someone whipped up and didn’t even bother to spot check.)