@@ -0,0 +1,1409 @@
+package wyboogie;%0A%0Aimport wycc.lang.Attribute.Source;%0Aimport wyil.lang.SyntaxTree.Location;%0A%0A/**%0A * Not Implemented errors, with some context information.%0A *%0A * @author Mark Utting%0A */%0A@SuppressWarnings(%22serial%22)%0Apublic class NotImplementedYet extends RuntimeException %7B%0A%09protected Location%3C?%3E location;%0A%0A%09/**%0A%09 * Record a Not Implemented Yet message, with a source file location.%0A%09 *%0A%09 * @param message%0A%09 * @param loc can be null if not known.%0A%09 */%0A%09public NotImplementedYet(String message, Location%3C?%3E loc) %7B%0A%09%09super(message);%0A%09%09location = loc;%0A%09%7D%0A%0A%09public NotImplementedYet(Throwable cause, Location%3C?%3E loc) %7B%0A%09%09super(cause);%0A%09%09location = loc;%0A%09%7D%0A%0A%09public NotImplementedYet(String message, Throwable cause, Location%3C?%3E loc) %7B%0A%09%09super(message, cause);%0A%09%09location = loc;%0A%09%7D%0A%0A%09public NotImplementedYet(String message, Throwable cause, Location%3C?%3E loc, boolean enableSuppression, boolean writableStackTrace) %7B%0A%09%09super(message, cause, enableSuppression, writableStackTrace);%0A%09%09location = loc;%0A%09%7D%0A%0A%09@Override%0A%09public String getMessage() %7B%0A%09%09String msg = super.getMessage();%0A%09%09Source src = null;%0A%09%09if (location != null) %7B%0A%09%09%09src = location.attribute(Source.class);%0A%09%09%09if (src == null) %7B%0A%09%09%09%09src = location.getEnclosingTree().getEnclosingDeclaration().attribute(Source.class);%0A%09%09%09%7D%0A%09%09%7D%0A%09%09if (src == null) %7B%0A%09%09%09return msg + %22 in %22 + location.toString();%0A%09%09%7D else %7B%0A%09%09%09return msg + %22 at %22 + src.toString();%0A%09%09%7D%0A%09%7D%0A%7D%0A

Add special NotImplementedYet exception and throw it whenever we come to a Whiley language construct that is not properly translated to Boogie yet. The goal is to either terminate with an exception, or produce correct Boogie output.