Memory Model C - Why3