Xr0 verifier, guarantee the safety of C programs at compile time