It works for the register language with infinite precision integers.

If you want it to work for C, you'll have to redefine the abstractions of addition and multiplication (and every other operation) appropriately.

You'll also have to parameterize it by word size, endianness, signedness and type of arithmetic.

That is, sound static analysis for C is almost certainly going to be platform-specific.

But, you can still do it.

Indeed. Arguably, compilers do it all the time to be able to (safely) do optimizations. Hence static analyzers are usually an extension to an compiler. Frama-C kind of being the exception, using CIL instead of the intermediate representation of a production compiler.