Comment by touisteur

Are you aiming to translate to Why3 like SPARK and Frama-C?