My rcc C compiler has a compile-time contracts and range/interval prover also. Needs -O3.

For full formal proofs it's easier to use cbmc or esbmc though