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@lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/why3-club
