It does so by first defining what a pointer dereference is (on the IR `Instruction` level), and then using the array length analysis and the range analysis together to prove that some of these pointer dereferences are safe.
