[Why3-club] Low level constructs

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Mon Aug 15 21:01:52 CEST 2016

Hi Neil,

There are no gotos in WhyML, as already mentioned by Per.

But WhyML supports exceptions and some gotos (typically forward gotos)
can be translated to exceptions (with a "raise" at the goto place and a
suitable "try with" to handle it at the goto label place).

Of course, if you are interested in the full power of gotos, this is a
different matter.

The ARM paper mentioned by Per builds upon an older paper of mine where
the verification of assembly programs is considered. You can find it
here: http://www.lri.fr/~filliatr/publis/verifmix.pdf
This handles arbitrary control flows, provided any loop in the CFG
contains at least an invariant.

Best regards,

On 15/08/2016 17:07, Neil Evans wrote:
> Hello,
> I'm trying to do a comparison between Why3 and MALPAS, specifically
> WhyML and the MALPAS Intermediate Language (MALPAS IL). (Knowledge of
> MALPAS is not important for answering my query but I thought I'd mention
> it just in case.)
> I would like to know to what extent WhyML can represent low-level
> language constructs such as GOTOs (unconditional jumps to labels) and
> updates to non-local variables (to model side effects). I've looked at
> the manual/tutorial but it's not immediately apparent if these sorts of
> thing are possible or not. These features are available in MALPAS IL but
> it is now old technology and I'm seeking alternative tools to model
> instruction sets and assembly code for formal analysis.
> Thanks,
> Neil.
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/why3-club

More information about the Why3-club mailing list