> We’re not talking about decidability of some semantic property in the general case; we’re talking about a specific claim about specific code
Is CodeQL special cased for your code? I very much doubt that. Then it must work in the general case. At that point decidability is impossible and at best either false positives or false negatives can be guaranteed to be absent, but not both (possibly neither of them!)
I don't doubt CodeQL claims can be demonstrably true, that's still coherent with Rice's theorem. However it does mean you'll have false negatives, that is cases where CodeQL reports no provable claim while your code is vulnerable to some issues.
Is CodeQL special cased for your code? I very much doubt that. Then it must work in the general case. At that point decidability is impossible and at best either false positives or false negatives can be guaranteed to be absent, but not both (possibly neither of them!)
I don't doubt CodeQL claims can be demonstrably true, that's still coherent with Rice's theorem. However it does mean you'll have false negatives, that is cases where CodeQL reports no provable claim while your code is vulnerable to some issues.