...
 
Commits (2)
......@@ -40,8 +40,11 @@
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::addInputCols()].JML normal_behavior operation contract.0";
\proofScript "script 'addInputCols_functional.script';"
......@@ -40,8 +40,11 @@
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::addInputCols()].Non-interference contract.0";
\proofScript "script 'addInputCols_inf_flow.script';"
package java.io;
public final class BufferedInputStream extends java.io.FilterInputStream {
/*@ public normal_behavior
@ assignable \nothing;
@*/
public BufferedInputStream(java.io.InputStream param0);
/*@ public normal_behavior
@ assignable \nothing;
@*/
public int read() throws java.io.IOException;
/*@ public normal_behavior
@ assignable \nothing;
@*/
public void close() throws java.io.IOException;
}
\ No newline at end of file
package java.io;
public class BufferedOutputStream extends java.io.FilterOutputStream {
public BufferedOutputStream(java.io.OutputStream param0);
}
\ No newline at end of file
package java.io;
public class ByteArrayInputStream extends java.io.InputStream {
public ByteArrayInputStream(byte[] param0);
public void close() throws java.io.IOException;
}
\ No newline at end of file
package java.io;
public class ByteArrayOutputStream extends java.io.OutputStream {
public ByteArrayOutputStream();
public byte[] toByteArray();
public void close() throws java.io.IOException;
}
\ No newline at end of file
package java.io;
public interface Closeable extends java.lang.AutoCloseable {
}
\ No newline at end of file
package java.io;
public final class FileInputStream extends java.io.InputStream {
/*@ public normal_behavior
@ assignable \nothing;
@*/
public FileInputStream(java.lang.String param0) throws java.io.FileNotFoundException;
}
\ No newline at end of file
package java.io;
public class FileNotFoundException extends java.io.IOException {
}
\ No newline at end of file
package java.io;
public class FileOutputStream extends java.io.OutputStream {
/*@ public normal_behavior
@ assignable \nothing;
@*/
public FileOutputStream(java.lang.String param0) throws java.io.FileNotFoundException;
}
\ No newline at end of file
package java.io;
public class FileReader extends java.io.InputStreamReader {
/*@ public normal_behavior
@ assignable \nothing;
@*/
public FileReader(java.lang.String param0) throws java.io.FileNotFoundException;
}
\ No newline at end of file
package java.io;
public class FilterInputStream extends java.io.InputStream {
}
\ No newline at end of file
package java.io;
public class FilterOutputStream extends java.io.OutputStream {
protected java.io.OutputStream out;
public void write(byte[] param0, int param1, int param2) throws java.io.IOException;
public void close() throws java.io.IOException;
}
package java.io;
public interface Flushable {
}
\ No newline at end of file
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.io;
public class IOException extends java.lang.Exception
{
public IOException();
public IOException(java.lang.String arg0);
public IOException(java.lang.String arg0, java.lang.Throwable arg1);
public IOException(java.lang.Throwable arg0);
}
package java.io;
public abstract class InputStream extends java.lang.Object implements java.io.Closeable {
public int read(byte[] param0) throws java.io.IOException;
}
\ No newline at end of file
package java.io;
public class InputStreamReader extends java.io.Reader {
}
\ No newline at end of file
package java.io;
public abstract class OutputStream extends java.lang.Object implements java.io.Closeable, java.io.Flushable {
public void write(byte[] param0, int param1, int param2) throws java.io.IOException;
public void close() throws java.io.IOException;
}
\ No newline at end of file
package java.io;
public class PrintStream extends java.io.FilterOutputStream {
public PrintStream(java.io.OutputStream out);
public PrintStream(java.io.OutputStream out, boolean autoFlush);
public void print(boolean b);
public void print(char c);
public void print(int i);
public void print(long l);
// public void print(float f);
// public void print(double d);
public void print(char[] s);
public void print(java.lang.String s);
public void print(java.lang.Object obj);
public void println();
public void println(boolean x);
public void println(char x);
public void println(int x);
public void println(long x);
// public void println(float x);
// public void println(double x);
public void println(char[] x);
public void println(java.lang.String x);
public void println(java.lang.Object x);
}
package java.io;
public abstract class Reader extends java.lang.Object implements java.lang.Readable, java.io.Closeable {
}
\ No newline at end of file
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.io;
public interface Serializable
{
}
public interface Appendable {
}
\ No newline at end of file
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class ArithmeticException extends java.lang.RuntimeException
{
public ArithmeticException() { super(); }
public ArithmeticException(java.lang.String arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class ArrayIndexOutOfBoundsException extends java.lang.IndexOutOfBoundsException
{
public ArrayIndexOutOfBoundsException() { super(); }
public ArrayIndexOutOfBoundsException(int arg0);
public ArrayIndexOutOfBoundsException(java.lang.String arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class ArrayStoreException extends java.lang.RuntimeException
{
public ArrayStoreException() { super(); }
public ArrayStoreException(java.lang.String arg0) { super(arg0); }
}
package java.lang;
public class AssertionError extends java.lang.Error {
public AssertionError() {}
public AssertionError(java.lang.Object detailMessage) {}
public AssertionError(boolean detailMessage){}
public AssertionError(char detailMessage) {}
// public AssertionError(double detailMessage) {}
// public AssertionError(float detailMessage) {}
public AssertionError(int detailMessage) {}
public AssertionError(long detailMessage) {}
}
package java.lang;
/**
* Exists only for proving EVotingMachine
*/
public final class Character extends java.lang.Object implements java.io.Serializable, java.lang.Comparable
{
static int digit(char ch, int radix);
}
\ No newline at end of file
package java.lang;
public final class Class {
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Tue Apr 15 10:18:21 CEST 2008
*/
package java.lang;
public class ClassCastException extends java.lang.RuntimeException
{
public ClassCastException() { super(); }
public ClassCastException(java.lang.String arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class CloneNotSupportedException extends java.lang.Exception
{
public CloneNotSupportedException() { super(); }
public CloneNotSupportedException(java.lang.String arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public interface Cloneable
{
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public interface Comparable
{
public int compareTo(java.lang.Object arg0);
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Jan 31 13:24:50 CET 2014
*/
package java.lang;
public abstract class Enum extends java.lang.Object implements java.lang.Comparable, java.io.Serializable
{
public final java.lang.String name();
public final int ordinal();
protected Enum(java.lang.String arg0, int arg1);
public final java.lang.Class getDeclaringClass();
public static java.lang.Enum valueOf(java.lang.Class arg0, java.lang.String arg1);
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class Error extends java.lang.Throwable
{
public Error() { super(); }
public Error(java.lang.String arg0) { super(arg0); }
public Error(java.lang.String arg0, java.lang.Throwable arg1) { super(arg0, arg1); }
public Error(java.lang.Throwable arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class Exception extends java.lang.Throwable
{
public Exception() { super(); }
public Exception(java.lang.String arg0) { super(arg0); }
public Exception(java.lang.String arg0, java.lang.Throwable arg1) { super(arg0, arg1); }
public Exception(java.lang.Throwable arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class ExceptionInInitializerError extends java.lang.LinkageError
{
public ExceptionInInitializerError() { super(); }
// the following is needed for in some examples to static initialisation:
public ExceptionInInitializerError(java.lang.Throwable arg0) {
super();
initCause(arg0);
}
public ExceptionInInitializerError(java.lang.String arg0) { super(arg0); }
public java.lang.Throwable getException();
public java.lang.Throwable getCause();
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class IllegalArgumentException extends java.lang.RuntimeException
{
public IllegalArgumentException() { super(); }
public IllegalArgumentException(java.lang.String arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class IndexOutOfBoundsException extends java.lang.RuntimeException
{
public IndexOutOfBoundsException() { super(); }
public IndexOutOfBoundsException(java.lang.String arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Jan 31 13:24:50 CET 2014
*/
package java.lang;
public final class Integer implements java.lang.Comparable
{
public final static int MIN_VALUE = -2147483648;
public final static int MAX_VALUE = 2147483647;
public final static java.lang.Class TYPE;
public final static int SIZE = 32;
public static java.lang.String toString(int arg0, int arg1);
public static java.lang.String toHexString(int arg0);
public static java.lang.String toOctalString(int arg0);
public static java.lang.String toBinaryString(int arg0);
public static java.lang.String toString(int arg0);
public static int parseInt(java.lang.String arg0, int arg1) throws java.lang.NumberFormatException;
public static int parseInt(java.lang.String arg0) throws java.lang.NumberFormatException;
public static java.lang.Integer valueOf(java.lang.String arg0, int arg1) throws java.lang.NumberFormatException;
public static java.lang.Integer valueOf(java.lang.String arg0) throws java.lang.NumberFormatException;
public static java.lang.Integer valueOf(int arg0);
public Integer(int arg0);
public Integer(java.lang.String arg0) throws java.lang.NumberFormatException;
public byte byteValue();
public short shortValue();
public int intValue();
public long longValue();
// public float floatValue();
// public double doubleValue();
public static java.lang.Integer getInteger(java.lang.String arg0);
public static java.lang.Integer getInteger(java.lang.String arg0, int arg1);
public static java.lang.Integer getInteger(java.lang.String arg0, java.lang.Integer arg1);
public static java.lang.Integer decode(java.lang.String arg0) throws java.lang.NumberFormatException;
public int compareTo(java.lang.Integer arg0);
public static int highestOneBit(int arg0);
public static int lowestOneBit(int arg0);
public static int numberOfLeadingZeros(int arg0);
public static int numberOfTrailingZeros(int arg0);
public static int bitCount(int arg0);
public static int rotateLeft(int arg0, int arg1);
public static int rotateRight(int arg0, int arg1);
public static int reverse(int arg0);
public static int signum(int arg0);
public static int reverseBytes(int arg0);
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class InterruptedException extends java.lang.Exception
{
public InterruptedException() { super(); }
public InterruptedException(java.lang.String arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public interface Iterable
{
public java.util.Iterator iterator();
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Tue Apr 15 10:18:21 CEST 2008
*/
package java.lang;
public class LinkageError extends java.lang.Error
{
public LinkageError() { super(); }
public LinkageError(java.lang.String arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Tue Apr 15 10:17:24 CEST 2008
*/
package java.lang;
public class NegativeArraySizeException extends java.lang.RuntimeException
{
public NegativeArraySizeException() { super(); }
public NegativeArraySizeException(java.lang.String arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class NoClassDefFoundError extends java.lang.LinkageError
{
public NoClassDefFoundError() { super(); }
public NoClassDefFoundError(java.lang.String arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class NullPointerException extends java.lang.RuntimeException
{
/*@ public normal_behavior
@ ensures message == null && cause == null;
@ assignable message, cause;
@*/
public NullPointerException() { }
/*@ public normal_behavior
@ ensures message == arg0 && cause == null;
@ assignable message, cause;
@*/
public NullPointerException(java.lang.String arg0) {
super(arg0);
}
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Jan 31 13:16:59 CET 2014
*/
package java.lang;
public abstract class Number extends java.lang.Object implements java.io.Serializable
{
public Number();
public abstract int intValue();
public abstract long longValue();
// public abstract float floatValue();
// public abstract double doubleValue();
public byte byteValue();
public short shortValue();
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Jan 31 13:24:50 CET 2014
*/
package java.lang;
public class NumberFormatException extends java.lang.IllegalArgumentException
{
public NumberFormatException() { super(); }
public NumberFormatException(java.lang.String arg0) { super(arg0); }
}
package java.lang;
public class Object {
/*@ public normal_behavior
@ assignable \nothing;
@ assignable<permissions> \nothing;
@*/
public /*@ pure @*/ Object() {}
public /*@ pure @*/ boolean equals(java.lang.Object o);
public int hashCode();
public java.lang.String toString();
protected void finalize() throws java.lang.Throwable {}
protected java.lang.Object clone() throws java.lang.CloneNotSupportedException {}
public final void notify();
public final void notifyAll();
public final void wait() throws java.lang.InterruptedException;
public final void wait(long ms) throws java.lang.InterruptedException;
public final void wait(long ms, int ns)
throws java.lang.InterruptedException;
}
package java.lang;
public class OutOfMemoryError extends java.lang.VirtualMachineError {
public OutOfMemoryError() {}
public OutOfMemoryError(java.lang.String arg0) {}
}
package java.lang;
public interface Runnable{
public void run();
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public class RuntimeException extends java.lang.Exception
{
public RuntimeException() { super(); }
public RuntimeException(java.lang.String arg0) { super(arg0); }
public RuntimeException(java.lang.String arg0, java.lang.Throwable arg1) { super(arg0, arg1); }
public RuntimeException(java.lang.Throwable arg0) { super(arg0); }
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.lang;
public final class String extends java.lang.Object implements java.io.Serializable, java.lang.Comparable
{
// public final static java.util.Comparator CASE_INSENSITIVE_ORDER;
public String();
public String(java.lang.String arg0);
public String(char[] arg0);
public String(char[] arg0, int arg1, int arg2);
public String(int[] arg0, int arg1, int arg2);
public String(byte[] arg0, int arg1, int arg2, int arg3);
public String(byte[] arg0, int arg1);
// public String(byte[] arg0, int arg1, int arg2, java.lang.String arg3) throws java.io.UnsupportedEncodingException;
// public String(byte[] arg0, int arg1, int arg2, java.nio.charset.Charset arg3);
// public String(byte[] arg0, java.lang.String arg1) throws java.io.UnsupportedEncodingException;
// public String(byte[] arg0, java.nio.charset.Charset arg1);
public String(byte[] arg0, int arg1, int arg2);
public String(byte[] arg0);
// public String(java.lang.StringBuffer arg0);
// public String(java.lang.StringBuilder arg0);
public int length();
public boolean isEmpty();
public char charAt(int arg0);
public int codePointAt(int arg0);
public int codePointBefore(int arg0);
public int codePointCount(int arg0, int arg1);
public int offsetByCodePoints(int arg0, int arg1);
public void getChars(int arg0, int arg1, char[] arg2, int arg3);
public void getBytes(int arg0, int arg1, byte[] arg2, int arg3);
// public byte[] getBytes(java.lang.String arg0) throws java.io.UnsupportedEncodingException;
// public byte[] getBytes(java.nio.charset.Charset arg0);
/*@ public normal_behavior
@ ensures \fresh(\result) && \typeof(\result) == \type(byte[]);
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
@ determines \result[*] \by \dl_strContent(this);
@*/
public byte[] getBytes();
public boolean equals(java.lang.Object arg0);
// public boolean contentEquals(java.lang.StringBuffer arg0);
// public boolean contentEquals(java.lang.CharSequence arg0);
public boolean equalsIgnoreCase(java.lang.String arg0);
public int compareTo(java.lang.String arg0);
public int compareToIgnoreCase(java.lang.String arg0);
public boolean regionMatches(int arg0, java.lang.String arg1, int arg2, int arg3);
public boolean regionMatches(boolean arg0, int arg1, java.lang.String arg2, int arg3, int arg4);
public boolean startsWith(java.lang.String arg0, int arg1);
public boolean startsWith(java.lang.String arg0);
public boolean endsWith(java.lang.String arg0);
public int hashCode();
public int indexOf(int arg0);
public int indexOf(int arg0, int arg1);
public int lastIndexOf(int arg0);
public int lastIndexOf(int arg0, int arg1);
public int indexOf(java.lang.String arg0);
public int indexOf(java.lang.String arg0, int arg1);
public int lastIndexOf(java.lang.String arg0);
public int lastIndexOf(java.lang.String arg0, int arg1);
public java.lang.String substring(int arg0);
public java.lang.String substring(int arg0, int arg1);
// public java.lang.CharSequence subSequence(int arg0, int arg1);
public java.lang.String concat(java.lang.String arg0);
public java.lang.String replace(char arg0, char arg1);
public boolean matches(java.lang.String arg0);
// public boolean contains(java.lang.CharSequence arg0);
public java.lang.String replaceFirst(java.lang.String arg0, java.lang.String arg1);
public java.lang.String replaceAll(java.lang.String arg0, java.lang.String arg1);
// public java.lang.String replace(java.lang.CharSequence arg0, java.lang.CharSequence arg1);
public java.lang.String[] split(java.lang.String arg0, int arg1);
public java.lang.String[] split(java.lang.String arg0);
// public java.lang.String toLowerCase(java.util.Locale arg0);
/*@ public normal_behavior
@ ensures \fresh(\result) && \typeof(\result) == \type(String);
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
@ determines \dl_strContent(\result) \by \dl_strContent(this);
@*/
public java.lang.String toLowerCase();
// public java.lang.String toUpperCase(java.util.Locale arg0);
/*@ public normal_behavior
@ ensures \fresh(\result) && \typeof(\result) == \type(String);
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
@ determines \dl_strContent(\result) \by \dl_strContent(this);
@*/
public java.lang.String toUpperCase();
public java.lang.String trim();
public java.lang.String toString();
/*@ public normal_behavior
@ ensures \result.length == \dl_strContent(this).length;
@ ensures (\forall \bigint i; 0 <= i && i < \result.length; \dl_inChar(\result[i]));
@ ensures \fresh(\result) && \typeof(\result) == \type(char[]);
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
@ determines \result[*] \by \dl_strContent(this);
@*/
public char[] toCharArray();
public static java.lang.String format(java.lang.String arg0, java.lang.Object[] arg1);
// public static java.lang.String format(java.util.Locale arg0, java.lang.String arg1, java.lang.Object[] arg2);
public static java.lang.String valueOf(java.lang.Object arg0);
public static java.lang.String valueOf(char[] arg0);
public static java.lang.String valueOf(char[] arg0, int arg1, int arg2);
public static java.lang.String copyValueOf(char[] arg0, int arg1, int arg2);
public static java.lang.String copyValueOf(char[] arg0);
public static java.lang.String valueOf(boolean arg0);
public static java.lang.String valueOf(char arg0);
public static java.lang.String valueOf(int arg0);
public static java.lang.String valueOf(long arg0);
// public static java.lang.String valueOf(float arg0);
// public static java.lang.String valueOf(double arg0);
public java.lang.String intern();
public int compareTo(java.lang.Object arg0);
}
This diff is collapsed.
package java.lang;
public class StringBuffer extends java.lang.Object implements java.io.Serializable, java.lang.Appendable
//, CharSequence
{
public StringBuffer() {}
public StringBuffer(int n);
public StringBuffer(java.lang.String s);
public StringBuffer append(boolean b);
public StringBuffer append(char c);
// public StringBuffer append(char[] str);
// public StringBuffer append(char[] str, int offset, int len);
// public StringBuffer append(double d);
// public StringBuffer append(float f);
public StringBuffer append(int i);
public StringBuffer append(long l);
public StringBuffer append(java.lang.Object obj);
public StringBuffer append(java.lang.StringBuffer sb);
public char charAt(int index) ;
public int length();
// public CharSequence subSequence(int start, int end);
java.lang.String toString();
}
package java.lang;
public final class StringBuilder implements java.io.Serializable, java.lang.Appendable {
public String str;
/*@ public normal_behavior
@ ensures \fresh(this) && \fresh(str) && \typeof(this) == \type(StringBuilder) && \typeof(str) == \type(String);
@ determines str \by \nothing \new_objects str;
@ determines \dl_strContent(str) \by \nothing;
@*/
public /*@pure@*/ StringBuilder();
/*@ public normal_behavior
@ ensures \fresh(this) && \fresh(str) && \typeof(this) == \type(StringBuilder) && \typeof(str) == \type(String);
@ determines str \by \nothing \new_objects str;
@ determines \dl_strContent(str) \by \nothing;
@*/
public /*@pure@*/ StringBuilder(int param0);
/*@ public normal_behavior
@ ensures \fresh(str) && str != null && \typeof(str) == \type(String);
@ ensures \result == this;
@ ensures \fresh(str);
@ assignable str;
@ determines str \by \nothing \new_objects str;
@ determines \dl_strContent(str) \by \dl_strContent(str), param0;
@*/
public java.lang.StringBuilder append(char param0);
public String toString() {
return str;
}
}
\ No newline at end of file
package java.lang;
public final class System {
public static final java.io.InputStream in;
public static final java.io.PrintStream out;
public static final java.io.PrintStream err;
/*@ public behavior
@ requires true;
@ ensures true;
@ assignable \everything;
@*/
public static void arraycopy(java.lang.Object src, int srcPos, java.lang.Object dest, int destPos, int length);
/*@ public behavior
@ ensures false;
@ signals_only \nothing;
@ diverges true;
@*/
public static void exit(int code);
}
package java.lang;
public class Thread{
}
\ No newline at end of file
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*
* Enriched by JML specifications by MU
*
*/
package java.lang;
public class Throwable extends java.lang.Object implements java.io.Serializable
{
//@ protected nullable ghost String message = null;
//@ protected nullable ghost Throwable cause = null;
/*@ public normal_behavior
@ requires true;
@ ensures message == null && cause == null;
@ assignable message, cause;
@*/
public Throwable() { }
/*@ public normal_behavior
@ requires true;
@ ensures message == arg0 && cause == null;
@ assignable message, cause;
@*/
public Throwable(java.lang.String arg0) {
this(arg0, null);
}
/*@ public normal_behavior
@ requires true;
@ ensures message == arg0 && cause == arg1;
@ assignable message, cause;
@*/
public Throwable(java.lang.String arg0, java.lang.Throwable arg1) {
//@ set message = arg0;
//@ set cause = arg1;
}
/*@ public normal_behavior
@ requires true;
@ ensures message == null && cause == arg0;
@ assignable message, cause;
@*/
public Throwable(java.lang.Throwable arg0) {
this(null, arg0);
}
/*@ public normal_behavior
@ ensures \result == message;
@*/
public /*@strictly_pure*/ java.lang.String getMessage();
public java.lang.String getLocalizedMessage();
/*@ public normal_behavior
@ ensures \result == cause;
@*/
public java.lang.Throwable getCause();
/*@ public normal_behavior
@ requires cause == null;
@ ensures \result == this && cause == arg0;
@ assignable cause;
@ helper // needs to be helper because called in constructor
@*/
public java.lang.Throwable initCause(java.lang.Throwable arg0) {
//@ set cause = arg0;
}
public java.lang.String toString();
public void printStackTrace();
// public void printStackTrace(java.io.PrintStream arg0);
// public void printStackTrace(java.io.PrintWriter arg0);
public java.lang.Throwable fillInStackTrace();
// public java.lang.StackTraceElement[] getStackTrace();
// public void setStackTrace(java.lang.StackTraceElement[] arg0);
}
package java.lang;
public abstract class VirtualMachineError extends java.lang.Error {
public VirtualMachineError() {}
public VirtualMachineError(java.lang.String arg0) {}
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Jan 31 13:24:50 CET 2014
*/
package java.lang.annotation;
public interface Annotation
{
public java.lang.Class annotationType();
}
package java.math;
public final class BigInteger extends java.lang.Number implements java.lang.Comparable {
//@ public final ghost \bigint value;
//@ public static invariant java.math.BigInteger.ZERO.value == (\bigint) 0;
public static final java.math.BigInteger ZERO = BigInteger.valueOf(0);
public static BigInteger valueOf(long v) {
BigInteger result = new BigInteger();
//@ set result.value = (\bigint) v;
return result;
}
/*@ public normal_behavior
@ requires true;
@ ensures (\result <= 0) <==> (this.value - param0.value <= 0);
@ ensures (\result >= 0) <==> (this.value - param0.value >= 0);
@ assignable \strictly_nothing;
@ determines \result \by this.value, param0.value;
@*/
public int compareTo(java.math.BigInteger param0);
/*@ public normal_behavior
@ requires true;
@ ensures \result.value == this.value % param0.value;
@ ensures \fresh(\result) && \fresh(\result.*) && \typeof(\result) == \type(BigInteger);
@ assignable \nothing;
@ determines \result \by \nothing \new_objects \result;
@ determines \result.value \by this.value, param0.value;
@*/
public java.math.BigInteger mod(java.math.BigInteger param0);
}
package java.nio;
public abstract class Buffer extends java.lang.Object {
public final java.nio.Buffer flip();
public final int remaining();
public final int position();
public final java.nio.Buffer position(int param0);
}
\ No newline at end of file
package java.nio;
public abstract class ByteBuffer extends java.nio.Buffer implements java.lang.Comparable {
public static java.nio.ByteBuffer allocate(int param0);
public final java.nio.ByteBuffer put(byte[] param0);
public abstract java.nio.ByteBuffer putInt(int param0);
public final byte[] array();
public java.nio.ByteBuffer get(byte[] param0, int param1, int param2);
public static java.nio.ByteBuffer wrap(byte[] param0);
}
\ No newline at end of file
package java.nio.file;
public final class Files extends java.lang.Object {
/*@ public behavior
@ requires true;
@ ensures true;
@ assignable \everything;
@*/
public static java.nio.file.Path write(java.nio.file.Path param0, byte[] param1) throws java.io.IOException;
/*@ public behavior
@ requires true;
@ ensures true;
@ assignable \everything;
@*/
public static java.nio.file.Path write(java.nio.file.Path param0, byte[] param1, java.nio.file.OpenOption[] param2) throws java.io.IOException;
}
\ No newline at end of file
package java.nio.file;
public interface OpenOption {
}
\ No newline at end of file
package java.nio.file;
public interface Path extends java.lang.Comparable, java.lang.Iterable, java.nio.file.Watchable {
public abstract java.lang.String toString();
public abstract java.nio.file.Path resolve(java.lang.String param0);
}
\ No newline at end of file
package java.nio.file;
public final class Paths extends java.lang.Object {
/*@ public normal_behavior
@ requires true;
@ ensures true;
@ assignable \nothing;
@*/
public static java.nio.file.Path get(java.lang.String param0);
/*@ public normal_behavior
@ requires true;
@ ensures true;
@ assignable \nothing;
@*/
public static java.nio.file.Path get(java.lang.String param0, java.lang.String[] param1);
}
\ No newline at end of file
package java.nio.file;
public interface Watchable {
}
\ No newline at end of file
package java.security;
public class GeneralSecurityException extends java.lang.Exception {
}
\ No newline at end of file
package java.security;
public interface Key extends java.io.Serializable {
}
\ No newline at end of file
package java.security;
public final class KeyPair extends java.lang.Object implements java.io.Serializable {
public KeyPair(java.security.PublicKey param0, java.security.PrivateKey param1);
public java.security.PublicKey getPublic();
public java.security.PrivateKey getPrivate();
}
\ No newline at end of file
package java.security;
public abstract class KeyPairGenerator extends java.security.KeyPairGeneratorSpi {
public static java.security.KeyPairGenerator getInstance(java.lang.String param0, java.lang.String param1) throws java.security.NoSuchAlgorithmException, java.security.NoSuchProviderException;
public void initialize(int param0);
public java.security.KeyPair generateKeyPair();
}
\ No newline at end of file
package java.security;
public abstract class KeyPairGeneratorSpi extends java.lang.Object {
}
\ No newline at end of file
package java.security;
public final class MessageDigest extends java.security.MessageDigestSpi {
/*@ public normal_behavior
@ assignable \nothing;
@ determines \result \by \dl_strContent(param0);
@*/
public static java.security.MessageDigest getInstance(java.lang.String param0) throws java.security.NoSuchAlgorithmException;
/*@ public normal_behavior
@ assignable \nothing;
@ ensures \fresh(\result) && \typeof(\result) == \type(byte[]);
@ determines \result \by \nothing \new_objects \result;
@ determines \result[*] \by \nothing;
@*/
public byte[] digest(byte[] param0);
/*@ public normal_behavior
@ requires true;
@ ensures true;
@ assignable \nothing;
@*/
public void update(byte[] param0);
/*@ public normal_behavior
@ assignable \nothing;
@ ensures \fresh(\result) && \typeof(\result) == \type(byte[]);
@ determines \result \by \nothing \new_objects \result;
@ determines \result[*] \by \nothing;
@*/
public byte[] digest();
}
\ No newline at end of file
package java.security;
public abstract class MessageDigestSpi extends java.lang.Object {
}
\ No newline at end of file
package java.security;
public class NoSuchAlgorithmException extends java.security.GeneralSecurityException {
}
\ No newline at end of file
package java.security;
public class NoSuchProviderException extends java.security.GeneralSecurityException {
}
\ No newline at end of file
package java.security;
public interface PrivateKey extends java.security.Key, javax.security.auth.Destroyable {
}
\ No newline at end of file
package java.security;
public abstract class Provider extends java.util.Properties {
}
\ No newline at end of file
package java.security;
public interface PublicKey extends java.security.Key {
}
\ No newline at end of file
package java.security;
public final class SecureRandom extends java.util.Random {
/*@ public normal_behavior
@ assignable param0[*];
@ determines param0[*] \by \nothing;
@*/
public void nextBytes(byte[] param0);
/*@ public normal_behavior
@ assignable \nothing;
@*/
public SecureRandom();
/*@ public normal_behavior
@ assignable \nothing;
@ determines \result \by \nothing;
@*/
public static java.security.SecureRandom getInstanceStrong() throws java.security.NoSuchAlgorithmException;
}
\ No newline at end of file
package java.security;
public final class Security extends java.lang.Object {
public static int addProvider(java.security.Provider param0);
}
\ No newline at end of file
package java.security;
public class SignatureException extends java.security.GeneralSecurityException {
public SignatureException(java.lang.String param0);
}
\ No newline at end of file
package java.security.spec;
public interface AlgorithmParameterSpec {
}
\ No newline at end of file
package java.text;
public abstract class DateFormat extends java.text.Format {
public final java.lang.String format(java.util.Date param0);
}
\ No newline at end of file
package java.text;
public abstract class Format extends java.lang.Object implements java.io.Serializable, java.lang.Cloneable {
}
\ No newline at end of file
package java.text;
public class SimpleDateFormat extends java.text.DateFormat {
public SimpleDateFormat(java.lang.String param0);
}
\ No newline at end of file
package java.util;
public final class ArrayList implements java.util.List {
/*@ public normal_behavior
@ ensures seq.length == 0;
@ ensures \fresh(this) && \fresh(this.*);
@ determines seq \by \nothing;
@*/
public /*@pure@*/ ArrayList();
/*@ public normal_behavior
@ ensures seq == c.seq;
@ ensures \fresh(this) && \fresh(this.*) && \typeof(this) == \type(ArrayList);
@ determines this, seq \by c.seq \new_objects this;
@*/
public /*@pure@*/ ArrayList(Collection c);
}
\ No newline at end of file