[Why3-club] [PUBLIC HI-LITE] loops and "Exit" exception
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
> while C do
> if C then raise Ada_Exit
> 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