Make Closeable subtype of AutoCloseable, move addSuppressed to Throwable

Added some specifications to addSuppressed so that it is closed automatically

Author: unp1

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/io/Closeable.java

@@ -1,5 +1,5 @@
 package java.io;
 
-public interface Closeable {
+public interface Closeable extends AutoCloseable {
     void close() throws IOException;
-}
+}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Exception.java

@@ -11,6 +11,4 @@ public class Exception extends java.lang.Throwable
    public Exception(java.lang.String arg0, java.lang.Throwable arg1) { super(arg0, arg1); }
    public Exception(java.lang.Throwable arg0) { super(arg0); }
 
-   /// Try-With-Resource
-   public final synchronized void addSuppressed(Throwable exception);
 }

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Throwable.java

@@ -12,6 +12,12 @@ public class Throwable extends java.lang.Object implements java.io.Serializable
 
    //@ protected nullable ghost String message = null;
    //@ protected nullable ghost Throwable cause = null;
+   //@ protected model \seq suppressedExceptions;
+   //@ protected model \locset suppressedListFootprint;
+   //@ accessible suppressedListFootprint: suppressedListFootprint;
+   //@ accessible suppressedExceptions: suppressedListFootprint;
+   //@ protected invariant \intersect(suppressedListFootprint,\set_union(this.message, this.cause))==\empty;
+
 
    /*@ public normal_behavior
      @    requires true;
@@ -78,4 +84,15 @@ public Throwable(java.lang.Throwable arg0) {
    public java.lang.Throwable fillInStackTrace();
 // public java.lang.StackTraceElement[] getStackTrace();
 // public void setStackTrace(java.lang.StackTraceElement[] arg0);
+
+   /// Try-With-Resource
+   /// the helper modifier should not be needed, but otherwise proofs of callers stop because they cannot show the
+   /// throwable invariant
+   /*@ public normal_behavior
+     @ assignable suppressedListFootprint;
+     @ accessible suppressedListFootprint;
+     @ ensures suppressedExceptions == \seq_concat(suppressedExceptions, \seq_singleton(exception));
+    */
+   public /*@ helper @*/ final synchronized void addSuppressed(Throwable exception);
+
 }

key.ui/examples/Java/TryWithResources/TryWithResources.java

@@ -19,7 +19,7 @@ public void m() throws Exception {
         }
     }
 
-    static class Resource implements AutoCloseable {
+    static final class Resource implements AutoCloseable {
         /*@ ensures true; requires true; */
         public void use() {
             // use the resource