Rice’s theorem applies to any non-trivial semantic property.
Looking at the docs, I’m not really sure CodeQL is semantic in the same sense as Rices theorem. It looks syntactic more than semantic.
Eg breaking Rices theorem would require it to detect that an application isn’t vulnerable if it contains the vulnerability but only in paths that are unreachable. Like
if request.params.limit > 1000:
throw error
# 1000 lines of code
if request.params.limit > 1000:
call_vulnerable_code()
I’m not at a PC right now, but I’d be curious if CodeQL thinks that’s vulnerable or not.It’s probably demonstrably true that there is syntactically a path to the vulnerability, I’m a little dubious that it’s demonstrably true the code path is actually reachable without executing the code.