[Why3-club] [PUBLIC HI-LITE] loops and "Exit" exception

Yannick Moy yannick.moy at adacore.com
Tue Mar 15 09:14:35 CET 2011

* 14/03/2011 15:05, Johannes Kanig:

> * Model the exit statement with another exception, as follows:
>   exception Ada_Exit
>   try
>      while C do
>            if C then raise Ada_Exit
>      done
>   with Ada_Exit -> ()
>   This is a clean solution and does not require any changes to Why3. The
> only problem I have with it is that now there are *two* exceptions and
> exception handling blocks around the loop. I don't know very well the
> behavior of Why3 in this case; do you think it could be a problem?

There should not be any problem with many exceptions and associated handlers
around the loop. The VCgen of Why handles these cases nicely, it is what we used
for exit/continue/return in Frama-C.

So I think there is no need for an infinite loop in Why, just use while (true).

More information about the Why3-club mailing list