diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java index b5cd2031913..63f1eed780d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java @@ -25,7 +25,6 @@ * nodes, or the number of interactions. * * @author bruns - * */ public class Statistics { public final int nodes; @@ -447,4 +446,76 @@ private int tmpQuantificationRuleApps(final RuleApp ruleApp) { return res; } } + + public long getAutoModeTimeInMillis() { + return autoModeTimeInMillis; + } + + public int getBlockLoopContractApps() { + return blockLoopContractApps; + } + + public int getBranches() { + return branches; + } + + public int getCachedBranches() { + return cachedBranches; + } + + public int getDependencyContractApps() { + return dependencyContractApps; + } + + public int getInteractiveSteps() { + return interactiveSteps; + } + + public int getLoopInvApps() { + return loopInvApps; + } + + public int getMergeRuleApps() { + return mergeRuleApps; + } + + public int getNodes() { + return nodes; + } + + public int getOperationContractApps() { + return operationContractApps; + } + + public int getOssApps() { + return ossApps; + } + + public int getQuantifierInstantiations() { + return quantifierInstantiations; + } + + public int getSmtSolverApps() { + return smtSolverApps; + } + + public List> getSummaryList() { + return summaryList; + } + + public int getSymbExApps() { + return symbExApps; + } + + public long getTimeInMillis() { + return timeInMillis; + } + + public float getTimePerStepInMillis() { + return timePerStepInMillis; + } + + public int getTotalRuleApps() { + return totalRuleApps; + } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestMiscTools.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestMiscTools.java index 23b76780998..a856c2ee279 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestMiscTools.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestMiscTools.java @@ -21,9 +21,9 @@ import de.uka.ilkd.key.java.recoderext.URLDataLocation; +import org.junit.jupiter.api.Disabled; import org.key_project.util.java.IOUtil; -import org.junit.jupiter.api.Disabled; import org.junit.jupiter.api.Test; import recoder.io.ArchiveDataLocation; import recoder.io.DataFileLocation; @@ -60,7 +60,7 @@ public void testMakeFilenameRelativeUnix() { @Test @Disabled("weigl: Disabled b/c failing on Windows Server (Github Action). " + - "Failing is not reproducible on Windows.") + "Failing is not reproducible on Windows 10.") public void testMakeFilenameRelativeWindows() { // run only on Windows systems if (File.separatorChar != '\\') { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java index 76eca687b4b..af5c07b4511 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java @@ -9,6 +9,8 @@ import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; +import org.checkerframework.checker.initialization.qual.UnderInitialization; + import static de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.SHORTCUT_KEY_MASK; /** @@ -58,6 +60,14 @@ public abstract class KeyAction extends AbstractAction { */ public static final String LOCAL_ACCELERATOR = "LOCAL_ACCELERATOR"; + /// {@inheritDoc} + @Override + public void putValue( + @UnderInitialization(KeyAction.class) KeyAction this, + String key, Object newValue) { + super.putValue(key, newValue); + } + public String getName() { return (String) getValue(NAME); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/util/CommandLine.java b/key.ui/src/main/java/de/uka/ilkd/key/util/CommandLine.java index 7ecbbdefcf9..9529f683453 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/util/CommandLine.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/util/CommandLine.java @@ -10,6 +10,8 @@ import de.uka.ilkd.key.core.Main; +import org.jspecify.annotations.Nullable; + /** * A small framework to handle command lines. * @@ -77,7 +79,7 @@ private class Option extends HelpElement { private String description; private String image; private String value; - private String parameter; + private @Nullable String parameter; @Override protected void print(PrintStream stream, int descriptionCol) { @@ -257,7 +259,7 @@ public boolean subCommandUsed(String name) { * this option (e.g. {@code , time, path}, ... * @param description the description of the option */ - public void addOption(String image, String parameter, String description) { + public void addOption(String image, @Nullable String parameter, String description) { if (!image.startsWith(MINUS)) { throw new IllegalArgumentException( diff --git a/key.util/src/main/java/org/key_project/util/helper/FindResources.java b/key.util/src/main/java/org/key_project/util/helper/FindResources.java index 2b2d8893032..c6731e1bb0a 100644 --- a/key.util/src/main/java/org/key_project/util/helper/FindResources.java +++ b/key.util/src/main/java/org/key_project/util/helper/FindResources.java @@ -168,7 +168,9 @@ public final class FindResources { } public static @Nullable Path getTestCasesDirectory() { - return findFolder("TEST_CASES", "src/test/resources/testcase"); + return findFolder("TEST_CASES", + "src/test/resources/testcase", + "../key.core/src/test/resources/testcase"); } public static @Nullable Path getTestResourcesDirectory() { diff --git a/keyext.proofmanagement/build.gradle b/keyext.proofmanagement/build.gradle index 863f937baa1..97b0b0b90b3 100644 --- a/keyext.proofmanagement/build.gradle +++ b/keyext.proofmanagement/build.gradle @@ -9,7 +9,7 @@ dependencies { implementation project(':key.core') implementation project(':key.ui') - implementation group: 'org.antlr', name: 'ST4', version: '4.3.4' + implementation("org.freemarker:freemarker:2.3.34") } application { @@ -18,6 +18,26 @@ application { applicationName = "pm" } + +def testIntegrationReport = tasks.register('testIntegrationReport', JavaExec) { + group = "verification" + mainClass.set(application.mainClass) + classpath = sourceSets.main.runtimeClasspath + + args('check', '--missing', '--settings', '--report', 'proofManagementReport.html', '--replay', '--dependency', + 'proofBundle/simpleBundleGeneration') +} + +def testIntegrationReport2 = tasks.register('testIntegrationReport2', JavaExec) { + group = "verification" + mainClass.set(application.mainClass) + classpath = sourceSets.main.runtimeClasspath + + args('check', '--missing', '--settings', '--report', 'proofManagementReport.html', '--replay', '--dependency', + 'src/test/pmexample2') +} +test.dependsOn(testIntegrationReport, testIntegrationReport2) + run { // for debugging, something like this can be used: //args('check', '--missing', '--settings', '--report', 'proofManagementReport.html', '--replay', '--dependency', 'pmexample2') @@ -32,3 +52,21 @@ shadowJar { archiveClassifier = "exe" archiveBaseName = "keyext.proofmanagement" } + + + +checkerFramework { + if(System.getProperty("ENABLE_NULLNESS")) { + checkers = [ + "org.checkerframework.checker.nullness.NullnessChecker", + ] + extraJavacArgs = [ + "-AonlyDefs=^org\\.key_project\\.proofmanagement", + "-Xmaxerrs", "10000", + "-Astubs=$projectDir/src/main/checkerframework:permit-nullness-assertion-exception.astub:checker.jar/junit-assertions.astub", + "-AstubNoWarnIfNotFound", + //"-Werror", + "-Aversion", + ] + } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/FilterOutputStream.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/FilterOutputStream.java new file mode 100644 index 00000000000..0ee5a481ecc --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/FilterOutputStream.java @@ -0,0 +1,7 @@ +package java.io; + +public class FilterOutputStream extends java.io.OutputStream { + + protected java.io.OutputStream out; + +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/IOException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/IOException.java new file mode 100644 index 00000000000..ce2a4d5e208 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/IOException.java @@ -0,0 +1,13 @@ +/* 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); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/InputStream.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/InputStream.java new file mode 100644 index 00000000000..34286f49389 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/InputStream.java @@ -0,0 +1,7 @@ +package java.io; + +public class InputStream { + + public InputStream(); + +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/OutputStream.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/OutputStream.java new file mode 100644 index 00000000000..1f7d73f21c1 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/OutputStream.java @@ -0,0 +1,6 @@ +package java.io; + +public class OutputStream { + + +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/PrintStream.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/PrintStream.java new file mode 100644 index 00000000000..cc1a7168f6e --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/PrintStream.java @@ -0,0 +1,27 @@ +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); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/Serializable.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/Serializable.java new file mode 100644 index 00000000000..7cbab07da4f --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/Serializable.java @@ -0,0 +1,9 @@ +/* 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 +{ + +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArithmeticException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArithmeticException.java new file mode 100644 index 00000000000..7c77a788775 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArithmeticException.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArrayIndexOutOfBoundsException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArrayIndexOutOfBoundsException.java new file mode 100644 index 00000000000..1609f29c468 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArrayIndexOutOfBoundsException.java @@ -0,0 +1,12 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArrayStoreException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArrayStoreException.java new file mode 100644 index 00000000000..0a49a9f8e28 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArrayStoreException.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/AssertionError.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/AssertionError.java new file mode 100644 index 00000000000..d1b743af381 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/AssertionError.java @@ -0,0 +1,12 @@ +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) {} +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Character.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Character.java new file mode 100644 index 00000000000..7f65576dac5 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Character.java @@ -0,0 +1,9 @@ +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 diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Class.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Class.java new file mode 100644 index 00000000000..94764a1af19 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Class.java @@ -0,0 +1,8 @@ + + +package java.lang; + + +public final class Class { + +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ClassCastException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ClassCastException.java new file mode 100644 index 00000000000..12a075ba59d --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ClassCastException.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/CloneNotSupportedException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/CloneNotSupportedException.java new file mode 100644 index 00000000000..cb216cab7b5 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/CloneNotSupportedException.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Cloneable.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Cloneable.java new file mode 100644 index 00000000000..6842225aeb0 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Cloneable.java @@ -0,0 +1,9 @@ +/* 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 +{ + +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Comparable.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Comparable.java new file mode 100644 index 00000000000..d90fa74e28f --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Comparable.java @@ -0,0 +1,10 @@ +/* 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); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Enum.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Enum.java new file mode 100644 index 00000000000..2f822fc942a --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Enum.java @@ -0,0 +1,14 @@ +/* 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); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Error.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Error.java new file mode 100644 index 00000000000..b67f5b3cc69 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Error.java @@ -0,0 +1,13 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Exception.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Exception.java new file mode 100644 index 00000000000..5be227222d9 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Exception.java @@ -0,0 +1,13 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ExceptionInInitializerError.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ExceptionInInitializerError.java new file mode 100644 index 00000000000..bba819146a7 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ExceptionInInitializerError.java @@ -0,0 +1,19 @@ +/* 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(); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/IllegalArgumentException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/IllegalArgumentException.java new file mode 100644 index 00000000000..8063a445223 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/IllegalArgumentException.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/IndexOutOfBoundsException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/IndexOutOfBoundsException.java new file mode 100644 index 00000000000..6c5cac27a64 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/IndexOutOfBoundsException.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Integer.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Integer.java new file mode 100644 index 00000000000..d5a9fdb19bc --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Integer.java @@ -0,0 +1,46 @@ +/* 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); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/InterruptedException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/InterruptedException.java new file mode 100644 index 00000000000..922b1daa6a6 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/InterruptedException.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Iterable.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Iterable.java new file mode 100644 index 00000000000..3e5413ae5d1 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Iterable.java @@ -0,0 +1,10 @@ +/* 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(); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/LinkageError.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/LinkageError.java new file mode 100644 index 00000000000..54c8539022d --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/LinkageError.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NegativeArraySizeException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NegativeArraySizeException.java new file mode 100644 index 00000000000..4b816e4ea8d --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NegativeArraySizeException.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NoClassDefFoundError.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NoClassDefFoundError.java new file mode 100644 index 00000000000..04c67bb073c --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NoClassDefFoundError.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NullPointerException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NullPointerException.java new file mode 100644 index 00000000000..8bfd65aaf04 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NullPointerException.java @@ -0,0 +1,23 @@ +/* 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); + } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Number.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Number.java new file mode 100644 index 00000000000..69d2dc26e12 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Number.java @@ -0,0 +1,16 @@ +/* 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(); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NumberFormatException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NumberFormatException.java new file mode 100644 index 00000000000..af79a8454c3 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/NumberFormatException.java @@ -0,0 +1,11 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Object.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Object.java new file mode 100644 index 00000000000..49639aa4ea4 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Object.java @@ -0,0 +1,32 @@ +package java.lang; + +public class Object { + + public int integer; + + + /*@ public normal_behavior + @ assignable \nothing; + @ assignable \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; + +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/OutOfMemoryError.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/OutOfMemoryError.java new file mode 100644 index 00000000000..73b0b475df1 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/OutOfMemoryError.java @@ -0,0 +1,8 @@ + + + +package java.lang; +public class OutOfMemoryError extends java.lang.VirtualMachineError { + public OutOfMemoryError() {} + public OutOfMemoryError(java.lang.String arg0) {} +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Runnable.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Runnable.java new file mode 100644 index 00000000000..18d2e9d9559 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Runnable.java @@ -0,0 +1,7 @@ +package java.lang; + +public interface Runnable{ + + public void run(); + +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/RuntimeException.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/RuntimeException.java new file mode 100644 index 00000000000..29b1e50efc1 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/RuntimeException.java @@ -0,0 +1,13 @@ +/* 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); } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/String.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/String.java new file mode 100644 index 00000000000..5257d1f2de0 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/String.java @@ -0,0 +1,91 @@ +/* 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 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 java.lang.String toLowerCase(); +// public java.lang.String toUpperCase(java.util.Locale arg0); + public java.lang.String toUpperCase(); + public java.lang.String trim(); + public java.lang.String toString(); + 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); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/String.key b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/String.key new file mode 100644 index 00000000000..72a70f71f0a --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/String.key @@ -0,0 +1,1348 @@ +\functions { + Seq strContent(java.lang.String); + java.lang.String strPool(Seq); +} + + +\contracts { + // + // length + // + stringLength { + \programVariables { + int result; + java.lang.String string; + } + true -> + \<{ + result = string.length(); + }\>(result = seqLen(strContent(string))) + \modifiable empty + }; + + + // + // charAt + // + stringCharAtNormal { + \programVariables { + char result; + java.lang.String string; + int charIdx; + java.lang.Throwable exc; + } + (charIdx >= 0 & charIdx < seqLen(strContent(string))) -> + \<{ + #catchAll(exc) { + result = string.charAt(charIdx); + }}\>(exc = null & result = int::seqGet(strContent(string), charIdx)) + \modifiable empty + }; + + stringCharAtExc { + \programVariables { + char result; + java.lang.String string; + int charIdx; + java.lang.Throwable exc; + } + (charIdx < 0 | charIdx >= seqLen(strContent(string))) -> + \<{ + #catchAll(exc) { + result = string.charAt(charIdx); + }}\>( exc != null + & java.lang.IndexOutOfBoundsException::instance(exc) = TRUE) + \modifiable empty + }; + + + // + // concat + // + stringConcatNormal { + \programVariables { + java.lang.String result, calleeStringObj, argumentStringObj; + Heap heapAtPre; + } + (argumentStringObj != null & seqLen(strContent(argumentStringObj)) > 0) -> + {heapAtPre := heap} + \<{ + result = calleeStringObj.concat(argumentStringObj); + }\>( boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null + & strContent(result) = seqConcat(strContent(calleeStringObj), strContent(argumentStringObj)) ) + \modifiable empty + }; + + stringConcatNormalLen0 { + \programVariables { + java.lang.String result, calleeStringObj, argumentStringObj; + } + (argumentStringObj != null & seqLen(strContent(argumentStringObj)) = 0) -> + \<{ + result = calleeStringObj.concat(argumentStringObj); + }\>(result = calleeStringObj) + \modifiable empty + }; + + stringConcatExc { + \programVariables { + java.lang.String result, calleeStringObj, argumentStringObj; + java.lang.Throwable exc; + } + (argumentStringObj = null) -> + \<{ + #catchAll(exc) { + result = calleeStringObj.concat(argumentStringObj); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + + + // + // substring + // + stringSubstringNormal { + \programVariables { + java.lang.String result, string; + int startIdx, endIdx; + Heap heapAtPre; + } + (endIdx >= startIdx & startIdx >= 0 & endIdx <= seqLen(strContent(string))) -> + {heapAtPre := heap} + \<{ + result = string.substring(startIdx, endIdx); + }\>( boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null + & strContent(result) = seqSub(strContent(string),startIdx, endIdx)) + \modifiable empty + }; + + stringSubstringExc { + \programVariables { + java.lang.String result, string; + int startIdx, endIdx; + java.lang.Throwable exc; + } + (startIdx > endIdx | startIdx < 0 | endIdx > seqLen(strContent(string))) -> + \<{ + #catchAll(exc) { + result = string.substring(startIdx, endIdx); + }}\>( exc != null + & java.lang.IndexOutOfBoundsException::instance(exc) = TRUE) + \modifiable empty + }; + + stringSubstring2Normal { + \programVariables { + java.lang.String result, string; + int startIdx; + Heap heapAtPre; + } + (startIdx >= 0 & startIdx < seqLen(strContent(string))) -> + {heapAtPre := heap} + \<{ + result = string.substring(startIdx); + }\>( boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null + & strContent(result) = seqSub( strContent(string), startIdx, seqLen(strContent(string)) ) ) + \modifiable empty + }; + + stringSubstring2Exc { + \programVariables { + java.lang.String result, string; + int startIdx; + java.lang.Throwable exc; + } + (startIdx < 0 | startIdx > seqLen(strContent(string))) -> + \<{ + #catchAll(exc) { + result = string.substring(startIdx); + }}\>( exc != null + & java.lang.IndexOutOfBoundsException::instance(exc) = TRUE) + \modifiable empty + }; + + + // + // compareTo + // + stringCompareToNormal { + \programVariables { + java.lang.String stringCallee, stringArgument; + int result; + } + (stringArgument != null) -> + \<{ + result = stringCallee.compareTo(stringArgument); + }\>( result = \ifEx int i; ( i < seqLen(strContent(stringCallee)) + & i < seqLen(strContent(stringArgument)) + & int::seqGet(strContent(stringCallee),i) + != int::seqGet(strContent(stringArgument),i) ) + \then (int::seqGet(strContent(stringCallee), i) - int::seqGet(strContent(stringArgument), i)) + \else (seqLen(strContent(stringCallee)) - seqLen(strContent(stringArgument))) ) + \modifiable empty + }; + + stringCompareToExc { + \programVariables { + java.lang.String stringCallee, stringArgument; + int result; + java.lang.Throwable exc; + } + (stringArgument = null) -> + \<{ + #catchAll(exc) { + result = stringCallee.compareTo(stringArgument); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + + + // + // endsWith + // + stringEndsWithNormal { + \programVariables { + java.lang.String stringCallee, stringArgument; + boolean result; + } + (stringArgument != null) -> + \<{ + result = stringCallee.endsWith(stringArgument); + }\>(result = TRUE <-> clEndsWith(strContent(stringCallee), strContent(stringArgument))) + \modifiable empty + }; + + stringEndsWithExc { + \programVariables { + java.lang.String stringCallee, stringArgument; + boolean result; + java.lang.Throwable exc; + } + (stringArgument = null) -> + \<{ + #catchAll(exc) { + result = stringCallee.endsWith(stringArgument); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + + // + // startsWith + // + stringStartsWith1Normal { + \programVariables { + java.lang.String stringCallee, stringArgument; + boolean result; + } + (stringArgument != null) -> + \<{ + result = stringCallee.startsWith(stringArgument); + }\>(result = TRUE <-> clStartsWith(strContent(stringCallee), strContent(stringArgument))) + \modifiable empty + }; + + stringStartsWith1Exc { + \programVariables { + java.lang.String stringCallee, stringArgument; + boolean result; + java.lang.Throwable exc; + } + (stringArgument = null) -> + \<{ + #catchAll(exc) { + result = stringCallee.startsWith(stringArgument); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + stringStartsWith2Normal { + \programVariables { + java.lang.String stringCallee, stringArgument; + boolean result; + int startIdx; + } + (stringArgument != null) -> + \<{ + result = stringCallee.startsWith(stringArgument, startIdx); + }\>(result = TRUE <-> ( (startIdx >= 0) + & (startIdx <= seqLen(strContent(stringCallee))) + & clStartsWith(seqSub(strContent(stringCallee), startIdx, seqLen(strContent(stringCallee))), + strContent(stringArgument)) + ) ) + \modifiable empty + }; + + stringStartsWith2Exc { + \programVariables { + java.lang.String stringCallee, stringArgument; + boolean result; + int startIdx; + java.lang.Throwable exc; + } + (stringArgument = null) -> + \<{ + #catchAll(exc) { + result = stringCallee.startsWith(stringArgument, startIdx); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + + // + // replace + // + stringReplaceNormal { + \programVariables { + java.lang.String s, result; + char c1, c2; + Heap heapAtPre; + } + true -> + {heapAtPre := heap} + \<{ + result = s.replace(c1,c2); + }\>(\if (\exists int i; ( i >= 0 + & i < seqLen(strContent(s)) + & int::seqGet(strContent(s), i) = c1)) + \then( boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null + & strContent(result) = clReplace(strContent(s), c1, c2) ) + \else ( result = s )) + \modifiable empty + }; + + + // + // indexOf + // + stringIndexOfNormal { + \programVariables { + java.lang.String s; + int charVal; + int result; + } + true -> + \<{ + result = s.indexOf(charVal); + }\> ( result = clIndexOfChar ( strContent(s), charVal, 0 ) ) + \modifiable empty + }; + + stringIndexOfFromNormal { + \programVariables { + java.lang.String s; + int charVal, from; + int result; + } + true -> + \<{ + result = s.indexOf(charVal,from); + }\>( result = clIndexOfChar(strContent(s), charVal, from) ) + \modifiable empty + }; + + stringIndexOfStringNormal { + \programVariables { + java.lang.String s, t; + int result; + } + (t != null) -> + \<{ + result = s.indexOf(t); + }\>(result = clIndexOfCl(strContent(s), 0, strContent(t))) + \modifiable empty + }; + + stringIndexOfStringExc { + \programVariables { + java.lang.String s, t; + int result; + java.lang.Throwable exc; + } + (t = null) -> + \<{ + #catchAll (exc) { + result = s.indexOf(t); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + stringIndexOfStringFromNormal { + \programVariables { + java.lang.String s, t; + int result, from; + } + (t != null) -> + \<{ + result = s.indexOf(t, from); + }\>(result = clIndexOfCl(strContent(s), from, strContent(t))) + \modifiable empty + }; + + stringIndexOfStringFromExc { + \programVariables { + java.lang.String s, t; + int result, from; + java.lang.Throwable exc; + } + (t = null) -> + \<{ + #catchAll (exc) { + result = s.indexOf(t,from); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + + // + // lastIndexOf + // + stringLastIndexOfNormal { + \programVariables { + java.lang.String s; + int charVal; + int result; + } + true -> + \<{ + result = s.lastIndexOf(charVal); + }\>(result = clLastIndexOfChar(strContent(s), charVal, seqLen(strContent(s)) - 1)) + \modifiable empty + }; + + stringLastIndexOfFromNormal { + \programVariables { + java.lang.String s; + int charVal, from; + int result; + } + true -> + \<{ + result = s.lastIndexOf(charVal, from); + }\>(result = clLastIndexOfChar(strContent(s), charVal, from)) + \modifiable empty + }; + + stringLastIndexOfStringNormal { + \programVariables { + java.lang.String s, t; + int result; + } + (t != null) -> + \<{ + result = s.lastIndexOf(t); + }\>(result = clLastIndexOfCl(strContent(s), + seqLen(strContent(s)) - 1, + strContent(t))) + \modifiable empty + }; + + stringLastIndexOfStringExc { + \programVariables { + java.lang.String s, t; + int result; + java.lang.Throwable exc; + } + (t = null) -> + \<{ + #catchAll (exc) { + result = s.lastIndexOf(t); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + stringLastIndexOfStringFromNormal { + \programVariables { + java.lang.String s, t; + int result, from; + } + (t != null) -> + \<{ + result = s.lastIndexOf(t, from); + }\>(result = clLastIndexOfCl(strContent(s), from, strContent(t))) + \modifiable empty + }; + + stringLastIndexOfStringFromExc { + \programVariables { + java.lang.String s, t; + int result, from; + java.lang.Throwable exc; + } + (t = null) -> + \<{ + #catchAll (exc) { + result = s.lastIndexOf(t, from); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + + // + // toString + // + stringToStringNormal { + \programVariables { + java.lang.String s, result; + } + true -> + \<{ + result = s.toString(); + }\>(result = s) + \modifiable empty + }; + + + // + // equals + // + stringEqualsNormal { + \programVariables { + java.lang.String s; + java.lang.Object obj; + boolean result; + } + true -> + \<{ + result = s.equals(obj); + }\>( result = TRUE <-> ( obj != null + & java.lang.String::instance(obj) = TRUE + & strContent(s) = strContent((java.lang.String)obj) )) + \modifiable empty + }; + + + // + // isEmpty + // + stringIsEmptyNormal { + \programVariables { + java.lang.String s; + boolean result; + } + true -> + \<{ + result = s.isEmpty(); + }\>( result = TRUE <-> strContent(s) = seqEmpty ) + \modifiable empty + }; + + + // + // copyValueOf + // + stringCopyValueOfNormal { + \programVariables { + java.lang.String result; + char[] data; + Heap heapAtPre; + } + (data != null) -> + {heapAtPre := heap} + \<{ + result = java.lang.String.copyValueOf(data); + }\>( seqLen(strContent(result)) = data.length + & \forall int i; ((i >= 0 & i < data.length) + -> int::seqGet(strContent(result),i) = data[i] ) + & boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null ) + \modifiable empty + }; + + stringCopyValueOfExc { + \programVariables { + java.lang.String result; + char[] data; + java.lang.Throwable exc; + } + (data = null) -> + \<{ + #catchAll (exc) { + result = java.lang.String.copyValueOf(data); + }}\> ( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + stringCopyValueOfRangeNormal { + \programVariables { + java.lang.String result; + char[] data; + int offset, count; + Heap heapAtPre; + } + ( data != null + & offset >= 0 + & count >= 0 + & offset+count <= data.length) + -> + {heapAtPre := heap} + \<{ + result = java.lang.String.copyValueOf(data, offset, count); + }\>( seqLen(strContent(result)) = count + & \forall int i; ((i >= 0 & i < count) + -> int::seqGet(strContent(result), i) = data[i+offset] ) + & boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null ) + \modifiable empty + }; + + stringCopyValueOfRangeExcBounds { + \programVariables { + java.lang.String result; + char[] data; + int offset, count; + java.lang.Throwable exc; + } + ( data != null + & ( offset < 0 + | count < 0 + | offset+count > data.length)) + -> + \<{ + #catchAll (exc) { + result = java.lang.String.copyValueOf (data,offset,count); + }}\>( exc != null + & java.lang.IndexOutOfBoundsException::instance(exc) = TRUE) + \modifiable empty + }; + + stringCopyValueOfRangeExcNull { + \programVariables { + java.lang.String result; + char[] data; + int offset, count; + java.lang.Throwable exc; + } + (data = null) -> + \<{ + #catchAll (exc) { + result = java.lang.String.copyValueOf(data, offset, count); + }}\> ( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + + // + // getChars + // + stringGetCharsNormal { + \programVariables { + java.lang.String s; + char[] dst; + int srcBegin, srcEnd, dstBegin; + Heap heapAtPre; + } + ( dst != null + & srcBegin >= 0 + & srcBegin <= srcEnd + & srcEnd <= seqLen(strContent(s)) + & dstBegin >= 0 + & dstBegin + (srcEnd - srcBegin) <= dst.length ) + -> + {heapAtPre := heap} + \<{ + s.getChars(srcBegin, srcEnd, dst, dstBegin); + }\>(\forall int i; ( ((i >= 0 & i < (srcEnd - srcBegin)) + -> int::seqGet(strContent(s), srcBegin + i) = dst[dstBegin + i]) + & ((i >= 0 & i < dstBegin) + -> dst[i] = int::select(heapAtPre, dst, arr(i))) + & ((i >= dstBegin + (srcEnd - srcBegin) & i < dst.length) + -> dst[i] = int::select(heapAtPre, dst, arr(i))) )) + \modifiable allFields(dst) + }; + + stringGetCharsExcBounds { + \programVariables { + java.lang.String s; + char[] dst; + int srcBegin, srcEnd, dstBegin; + java.lang.Throwable exc; + } + ( dst != null + & ( srcBegin < 0 + | srcBegin > srcEnd + | srcEnd > seqLen(strContent(s)) + | dstBegin < 0 + | dstBegin + (srcEnd - srcBegin) > dst.length )) + -> + \<{ + #catchAll (exc) { + s.getChars(srcBegin, srcEnd, dst, dstBegin); + }}\>( exc != null + & java.lang.IndexOutOfBoundsException::instance(exc) = TRUE) + \modifiable empty + }; + + stringGetCharsExcNull { + \programVariables { + java.lang.String s; + char[] dst; + int srcBegin, srcEnd, dstBegin; + java.lang.Throwable exc; + } + (dst = null) -> + \<{ + #catchAll (exc) { + s.getChars(srcBegin, srcEnd, dst, dstBegin); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE) + \modifiable empty + }; + + + // + // toCharArray + // + stringToCharArray { + \programVariables { + java.lang.String s; + char[] result; + Heap heapAtPre; + } + true -> + {heapAtPre := heap} + \<{ + result = s.toCharArray(); + }\>( result != null + & result.length = seqLen(strContent(s)) + & \forall int i; ((i >= 0 & i < seqLen(strContent(s))) + -> int::seqGet(strContent(s), i) = result[i]) + & boolean::select(heapAtPre, result, java.lang.Object::) = FALSE) + \modifiable empty + }; + + + // + // valueOf + // + stringValueOfBoolean { + \programVariables { + java.lang.String result; + boolean bVal; + Heap heapAtPre; + } + true -> + {heapAtPre := heap} + \<{ + result = java.lang.String.valueOf(bVal); + }\>(strContent(result) = \if (bVal = TRUE) + \then ( "true" ) + \else ( "false" ) + & boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null ) + \modifiable empty + }; + + stringValueOfChar { + \programVariables { + java.lang.String result; + char charVal; + Heap heapAtPre; + } + true -> + {heapAtPre := heap} + \<{ + result = java.lang.String.valueOf(charVal); + }\>( strContent(result) = seqSingleton(charVal) + & boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null ) + \modifiable empty + }; + + stringValueOfCharArrayNormal { + \programVariables { + java.lang.String result; + char[] data; + Heap heapAtPre; + } + (data != null) -> + {heapAtPre := heap} + \<{ + result = java.lang.String.valueOf(data); + }\>( (\forall int i; ((i >= 0 & i < data.length) + -> int::seqGet(strContent(result), i) = data[i])) + & seqLen(strContent(result)) = data.length + & boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null ) + \modifiable empty + }; + + stringValueOfCharArrayExc { + \programVariables { + java.lang.String result; + char[] data; + java.lang.Throwable exc; + } + (data = null) -> + \<{ + #catchAll (exc) { + result = java.lang.String.valueOf(data); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE ) + \modifiable empty + }; + + stringValueOfInt { + \programVariables { + java.lang.String result; + int iVal; + Heap heapAtPre; + } + true -> + {heapAtPre := heap} + \<{ + result = java.lang.String.valueOf(iVal); + }\>( strContent(result) = clRemoveZeros(clTranslateInt(iVal)) + & boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null ) + \modifiable empty + }; + + stringValueOfLong { + \programVariables { + java.lang.String result; + long lVal; + Heap heapAtPre; + } + true -> + {heapAtPre := heap} + \<{ + result = java.lang.String.valueOf(lVal); + }\>( strContent(result) = clRemoveZeros(clTranslateInt(lVal)) + & boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null ) + \modifiable empty + }; + + stringValueOfCharArrayRangeNormal { + \programVariables { + java.lang.String result; + char[] data; + int offset, count; + Heap heapAtPre; + } + ( data != null & offset >= 0 & count >= 0 + & offset + count <= data.length) + -> + {heapAtPre := heap} + \<{ + result = java.lang.String.valueOf(data, offset, count); + }\>( (\forall int i; ((i >= 0 & i < count) + -> int::seqGet(strContent(result), i) = data[offset + i])) + & seqLen(strContent(result)) = count + & boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null ) + \modifiable empty + }; + + stringValueOfCharArrayRangeExcBounds { + \programVariables { + java.lang.String result; + char[] data; + int offset, count; + java.lang.Throwable exc; + } + ( data != null + & (offset < 0 | count < 0 | offset+count > data.length)) + -> + \<{ + #catchAll (exc) { + result = java.lang.String.valueOf(data, offset, count); + }}\>( exc != null + & java.lang.IndexOutOfBoundsException::instance(exc) = TRUE ) + \modifiable empty + }; + + stringValueOfCharArrayRangeExcNull { + \programVariables { + java.lang.String result; + char[] data; + int offset, count; + java.lang.Throwable exc; + } + (data = null) -> + \<{ + #catchAll (exc) { + result = java.lang.String.valueOf(data, offset, count); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE ) + \modifiable empty + }; + + stringValueOfObjectNull { + \programVariables { + java.lang.String result; + java.lang.Object obj; + Heap heapAtPre; + } + obj = null -> + {heapAtPre := heap} + \<{ + result = java.lang.String.valueOf(obj); + }\>( strContent(result) = "null" + & boolean::select(heapAtPre, result, java.lang.Object::) = FALSE + & result != null ) + \modifiable empty + }; + + stringValueOfObjectNonNull { + \programVariables { + java.lang.String result; + java.lang.Object obj; + } + obj != null -> + \<{ + result = java.lang.String.valueOf(obj); + }\>( result = obj.toString() ) + \modifiable empty + }; + + + // + // hashCode + // + stringHashCode { + \programVariables { + java.lang.String s; + int result; + } + true -> + \<{ + result = s.hashCode(); + }\>(result = clHashCode(strContent(s))) + \modifiable empty + }; + + + // + // intern + // + stringIntern { + \programVariables { + java.lang.String s; + String result; + Heap heapAtPre; + } + true -> + {heapAtPre:=heap}\<{ + result = s.intern(); + }\>(result != null & result = strPool(strContent(s)) & + boolean::select(heap, result, java.lang.Object::) = TRUE) + \modifiable false + }; + + + // + // Constructors + // + stringConstrNormal { + \programVariables { + java.lang.String s; + } + true -> + \<{ + s = new String(); + }\>(strContent(s) = seqEmpty) + \modifiable empty + }; + + stringConstrCharArrayNormal { + \programVariables { + java.lang.String s; + char[] v; + } + (v != null) -> + \<{ + s = new String(v); + }\>( seqLen ( strContent ( s ) ) = v.length + & \forall int i; ((i >= 0 & i < v.length) + -> int::seqGet(strContent(s), i) = v[i]) ) + \modifiable empty + }; + + stringConstrCharArrayExc { + \programVariables { + java.lang.String s; + char[] v; + java.lang.Throwable exc; + } + (v = null) -> + \<{ + #catchAll (exc) { + s = new String(v); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE ) + \modifiable empty + }; + + stringConstrCharArrayRangeNormal { + \programVariables { + java.lang.String s; + char[] v; + int offset, count; + } + ( v != null & offset >= 0 + & count >= 0 & offset + count <= v.length) -> + \<{ + s = new String(v, offset, count); + }\>( seqLen(strContent(s)) = count + & \forall int i; ((i >= 0 & i < count) + -> int::seqGet(strContent(s), i) = v[offset+i]) ) + \modifiable empty + }; + + stringConstrCharArrayRangeExcBounds { + \programVariables { + java.lang.String s; + char[] v; + int offset, count; + java.lang.Throwable exc; + } + (v != null & (offset < 0 | count < 0 | offset + count > v.length)) + -> + \<{ + #catchAll(exc) { + s = new String(v, offset, count); + }}\>( exc != null + & java.lang.IndexOutOfBoundsException::instance(exc) = TRUE ) + \modifiable empty + }; + + stringConstrCharArrayRangeExcNull { + \programVariables { + java.lang.String s; + char[] v; + int offset, count; + java.lang.Throwable exc; + } + (v = null) -> + \<{ + #catchAll(exc) { + s = new String(v, offset, count); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE ) + \modifiable empty + }; + + stringConstrCopyNormal { + \programVariables { + java.lang.String s, t; + } + (t != null) -> + \<{ + s = new String(t); + }\>( strContent(s) = strContent(t) ) + \modifiable empty + }; + + stringConstrCopyExc { + \programVariables { + java.lang.String s, t; + java.lang.Throwable exc; + } + (t = null) -> + \<{ + #catchAll(exc) { + s = new String(t); + }}\>( exc != null + & java.lang.NullPointerException::instance(exc) = TRUE ) + \modifiable empty + }; +} + +/* + * Program Rules for Strings + */ +\rules { + + poolKeyIsContentOfValue { + \schemaVar \term Seq slit; + \find (strContent(strPool(slit))) + \replacewith(slit) + \heuristics (simplify) + }; + + + poolIsInjective { + \schemaVar \term Seq slit1, slit2; + \find (strPool(slit1) = strPool(slit2)) + \replacewith(slit1 = slit2) + \heuristics (simplify) + }; + + + insert_constant_string_value { + \schemaVar \program ConstantStringVariable #csv; + \assumes(wellFormed(heap) ==>) + \find(#csv) + \sameUpdateLevel + \replacewith(\if (#constantvalue(#csv) = null) \then (null) \else (strPool((Seq)#constantvalue(#csv))) ) + \heuristics(concrete) + }; + + + nullString { + \find ( strContent(null) ) + \replacewith("null") + \heuristics(concrete) + }; + + + // + // Assignment of a Literal + // + stringAssignment { + \schemaVar \modalOperator { diamond, box} #normalassign; + \schemaVar \program Variable #v; + \schemaVar \program StringLiteral #slit; + \schemaVar \formula post; + + \find (\modality{#normalassign}{.. #v = #slit; ...}\endmodality(post)) + \sameUpdateLevel + + \replacewith ({ #v := strPool(#slit) } + \modality{#normalassign}{.. ...}\endmodality(post)) + \add(strPool(#slit) != null, boolean::select(heap, strPool(#slit), java.lang.Object::) = TRUE ==>) + + \heuristics (simplify_prog, simplify_prog_subset) + }; + + + // + // The "+" operator + // + stringConcat { + \schemaVar \modalOperator { diamond, box } #normalassign; + \schemaVar \program Variable #v; + \schemaVar \program SimpleStringExpression #sstr1, #sstr2; + \schemaVar \formula post; + \schemaVar \skolemTerm java.lang.String sk; + + \find ( \modality{#normalassign} {.. + #v = #sstr1 + #sstr2; + ...}\endmodality(post)) + \sameUpdateLevel + \varcond(\newDependingOn(sk, post)) + + \replacewith ( { #v := sk } + { heap := create(heap, sk) } + \modality{#normalassign}{.. ...}\endmodality(post) ) + \add(strContent(sk) = seqConcat(strContent(#sstr1), strContent(#sstr2)) ==> sk = null) + \heuristics (simplify_prog, simplify_prog_subset) + }; + + + stringConcatIntExpLeft { + \schemaVar \modalOperator { diamond, box } #normalassign; + \schemaVar \program Variable #v; + \schemaVar \program SimpleStringExpression #sstrRight; + \schemaVar \program AnyJavaTypeExpression #seLeft; + \schemaVar \formula post; + \schemaVar \skolemTerm java.lang.String sk; + + \find ( \modality{#normalassign} + {.. #v = #seLeft + #sstrRight; ...} + \endmodality(post)) + \sameUpdateLevel + \varcond(\newDependingOn(sk, post)) + + \replacewith ( { #v := sk } + { heap := create(heap, sk) } + \modality{#normalassign}{.. ...}\endmodality(post) ) + \add(strContent(sk) = seqConcat(clTranslateInt(#seLeft), strContent(#sstrRight)) ==> sk = null) + \heuristics (simplify_prog, simplify_prog_subset) + }; + + + stringConcatIntExpRight { + \schemaVar \modalOperator { diamond, box } #normalassign; + \schemaVar \program Variable #v; + \schemaVar \program SimpleStringExpression #sstrLeft; + \schemaVar \program AnyJavaTypeExpression #seRight; + \schemaVar \formula post; + \schemaVar \skolemTerm java.lang.String sk; + + \find ( \modality{#normalassign} + {.. #v = #sstrLeft + #seRight; ...} + \endmodality(post)) + \sameUpdateLevel + \varcond(\newDependingOn(sk, post)) + + \replacewith ( { #v := sk } + { heap := create(heap, sk) } + \modality{#normalassign}{.. ...}\endmodality(post) ) + \add(strContent(sk) = seqConcat(strContent(#sstrLeft), clTranslateInt(#seRight)) ==> sk = null) + \heuristics (simplify_prog, simplify_prog_subset) + }; + + stringConcatCharExpLeft { + \schemaVar \modalOperator { diamond, box } #normalassign; + \schemaVar \program Variable #v; + \schemaVar \program SimpleStringExpression #sstrRight; + \schemaVar \program JavaCharExpression #seLeft; + \schemaVar \formula post; + \schemaVar \skolemTerm java.lang.String sk; + + \find ( \modality{#normalassign} + {.. #v = #seLeft + #sstrRight; ...} + \endmodality(post)) + \sameUpdateLevel + \varcond(\newDependingOn(sk, post)) + + \replacewith ( { #v := sk } + { heap := create(heap, sk) } + \modality{#normalassign}{.. ...}\endmodality(post) ) + \add(strContent(sk) = seqConcat(seqSingleton(#seLeft), strContent(#sstrRight)) ==> sk = null) + \heuristics (simplify_prog, simplify_prog_subset) + }; + + + stringConcatCharExpRight { + \schemaVar \modalOperator { diamond, box } #normalassign; + \schemaVar \program Variable #v; + \schemaVar \program SimpleStringExpression #sstrLeft; + \schemaVar \program JavaCharExpression #seRight; + \schemaVar \formula post; + \schemaVar \skolemTerm java.lang.String sk; + + \find ( \modality{#normalassign} + {.. #v = #sstrLeft + #seRight; ...} + \endmodality(post)) + \sameUpdateLevel + \varcond(\newDependingOn(sk, post)) + + \replacewith ( { #v := sk } + { heap := create(heap, sk) } + \modality{#normalassign}{.. ...}\endmodality(post) ) + \add(strContent(sk) = seqConcat(strContent(#sstrLeft), seqSingleton(#seRight)) ==> sk = null) + \heuristics (simplify_prog, simplify_prog_subset) + }; + + stringConcatBooleanLeft { + \schemaVar \modalOperator { diamond, box } #normalassign; + \schemaVar \program Variable #v; + \schemaVar \program SimpleStringExpression #sstrRight; + \schemaVar \program SimpleJavaBooleanExpression #seLeft; + \schemaVar \formula post; + \schemaVar \skolemTerm java.lang.String sk; + + \find ( \modality{#normalassign} + {.. #v = #seLeft + #sstrRight; ...} + \endmodality(post)) + \sameUpdateLevel + \varcond(\newDependingOn(sk, post)) + + \replacewith ( { #v := sk } + { heap := create(heap, sk) } + \modality{#normalassign}{.. ...}\endmodality(post) ) + \add(strContent(sk) = seqConcat(\if (#seLeft = TRUE) + \then ( "true" ) + \else ( "false" ), + strContent(#sstrRight)) ==> sk = null) + \heuristics (simplify_prog, simplify_prog_subset) + }; + + + stringConcatBooleanRight { + \schemaVar \modalOperator { diamond, box } #normalassign; + \schemaVar \program Variable #v; + \schemaVar \program SimpleStringExpression #sstrLeft; + \schemaVar \program SimpleJavaBooleanExpression #seRight; + \schemaVar \formula post; + \schemaVar \skolemTerm java.lang.String sk; + + \find ( \modality{#normalassign} + {.. #v = #sstrLeft + #seRight; ...} + \endmodality(post)) + \sameUpdateLevel + \varcond(\newDependingOn(sk, post)) + + \replacewith ( { #v := sk } + { heap := create(heap, sk) } + \modality{#normalassign}{.. ...}\endmodality(post) ) + \add(strContent(sk) = seqConcat(strContent(#sstrLeft), + \if (#seRight = TRUE) + \then ("true") + \else ("false") )==> sk = null) + \heuristics (simplify_prog, simplify_prog_subset) + }; + + + stringConcatObjectLeft { + \schemaVar \modalOperator { diamond, box } #normalassign; + \schemaVar \program Variable #v; + \schemaVar \program SimpleStringExpression #sstrRight; + \schemaVar \program SimpleNonStringObjectExpression #seLeft; + \schemaVar \formula post; + \schemaVar \skolemTerm java.lang.String sk; + + \find ( \modality{#normalassign} + {.. #v = #seLeft + #sstrRight; ...} + \endmodality(post)) + \sameUpdateLevel + \varcond(\newDependingOn(sk, post)) + + "#seLeft not null": + \replacewith ( + \modality{#normalassign} + {.. #v = #seLeft.toString() + #sstrRight; ...} + \endmodality(post) ) + \add(==> #seLeft = null); + + "#seLeft null": + \replacewith ( { #v := sk } + { heap := create(heap, sk) } + \modality{#normalassign}{.. ...}\endmodality(post) ) + \add(#seLeft = null, strContent(sk) = seqConcat(strContent(null), strContent(#sstrRight)) ==> sk = null) + + \heuristics (simplify_prog, simplify_prog_subset) + }; + + + stringConcatObjectRight { + \schemaVar \modalOperator { diamond, box } #normalassign; + \schemaVar \program Variable #v; + \schemaVar \program SimpleStringExpression #sstrLeft; + \schemaVar \program SimpleNonStringObjectExpression #seRight; + \schemaVar \formula post; + \schemaVar \skolemTerm java.lang.String sk; + + \find ( \modality{#normalassign} + {.. #v = #sstrLeft + #seRight; ...} + \endmodality(post)) + \sameUpdateLevel + \varcond(\newDependingOn(sk, post)) + + "#seRight not null": + \replacewith ( + \modality{#normalassign} + {.. #v = #sstrLeft + #seRight.toString(); ...} + \endmodality(post) ) + \add(==> #seRight = null); + + "#seRight null": + \replacewith ( { #v := sk } + { heap := create(heap, sk) } + \modality{#normalassign}{.. ...}\endmodality(post) ) + \add(#seRight = null, strContent(sk) = seqConcat(strContent(#sstrLeft), strContent(null)) ==> sk = null) + + \heuristics (simplify_prog, simplify_prog_subset) + }; +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/StringBuffer.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/StringBuffer.java new file mode 100644 index 00000000000..77f7a386c45 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/StringBuffer.java @@ -0,0 +1,25 @@ +package java.lang; + +public class StringBuffer extends java.lang.Object implements java.io.Serializable + //, 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(); + } diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/System.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/System.java new file mode 100644 index 00000000000..8f4270709fc --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/System.java @@ -0,0 +1,9 @@ +package java.lang; + +public class System { + + public static final java.io.InputStream in; + public static final java.io.PrintStream out; + public static final java.io.PrintStream err; + +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Thread.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Thread.java new file mode 100644 index 00000000000..e1731e5f730 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Thread.java @@ -0,0 +1,7 @@ +package java.lang; + +public class Thread{ + + + +} \ No newline at end of file diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Throwable.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Throwable.java new file mode 100644 index 00000000000..d9b2084784a --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Throwable.java @@ -0,0 +1,82 @@ +/* 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(); + + // TODO There should be "cause != this" as another precondition. + /*@ 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; + return this; + } + + 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); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/VirtualMachineError.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/VirtualMachineError.java new file mode 100644 index 00000000000..2901620eb3a --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/VirtualMachineError.java @@ -0,0 +1,8 @@ + + + +package java.lang; +public abstract class VirtualMachineError extends java.lang.Error { + public VirtualMachineError() {} + public VirtualMachineError(java.lang.String arg0) {} +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/annotation/Annotation.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/annotation/Annotation.java new file mode 100644 index 00000000000..ed8b65547ec --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/annotation/Annotation.java @@ -0,0 +1,10 @@ +/* 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(); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Collection.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Collection.java new file mode 100644 index 00000000000..eba0a4dd421 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Collection.java @@ -0,0 +1,24 @@ +/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker) + * Date: Fri Mar 28 13:47:08 CET 2008 + */ +package java.util; + +public interface Collection extends java.lang.Iterable +{ + + public int size(); + public boolean isEmpty(); + public boolean contains(java.lang.Object arg0); + public java.util.Iterator iterator(); + public java.lang.Object[] toArray(); + public java.lang.Object[] toArray(java.lang.Object[] arg0); + public boolean add(java.lang.Object arg0); + public boolean remove(java.lang.Object arg0); + public boolean containsAll(java.util.Collection arg0); + public boolean addAll(java.util.Collection arg0); + public boolean removeAll(java.util.Collection arg0); + public boolean retainAll(java.util.Collection arg0); + public void clear(); + public boolean equals(java.lang.Object arg0); + public int hashCode(); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Iterator.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Iterator.java new file mode 100644 index 00000000000..62675536038 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Iterator.java @@ -0,0 +1,12 @@ +/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker) + * Date: Fri Mar 28 13:47:08 CET 2008 + */ +package java.util; + +public interface Iterator +{ + + public boolean hasNext(); + public java.lang.Object next(); + public void remove(); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/List.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/List.java new file mode 100644 index 00000000000..c219a96503c --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/List.java @@ -0,0 +1,34 @@ +/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker) + * Date: Fri Mar 28 13:47:08 CET 2008 + */ +package java.util; + +public interface List extends java.util.Collection +{ + + public int size(); + public boolean isEmpty(); + public boolean contains(java.lang.Object arg0); + public java.util.Iterator iterator(); + public java.lang.Object[] toArray(); + public java.lang.Object[] toArray(java.lang.Object[] arg0); + public boolean add(java.lang.Object arg0); + public boolean remove(java.lang.Object arg0); + public boolean containsAll(java.util.Collection arg0); + public boolean addAll(java.util.Collection arg0); + public boolean addAll(int arg0, java.util.Collection arg1); + public boolean removeAll(java.util.Collection arg0); + public boolean retainAll(java.util.Collection arg0); + public void clear(); + public boolean equals(java.lang.Object arg0); + public int hashCode(); + public java.lang.Object get(int arg0); + public java.lang.Object set(int arg0, java.lang.Object arg1); + public void add(int arg0, java.lang.Object arg1); + public java.lang.Object remove(int arg0); + public int indexOf(java.lang.Object arg0); + public int lastIndexOf(java.lang.Object arg0); + public java.util.ListIterator listIterator(); + public java.util.ListIterator listIterator(int arg0); + public java.util.List subList(int arg0, int arg1); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/ListIterator.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/ListIterator.java new file mode 100644 index 00000000000..7ddf49d4f51 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/ListIterator.java @@ -0,0 +1,18 @@ +/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker) + * Date: Fri Mar 28 13:47:08 CET 2008 + */ +package java.util; + +public interface ListIterator extends java.util.Iterator +{ + + public boolean hasNext(); + public java.lang.Object next(); + public boolean hasPrevious(); + public java.lang.Object previous(); + public int nextIndex(); + public int previousIndex(); + public void remove(); + public void set(java.lang.Object arg0); + public void add(java.lang.Object arg0); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Map.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Map.java new file mode 100644 index 00000000000..bbabc38cc04 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Map.java @@ -0,0 +1,23 @@ +/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker) + * Date: Fri Mar 28 13:47:08 CET 2008 + */ +package java.util; + +public interface Map +{ + + public int size(); + public boolean isEmpty(); + public boolean containsKey(java.lang.Object arg0); + public boolean containsValue(java.lang.Object arg0); + public java.lang.Object get(java.lang.Object arg0); + public java.lang.Object put(java.lang.Object arg0, java.lang.Object arg1); + public java.lang.Object remove(java.lang.Object arg0); + public void putAll(java.util.Map arg0); + public void clear(); + public java.util.Set keySet(); + public java.util.Collection values(); + public java.util.Set entrySet(); + public boolean equals(java.lang.Object arg0); + public int hashCode(); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Set.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Set.java new file mode 100644 index 00000000000..c09b759367c --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/a/util/Set.java @@ -0,0 +1,38 @@ +/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker) + * Date: Fri Mar 28 13:47:08 CET 2008 + */ +package java.util; + +public interface Set extends java.util.Collection +{ + + public int size(); + + public boolean isEmpty(); + + public boolean contains(java.lang.Object arg0); + + public java.util.Iterator iterator(); + + public java.lang.Object[] toArray(); + + public java.lang.Object[] toArray(java.lang.Object[] arg0); + + public boolean add(java.lang.Object arg0); + + public boolean remove(java.lang.Object arg0); + + public boolean containsAll(java.util.Collection arg0); + + public boolean addAll(java.util.Collection arg0); + + public boolean retainAll(java.util.Collection arg0); + + public boolean removeAll(java.util.Collection arg0); + + public void clear(); + + public boolean equals(java.lang.Object arg0); + + public int hashCode(); +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/Compressed.zip b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/Compressed.zip new file mode 100644 index 00000000000..0c2d4fa578b Binary files /dev/null and b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/Compressed.zip differ diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/Compressed/C2.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/Compressed/C2.java new file mode 100644 index 00000000000..80114c77a98 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/Compressed/C2.java @@ -0,0 +1,2 @@ +public class C2 { +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/Compressed/subdir/C1.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/Compressed/subdir/C1.java new file mode 100644 index 00000000000..934e84e637f --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/Compressed/subdir/C1.java @@ -0,0 +1,2 @@ +public class C1 { +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/cp1/B.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/cp1/B.java new file mode 100644 index 00000000000..b5952d8b66a --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/cp1/B.java @@ -0,0 +1,3 @@ +public class B { + +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/cp1/subdir/A.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/cp1/subdir/A.java new file mode 100644 index 00000000000..f7e8cc3b903 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/cp1/subdir/A.java @@ -0,0 +1,2 @@ +public class A { +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/cp2/D.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/cp2/D.java new file mode 100644 index 00000000000..a50cc332bc6 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/b/cp2/D.java @@ -0,0 +1,10 @@ +public class D { + /*@ normal_behavior + @ requires true; + @ ensures \result == 5; + @ assignable \strictly_nothing; + @*/ + public int constant() { + return 5; + } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/src/Client.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/src/Client.java new file mode 100644 index 00000000000..e2ecc8319b7 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/src/Client.java @@ -0,0 +1,2 @@ +public class Client { +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/src/Test.java b/keyext.proofmanagement/proofBundle/complexBundleGeneration/src/Test.java new file mode 100644 index 00000000000..06a5b3f0778 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/src/Test.java @@ -0,0 +1,37 @@ +import java.util.List; +import java.io.InputStream; + +public class Test { + // check that all of these classes are correctly loaded: + // bootclasspath + Object o; + String str; + List l; + InputStream is; + + // classpath + A a; // *.class + B b; // *.java + C1 c1; // loading from a zip + C2 c2; // loading from a zip + D d; // *.java + + // javaSource + Client cl; + + /*@ normal_behavior + @ requires true; + @ ensures true; + @*/ + public void trivial() { + } + + /*@ normal_behavior + @ requires d != null; + @ requires \invariant_for(d); + @ ensures \result == 5; + @*/ + public int constant() { + return d.constant(); + } +} diff --git a/keyext.proofmanagement/proofBundle/complexBundleGeneration/test.key b/keyext.proofmanagement/proofBundle/complexBundleGeneration/test.key new file mode 100644 index 00000000000..d9f84c2f55e --- /dev/null +++ b/keyext.proofmanagement/proofBundle/complexBundleGeneration/test.key @@ -0,0 +1,43 @@ +\settings { +"#Proof-Settings-Config-File +#Wed Jul 17 16:49:03 UTC 2019 +[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[Choice]DefaultChoices=assertions-assertions\:safe , initialisation-initialisation\:disableStaticInitialisation , +intRules-intRules\:arithmeticSemanticsIgnoringOF , programRules-programRules\:Java , +runtimeExceptions-runtimeExceptions\:ban , JavaCard-JavaCard\:off , Strings-Strings\:on , +modelFields-modelFields\:treatAsAxiom , bigint-bigint\:on , sequences-sequences\:on , moreSeqRules-moreSeqRules\:off , +reach-reach\:on , integerSimplificationRules-integerSimplificationRules\:full , permissions-permissions\:off , +wdOperator-wdOperator\:L , wdChecks-wdChecks\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\:off +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT +[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE +[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON +[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF +[Strategy]MaximumNumberOfAutomaticApplications=10000 +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE +[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE +[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF +[Strategy]Timeout=-1 +[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF +[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +[StrategyProperty]VBT_PHASE=VBT_SYM_EX +" +} + +\bootclasspath "a/"; +\classpath "b/cp1"; +\classpath "b/cp2/"; +\classpath "b/Compressed.zip"; +\javaSource "src"; + +\chooseContract "Test[Test::constant()].JML normal_behavior operation contract.0"; diff --git a/keyext.proofmanagement/proofBundle/simpleBundleGeneration/src/Client.java b/keyext.proofmanagement/proofBundle/simpleBundleGeneration/src/Client.java new file mode 100644 index 00000000000..e2ecc8319b7 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/simpleBundleGeneration/src/Client.java @@ -0,0 +1,2 @@ +public class Client { +} diff --git a/keyext.proofmanagement/proofBundle/simpleBundleGeneration/src/Test.java b/keyext.proofmanagement/proofBundle/simpleBundleGeneration/src/Test.java new file mode 100644 index 00000000000..f6dcc3bc729 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/simpleBundleGeneration/src/Test.java @@ -0,0 +1,30 @@ +import java.util.List; +import java.io.InputStream; + +public class Test { + // check that all of these classes are correctly loaded: + // bootclasspath + Object o; + String str; + List l; + InputStream is; + + // classpath: empty + + // javaSource + Client cl; + + /*@ normal_behavior + @ requires true; + @ ensures true; + @*/ + public void trivial() { + } + + /*@ normal_behavior + @ ensures \result == 5; + @*/ + public int constant() { + return 5; + } +} diff --git a/keyext.proofmanagement/proofBundle/simpleBundleGeneration/test.key b/keyext.proofmanagement/proofBundle/simpleBundleGeneration/test.key new file mode 100644 index 00000000000..064ee9b7a32 --- /dev/null +++ b/keyext.proofmanagement/proofBundle/simpleBundleGeneration/test.key @@ -0,0 +1,38 @@ +\settings { +"#Proof-Settings-Config-File +#Wed Jul 17 16:49:03 UTC 2019 +[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[Choice]DefaultChoices=assertions-assertions\:safe , initialisation-initialisation\:disableStaticInitialisation , +intRules-intRules\:arithmeticSemanticsIgnoringOF , programRules-programRules\:Java , +runtimeExceptions-runtimeExceptions\:ban , JavaCard-JavaCard\:off , Strings-Strings\:on , +modelFields-modelFields\:treatAsAxiom , bigint-bigint\:on , sequences-sequences\:on , moreSeqRules-moreSeqRules\:off , +reach-reach\:on , integerSimplificationRules-integerSimplificationRules\:full , permissions-permissions\:off , +wdOperator-wdOperator\:L , wdChecks-wdChecks\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\:off +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT +[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE +[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON +[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF +[Strategy]MaximumNumberOfAutomaticApplications=10000 +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE +[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE +[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF +[Strategy]Timeout=-1 +[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF +[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +[StrategyProperty]VBT_PHASE=VBT_SYM_EX +" +} + +\javaSource "src"; +\chooseContract "Test[Test::constant()].JML normal_behavior operation contract.0"; diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/CheckConfigDialog.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/CheckConfigDialog.java index 4a96d0f0841..4e4916edbe7 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/CheckConfigDialog.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/CheckConfigDialog.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.gui.KeYFileChooser; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -38,7 +39,7 @@ class CheckConfigDialog extends JDialog { private final Component glassPane = new BlockingGlassPane(); - private transient SwingWorker checkWorker; + private transient @Nullable SwingWorker checkWorker; private class ProofManagementCheckWorker extends SwingWorker { @Override @@ -106,7 +107,9 @@ public void mouseClicked(MouseEvent e) { containerPoint.x, containerPoint.y); if (component == runButton) { - checkWorker.cancel(true); + if (checkWorker != null) { + checkWorker.cancel(true); + } } else { e.consume(); } @@ -167,7 +170,7 @@ public void keyTyped(KeyEvent e) { } } - public CheckConfigDialog(Frame parent, String title, boolean modal) { + public CheckConfigDialog(@Nullable Frame parent, String title, boolean modal) { super(parent, title, modal); setDefaultCloseOperation(DISPOSE_ON_CLOSE); @@ -205,17 +208,7 @@ public CheckConfigDialog(Frame parent, String title, boolean modal) { bundleBox.add(bundleFileField); bundleBox.add(Box.createHorizontalStrut(5)); runButton.setEnabled(false); - JButton chooseBundleButton = new JButton("Choose file..."); - chooseBundleButton.addActionListener(e -> { - KeYFileChooser fc = KeYFileChooser.getFileChooser("Choose file"); - fc.setFileFilter(KeYFileChooser.PROOF_BUNDLE_FILTER); - if (fc.showOpenDialog(CheckConfigDialog.this) == JFileChooser.APPROVE_OPTION) { - bundleFileField.setText(fc.getSelectedFile().toString()); - runButton.setEnabled(true); - } - }); - chooseBundleButton.setPreferredSize(buttonDim); - chooseBundleButton.setMinimumSize(buttonDim); + JButton chooseBundleButton = getChooseBundleButton(buttonDim); bundleBox.add(chooseBundleButton); centerBox.add(bundleBox); @@ -292,4 +285,19 @@ public CheckConfigDialog(Frame parent, String title, boolean modal) { pack(); setLocationRelativeTo(parent); } + + private JButton getChooseBundleButton(Dimension buttonDim) { + JButton chooseBundleButton = new JButton("Choose file..."); + chooseBundleButton.addActionListener(e -> { + KeYFileChooser fc = KeYFileChooser.getFileChooser("Choose file"); + fc.setFileFilter(KeYFileChooser.PROOF_BUNDLE_FILTER); + if (fc.showOpenDialog(CheckConfigDialog.this) == JFileChooser.APPROVE_OPTION) { + bundleFileField.setText(fc.getSelectedFile().toString()); + runButton.setEnabled(true); + } + }); + chooseBundleButton.setPreferredSize(buttonDim); + chooseBundleButton.setMinimumSize(buttonDim); + return chooseBundleButton; + } } diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/Main.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/Main.java index 6745745cbc2..007e70efa6f 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/Main.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/Main.java @@ -20,6 +20,8 @@ import org.key_project.proofmanagement.io.ProofBundleHandler; import org.key_project.proofmanagement.merge.ProofBundleMerger; +import org.jspecify.annotations.Nullable; + /** * This is the starting class for ProofManagement. *
@@ -49,6 +51,7 @@ * * @author Wolfram Pfeifer */ +@SuppressWarnings("CallToPrintStackTrace") public final class Main { /** resource bundle where the description strings for the CLI are stored */ private static final ResourceBundle STRINGS = ResourceBundle.getBundle("strings"); @@ -161,7 +164,7 @@ public static void main(String[] args) { * @param reportPath the output path for the HTML report (if selected) */ public static void check(boolean missing, boolean settings, boolean replay, boolean dependency, - Path bundlePath, Path reportPath) { + Path bundlePath, @Nullable Path reportPath) { // we accumulate results in this variable CheckerData globalResult = new CheckerData(LogLevel.DEBUG); @@ -229,7 +232,7 @@ private static void check(CommandLine commandLine) { reportPath = Paths.get(outFileName).toAbsolutePath(); } - String pathStr = arguments.get(0); + String pathStr = arguments.getFirst(); Path bundlePath = Paths.get(pathStr); check(commandLine.isSet("--missing"), commandLine.isSet("--settings"), commandLine.isSet("--replay"), commandLine.isSet("--dependency"), @@ -254,7 +257,7 @@ private static void merge() { for (int i = 0; i < arguments.size() - 1; i++) { inputs.add(Paths.get(arguments.get(i))); } - Path output = Paths.get(arguments.get(arguments.size() - 1)); + Path output = Paths.get(arguments.getLast()); // Usually, the merging process is cancelled if there are conflicting files in both bundles. // This option forces merging. For the conflicting files, their versions from the first diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/ProofManagementExt.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/ProofManagementExt.java index 6b856b8bac8..d449f44c343 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/ProofManagementExt.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/ProofManagementExt.java @@ -12,7 +12,6 @@ import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.help.HelpInfo; -import org.jspecify.annotations.NonNull; /** * @author Wolfram Pfeifer @@ -29,7 +28,7 @@ public class ProofManagementExt implements private static final String MENU_PM = "Proof Management"; @Override - public @NonNull List getMainMenuActions(@NonNull MainWindow mainWindow) { + public List getMainMenuActions(MainWindow mainWindow) { return List.of(new CheckAction()); } diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/CheckerData.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/CheckerData.java index 40906628347..88bb0cf02c2 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/CheckerData.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/CheckerData.java @@ -7,14 +7,7 @@ import java.nio.file.Path; import java.time.LocalDateTime; import java.time.format.DateTimeFormatter; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; -import java.util.SortedSet; -import java.util.TreeSet; +import java.util.*; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.KeYUserProblemFile; @@ -30,6 +23,8 @@ import org.key_project.proofmanagement.io.Logger; import org.key_project.proofmanagement.io.ProofBundleHandler; +import org.jspecify.annotations.Nullable; + /** * This container serves for accumulating data given to checkers and results returned by them. * @@ -50,28 +45,34 @@ public String getCheckDate() { private final Map checks = new HashMap<>(); - /** minimum log level: all messages with a smaller LogLevel will be suppressed */ + /** + * minimum log level: all messages with a smaller LogLevel will be suppressed + */ private final LogLevel minLogLevel; - private final List messages = new ArrayList<>(); + private final List messages = new ArrayList<>(); // TODO: side effects: may be changed by checkers (e.g. remove paths of taclet proofs) - private List proofPaths; + private @Nullable List proofPaths = null; - ////////////////////////////////// results from dependency checker + /// /////////////////////////////// results from dependency checker - private DependencyGraph dependencyGraph; + private @Nullable DependencyGraph dependencyGraph; - ////////////////////////////////// results from missing proofs checker + /// /////////////////////////////// results from missing proofs checker public Set getContractsWithoutProof() { return contractsWithoutProof; } - /** user provided contracts for which no proof exists */ + /** + * user provided contracts for which no proof exists + */ private final Set contractsWithoutProof = new HashSet<>(); - /** internal contracts (from classes shipped with KeY) without a proof */ + /** + * internal contracts (from classes shipped with KeY) without a proof + */ private final Set internalContractsWithoutProof = new HashSet<>(); public void addContractWithoutProof(Contract c, boolean internal) { @@ -89,17 +90,23 @@ public void addContractWithoutProof(Contract c, boolean internal) { ////////////////////////////////// results from settings checker - /** all choice names that occur in at least one settings object of a proof */ + /** + * all choice names that occur in at least one settings object of a proof + */ private final SortedSet choiceNames = new TreeSet<>(); public SortedSet getChoiceNames() { return choiceNames; } - /** choices used as reference (mapped to their corresponding id) */ + /** + * choices used as reference (mapped to their corresponding id) + */ private final Map, Integer> referenceChoices = new HashMap<>(); - /** mapping from choices to the reference id */ + /** + * mapping from choices to the reference id + */ private final Map, Integer> choices2Id = new HashMap<>(); /** @@ -159,7 +166,7 @@ public Map, Integer> getShortChoices2Id() { return res; } - ////////////////////////////////// + /// /////////////////////////////// private LoadingState srcLoadingState = LoadingState.UNKNOWN; // we use methods to determine these states on the fly @@ -169,16 +176,16 @@ public Map, Integer> getShortChoices2Id() { private SettingsState settingsState = SettingsState.UNKNOWN; private GlobalState globalState = GlobalState.UNKNOWN; - private ProofBundleHandler pbh; - private PathNode fileTree; + private @Nullable ProofBundleHandler pbh; + private @Nullable PathNode fileTree; private final List proofEntries = new ArrayList<>(); - private SLEnvInput slenv; + private @Nullable SLEnvInput slenv; - public SLEnvInput getSlenv() { + public @Nullable SLEnvInput getSlenv() { return slenv; } - public void setSlenv(SLEnvInput slenv) { + public void setSlenv(@Nullable SLEnvInput slenv) { this.slenv = slenv; } @@ -197,9 +204,9 @@ public enum SettingsState { } public enum ReplayState { - ERROR("\u2718"), // cross/xmark + ERROR("✘"), // cross/xmark UNKNOWN("?"), - SUCCESS("\u2714"); // checkmark + SUCCESS("✔"); // checkmark private final String shortStr; @@ -214,9 +221,9 @@ public String toString() { } public enum LoadingState { - ERROR("\u2718"), // cross/xmark + ERROR("✘"), // cross/xmark UNKNOWN("?"), - SUCCESS("\u2714"); // checkmark + SUCCESS("✔"); // checkmark private final String shortStr; @@ -234,7 +241,7 @@ public enum DependencyState { UNKNOWN("?"), ILLEGAL_CYCLE("cycle"), UNPROVEN_DEP("open dep."), - OK("\u2714"); // checkmark + OK("✔"); // checkmark private final String shortStr; @@ -265,35 +272,9 @@ public String toString() { } } - public class ProofEntry { - public LoadingState loadingState = LoadingState.UNKNOWN; - public ReplayState replayState = ReplayState.UNKNOWN; - public DependencyState dependencyState = DependencyState.UNKNOWN; - public ProofState proofState = ProofState.UNKNOWN; - - public boolean replaySuccess() { - return replayState == ReplayState.SUCCESS; - } - - public Path proofFile; - public KeYUserProblemFile envInput; - public ProblemInitializer problemInitializer; - public Proof proof; - - public Contract contract; - public URL sourceFile; - public String shortSrc; - public IntermediatePresentationProofFileParser.Result parseResult; - public AbstractProblemLoader.ReplayResult replayResult; - - public Integer settingsId() { - return choices2Id.get(proof.getSettings().getChoiceSettings().getDefaultChoices()); - } - } - - public ProofEntry getProofEntryByContract(Contract contract) { + public @Nullable ProofEntry getProofEntryByContract(Contract contract) { for (ProofEntry p : proofEntries) { - if (p.contract.equals(contract)) { + if (Objects.equals(p.contract, contract)) { return p; } } @@ -326,17 +307,18 @@ public void print(LogLevel level, String message) { // for multiline strings, every line should have correct prefix String[] lines = message.split("\\r?\\n"); for (String l : lines) { - messages.add(level + l); - System.out.println(level + l); + var ll = new Logline(level, l); + messages.add(ll); + System.out.println(ll); } } } - public List getMessages() { + public List getMessages() { return messages; } - public PathNode getFileTree() { + public @Nullable PathNode getFileTree() { return fileTree; } @@ -348,7 +330,7 @@ public DependencyGraph getDependencyGraph() { return dependencyGraph; } - public ProofBundleHandler getPbh() { + public @Nullable ProofBundleHandler getPbh() { return pbh; } @@ -497,8 +479,8 @@ public void setPbh(ProofBundleHandler pbh) { this.pbh = pbh; } - public List getProofPaths() throws ProofManagementException { - if (proofPaths == null) { + public @Nullable List getProofPaths() throws ProofManagementException { + if (proofPaths == null && pbh != null) { proofPaths = pbh.getProofFiles(); } return proofPaths; @@ -511,4 +493,31 @@ public void setFileTree(PathNode fileTree) { public void setDependencyGraph(DependencyGraph dependencyGraph) { this.dependencyGraph = dependencyGraph; } + + public class ProofEntry { + public LoadingState loadingState = LoadingState.UNKNOWN; + public ReplayState replayState = ReplayState.UNKNOWN; + public DependencyState dependencyState = DependencyState.UNKNOWN; + public ProofState proofState = ProofState.UNKNOWN; + + public boolean replaySuccess() { + return replayState == ReplayState.SUCCESS; + } + + public @Nullable Path proofFile; + public @Nullable KeYUserProblemFile envInput; + public @Nullable ProblemInitializer problemInitializer; + public @Nullable Proof proof; + + public @Nullable Contract contract; + public @Nullable URL sourceFile; + public @Nullable String shortSrc; + public IntermediatePresentationProofFileParser.@Nullable Result parseResult; + public AbstractProblemLoader.@Nullable ReplayResult replayResult; + + public Integer settingsId() { + return choices2Id.get(proof.getSettings().getChoiceSettings().getDefaultChoices()); + } + } + } diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/DependencyChecker.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/DependencyChecker.java index 2970eb97ef0..b1a26b9b6eb 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/DependencyChecker.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/DependencyChecker.java @@ -11,6 +11,8 @@ import org.key_project.proofmanagement.io.LogLevel; import org.key_project.proofmanagement.io.ProofBundleHandler; +import org.jspecify.annotations.Nullable; + import static org.key_project.proofmanagement.check.dependency.DependencyGraph.EdgeType.TERMINATION_SENSITIVE; /** @@ -55,7 +57,7 @@ public class DependencyChecker implements Checker { * data container used to store checker result and share intermediate data * (for example proof AST, dependency graph, ...) */ - private CheckerData data; + private @Nullable CheckerData data; @Override public void check(ProofBundleHandler pbh, CheckerData checkerData) diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java index 6ccf66aed57..895597c1c47 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java @@ -33,6 +33,7 @@ import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.util.ProgressMonitor; +import org.key_project.proofmanagement.check.CheckerData.ProofEntry; import org.key_project.proofmanagement.check.dependency.DependencyGraph; import org.key_project.proofmanagement.check.dependency.DependencyGraphBuilder; import org.key_project.proofmanagement.io.LogLevel; @@ -100,8 +101,8 @@ public static void ensureProofsLoaded(CheckerData data) throws ProofManagementEx } } - private static CheckerData.ProofEntry ensureProofEntryExists(Path proofPath, CheckerData data) { - CheckerData.ProofEntry line = findProofLine(proofPath, data); + private static ProofEntry ensureProofEntryExists(Path proofPath, CheckerData data) { + ProofEntry line = findProofLine(proofPath, data); if (line == null) { line = data.new ProofEntry(); data.getProofEntries().add(line); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/Logline.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/Logline.java new file mode 100644 index 00000000000..d25998f89e6 --- /dev/null +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/Logline.java @@ -0,0 +1,19 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.proofmanagement.check; + +import org.key_project.proofmanagement.io.LogLevel; + +/** + * A record representing a line in the output log. + * + * @param level the {@link LogLevel} of the line + * @param message the content + */ +public record Logline(LogLevel level, String message) { + @Override + public String toString() { + return level + message; + } +} diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/MissingProofsChecker.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/MissingProofsChecker.java index 903ca9247dd..2fb87bc1f79 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/MissingProofsChecker.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/MissingProofsChecker.java @@ -73,7 +73,7 @@ private static void removeContractsWithProof(Set contracts, CheckerDat // compare: Is there a proof for every contract? for (CheckerData.ProofEntry entry : data.getProofEntries()) { - Proof p = entry.proof; + Proof p = Objects.requireNonNull(entry.proof); SpecificationRepository sr = p.getServices().getSpecificationRepository(); ContractPO cpo = sr.getPOForProof(p); Contract foundContract = cpo.getContract(); @@ -104,7 +104,8 @@ private static void reportContractsWithoutProof(Set contracts, Checker if (type instanceof TypeDeclaration td) { PositionInfo positionInfo = td.getPositionInfo(); URI uri = positionInfo.getURI().orElseThrow().normalize(); - URI srcURI = data.getPbh().getPath("src").toAbsolutePath().normalize().toUri(); + URI srcURI = Objects.requireNonNull(data.getPbh()) + .getPath("src").toAbsolutePath().normalize().toUri(); // ignore contracts from files not in src path (e.g. from bootclasspath) diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/Node.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/Node.java index 53b2525d6c9..188df040a97 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/Node.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/Node.java @@ -6,6 +6,8 @@ import java.util.SortedSet; import java.util.TreeSet; +import org.jspecify.annotations.Nullable; + /** * Represents a vertex/node of a tree. * @@ -14,7 +16,7 @@ */ public class Node> implements Comparable> { /** the parent node */ - private final Node parent; + private final @Nullable Node parent; /** the children nodes */ private final SortedSet> children = new TreeSet<>(); @@ -28,7 +30,7 @@ public class Node> implements Comparable> { * @param parent the parent node * @param element the content to store inside this node */ - public Node(Node parent, T element) { + public Node(@Nullable Node parent, T element) { this.parent = parent; this.content = element; } @@ -37,7 +39,7 @@ public T getContent() { return content; } - public Node getParent() { + public @Nullable Node getParent() { return parent; } diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/PathNode.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/PathNode.java index 847590fdba0..b93ea7d53a5 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/PathNode.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/PathNode.java @@ -6,6 +6,8 @@ import java.nio.file.Files; import java.nio.file.Path; +import org.jspecify.annotations.Nullable; + /** * Represents a node in a file tree where nodes contain Path objects. * @@ -19,12 +21,12 @@ public class PathNode extends Node { * @param parent the parent of the new node * @param element the Path to store at the new PathNode */ - public PathNode(PathNode parent, Path element) { + public PathNode(@Nullable PathNode parent, Path element) { super(parent, element); } @Override - public PathNode getParent() { + public @Nullable PathNode getParent() { return (PathNode) super.getParent(); } diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/SettingsChecker.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/SettingsChecker.java index ee09c59a8fb..f0c465e9a80 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/SettingsChecker.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/SettingsChecker.java @@ -101,7 +101,7 @@ private static boolean choicesConsistent(List choiceSettings, boolean consistent = true; // store reference settings in data with id 0 - ChoiceSettings reference = choiceSettings.get(0); + ChoiceSettings reference = choiceSettings.getFirst(); Map refChoices = reference.getDefaultChoices(); data.addReferenceChoices(refChoices); data.print(LogLevel.DEBUG, "Reference settings (id 0) are: " + refChoices); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/ContractAppCollector.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/ContractAppCollector.java index 925c988ea14..09b1d5d094a 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/ContractAppCollector.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/ContractAppCollector.java @@ -54,13 +54,13 @@ public class ContractAppCollector extends NodeIntermediateWalker { * the proof we search for contract applications (needed to get the SpecificationRepository, * JavaInfo, ...) */ - private Proof proof; + private final Proof proof; /** the logger to print out messages */ - private Logger logger; + private final Logger logger; /** the contracts (by name) as found by this collector as well as the termination type */ - private Map result = new HashMap<>(); + private final Map result = new HashMap<>(); /** * Creates a new collector for the given proof, starting at given root node. @@ -154,7 +154,7 @@ private void extractContractFromContractTaclet(TacletAppIntermediate tacletApp) * only one model method with same name is allowed (no overloading) */ assert axiomList.size() == 1; - ClassAxiom axiom = axiomList.get(0); + ClassAxiom axiom = axiomList.getFirst(); // found axiom always is a contract axiom, target always a program (model) method! assert axiom instanceof ContractAxiom; @@ -171,7 +171,7 @@ private void extractContractFromContractTaclet(TacletAppIntermediate tacletApp) // TODO: this is not the case if multiple contracts are combined with also keyword, // however, in this case the contract axioms are completely broken anyway assert contractList.size() == 1; - Contract contract = contractList.get(0); + Contract contract = contractList.getFirst(); // model method contract application is always termination sensitive! result.putIfAbsent(contract.getName(), TERMINATION_SENSITIVE); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraph.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraph.java index 775f6d76c66..b4e3ff53023 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraph.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraph.java @@ -3,16 +3,13 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.proofmanagement.check.dependency; -import java.util.ArrayDeque; -import java.util.HashMap; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; +import java.util.*; import java.util.stream.Collectors; import org.key_project.proofmanagement.io.Logger; +import org.jspecify.annotations.Nullable; + /** * Represents a graph of dependencies between contracts/proofs, i.e. which proof depends on * which contracts to be proven. @@ -21,7 +18,7 @@ */ public class DependencyGraph { /** - * indicates the type of a contract application (if termination has to be considered or not) + * indicates the type of contract application (if termination has to be considered or not) */ public enum EdgeType { /** @@ -118,7 +115,7 @@ public String toString() { * null indicates that it is invalid an has to be (re-)computed by calling * {@link #recalculateSCCs()}. */ - private Set allSCCs = null; + private @Nullable Set allSCCs; /** maps each dependency node to the SCC it corresponds to */ private final Map node2SCC = new HashMap<>(); @@ -140,6 +137,10 @@ public Map getNode2SCC() { return node2SCC; } + public SCC getSCCofNode(DependencyNode node) { + return node2SCC.get(node); + } + public Set getNodes() { return nodes; } @@ -171,7 +172,7 @@ public Set getAllSCCs() { if (allSCCs == null) { recalculateSCCs(); } - return allSCCs; + return Objects.requireNonNull(allSCCs); } /** @@ -180,7 +181,7 @@ public Set getAllSCCs() { * @param contractName the contract name to search for (only exact matches will be found) * @return the DependencyNode for the given contractName or null, if none found */ - public DependencyNode getNodeByName(String contractName) { + public @Nullable DependencyNode getNodeByName(String contractName) { return name2Node.get(contractName); } @@ -235,6 +236,7 @@ private void calculateSCCForNode(DependencyNode node) { } if (node.getLowLink() == node.getIndex()) { // back to "root" of SCC? -> store SCC + assert allSCCs != null; SCC scc = new SCC(allSCCs.size()); DependencyNode w; do { diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java index 38931951162..618825cfdac 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java @@ -5,6 +5,7 @@ import java.util.List; import java.util.Map; +import java.util.Objects; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.proof.Proof; @@ -36,23 +37,24 @@ public static DependencyGraph buildGraph(List proofEntri // first create the nodes of the graph (one for each loaded proof) for (CheckerData.ProofEntry line : proofEntries) { - Proof proof = line.proof; + Proof proof = Objects.requireNonNull(line.proof); String contractName = proof.name().toString(); Services services = proof.getServices(); SpecificationRepository specRepo = services.getSpecificationRepository(); Contract contract = specRepo.getContractByName(contractName); // create fresh node for current contract - DependencyNode node = new DependencyNode(contract); + DependencyNode node = new DependencyNode(Objects.requireNonNull(contract)); graph.addNode(node); } // add dependencies between nodes for (CheckerData.ProofEntry line : proofEntries) { // get current node and root of proof - Proof proof = line.proof; - DependencyNode currentNode = graph.getNodeByName(proof.name().toString()); - BranchNodeIntermediate node = line.parseResult.parsedResult(); + Proof proof = Objects.requireNonNull(line.proof); + DependencyNode currentNode = + Objects.requireNonNull(graph.getNodeByName(proof.name().toString())); + BranchNodeIntermediate node = Objects.requireNonNull(line.parseResult).parsedResult(); // collect all contracts the current proof refers to Services services = proof.getServices(); @@ -69,7 +71,7 @@ public static DependencyGraph buildGraph(List proofEntri // This is the case for contracts that have no proof in bundle, // particularly those from JavaRedux shipped with KeY. if (dependentNode == null) { - Contract contract = specRepo.getContractByName(depName); + Contract contract = Objects.requireNonNull(specRepo.getContractByName(depName)); dependentNode = new DependencyNode(contract); graph.addNode(dependentNode); } diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/NodeIntermediateWalker.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/NodeIntermediateWalker.java index 9afa8bbd5c9..aec945ba2f9 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/NodeIntermediateWalker.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/NodeIntermediateWalker.java @@ -13,7 +13,7 @@ */ public abstract class NodeIntermediateWalker { /** the root where the walker starts */ - private NodeIntermediate root; + private final NodeIntermediate root; /** * create a walker starting from the given root diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/package-info.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/package-info.java new file mode 100644 index 00000000000..4b9a5becdeb --- /dev/null +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (6/18/25) + */ +@NullMarked +package org.key_project.proofmanagement.check.dependency; + +import org.jspecify.annotations.NullMarked; diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/package-info.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/package-info.java new file mode 100644 index 00000000000..92550b229a3 --- /dev/null +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (6/18/25) + */ +@NullMarked +package org.key_project.proofmanagement.check; + +import org.jspecify.annotations.NullMarked; diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java index 171056afa64..893c2c6e5a1 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java @@ -4,20 +4,20 @@ package org.key_project.proofmanagement.io; import java.io.IOException; -import java.lang.reflect.Method; -import java.net.URL; +import java.io.InputStream; import java.nio.file.Files; import java.nio.file.Path; +import java.util.HashMap; import java.util.Map; import org.key_project.proofmanagement.check.CheckerData; import org.key_project.proofmanagement.check.PathNode; +import org.key_project.util.java.IOUtil; -import org.stringtemplate.v4.*; -import org.stringtemplate.v4.misc.MapModelAdaptor; -import org.stringtemplate.v4.misc.ObjectModelAdaptor; -import org.stringtemplate.v4.misc.STMessage; -import org.stringtemplate.v4.misc.STNoSuchPropertyException; +import freemarker.template.Configuration; +import freemarker.template.DefaultObjectWrapper; +import freemarker.template.Template; +import freemarker.template.TemplateException; /** * Provides a static method to print the check results in HTML format to a given path. @@ -25,7 +25,9 @@ * @author Wolfram Pfeifer */ public final class HTMLReport { - /** to prevent from instantiating */ + /** + * to prevent from instantiating + */ private HTMLReport() { } @@ -38,130 +40,55 @@ private HTMLReport() { * template resources */ public static void print(CheckerData data, Path target) throws IOException { + Configuration cfg = new Configuration(Configuration.VERSION_2_3_32); + cfg.setClassLoaderForTemplateLoading(HTMLReport.class.getClassLoader(), "/report/html"); + cfg.setDefaultEncoding("UTF-8"); + + // Use DefaultObjectWrapper to expose fields of objects in the data model + DefaultObjectWrapper wrapper = new DefaultObjectWrapper(Configuration.VERSION_2_3_32); + wrapper.setExposeFields(true); + cfg.setObjectWrapper(wrapper); + + // Load template + Template template = cfg.getTemplate("report.ftl"); - ST st = prepareStringTemplate(); + // Prepare data model + Map st = new HashMap<>(); - st.add("title", data.getPbh().getBundleName() + " - Proof Management Report"); + st.put("style", loadFromClasspath("/report/html/style.css")); + st.put("scripts", loadFromClasspath("/report/html/scripts.js")); + + + st.put("title", data.getPbh() != null ? data.getPbh().getBundleName() : ""); PathNode fileTree = data.getFileTree(); - st.add("checkerData", data); - st.add("bundleFileName", fileTree == null ? null : fileTree.getContent()); - st.add("treeRoot", fileTree); - st.add("entries", data.getProofEntries()); - st.add("graph", data.getDependencyGraph()); + st.put("checkerData", data); + st.put("bundleFileName", fileTree == null ? null : fileTree.getContent()); + st.put("treeRoot", fileTree); + st.put("entries", data.getProofEntries()); + st.put("graph", data.getDependencyGraph()); data.print("All checks completed!"); data.print("Generating html report ..."); - try { - String output = st.render(); - Files.writeString(target, output); + + + try (var out = Files.newBufferedWriter(target)) { + template.process(st, out); data.print("Report generated at " + target.normalize()); } catch (IOException e) { data.print("Unable to generate report: " + e.getMessage()); + } catch (TemplateException e) { + throw new RuntimeException(e); } } - /** - * Set up StringTemplate model adaptors and listeners. - * - * @return the ST object for rendering the HTML report - * @throws IOException if an error occurs accessing the StringTemplate resources - */ - @SuppressWarnings("rawtypes") - private static ST prepareStringTemplate() throws IOException { - ClassLoader classLoader = HTMLReport.class.getClassLoader(); - URL url = classLoader.getResource("report/html"); - - if (url == null) { - throw new IOException("Could not load report template resource from report/html."); + private static String loadFromClasspath(String name) throws IOException { + InputStream input = HTMLReport.class.getResourceAsStream(name); + if (input == null) { + return ""; } - - STGroup group = new STRawGroupDir(url, "UTF-8", '$', '$'); - - // provide access to getter methods with a name equal to the property (without "get") - // (needed to access some KeY properties, e.g. Proof.name() - group.registerModelAdaptor(Object.class, new ObjectModelAdaptor<>() { - @Override - public synchronized Object getProperty(Interpreter interp, ST self, Object o, - Object property, String propertyName) - throws STNoSuchPropertyException { - Method m = tryGetMethod(o.getClass(), propertyName); - if (m != null) { - try { - return m.invoke(o); - } catch (Exception e) { - throwNoSuchProperty(o.getClass(), propertyName, e); - } - } - return super.getProperty(interp, self, o, property, propertyName); - } - }); - - // provide access to entrySet property of Maps - Class> mapClass = (Class>) (Class) Map.class; - group.registerModelAdaptor(mapClass, new MapModelAdaptor() { - @Override - public Object getProperty(Interpreter interp, ST self, Map map, Object property, - String propertyName) - throws STNoSuchPropertyException { - if (property.equals("entrySet")) { - return map.entrySet(); - } - return super.getProperty(interp, self, map, property, propertyName); - } - }); - - /* - * This additional ModelAdaptor is workaround needed for access of Node.getValue in string - * template, otherwise we would have to add this to build.gradle files in key.ui and - * keyext.proofmanagement: - * jvmArgs += ['--add-opens', 'java.base/java.util=ALL-UNNAMED'] - */ - Class> mapEntryClass = (Class>) (Class) Map.Entry.class; - group.registerModelAdaptor(mapEntryClass, new ObjectModelAdaptor<>() { - @Override - public synchronized Object getProperty(Interpreter interp, ST self, - Map.Entry entry, Object property, - String propertyName) - throws STNoSuchPropertyException { - if (property.equals("value")) { - return entry.getValue(); - } else if (property.equals("key")) { - return entry.getKey(); - } - return super.getProperty(interp, self, entry, property, propertyName); - } - }); - - // StringRenderer to escape special HTML chars, for example in java.lang.Object:: - group.registerRenderer(String.class, new StringRenderer()); - // NumberRenderer to allow for format strings such as %02d - group.registerRenderer(Number.class, new NumberRenderer()); - - // register listeners to get error output on console - group.setListener(new STErrorListener() { - @Override - public void compileTimeError(STMessage msg) { - throw new RuntimeException(msg.toString(), msg.cause); - } - - @Override - public void runTimeError(STMessage msg) { - throw new RuntimeException(msg.toString(), msg.cause); - } - - @Override - public void IOError(STMessage msg) { - throw new RuntimeException(msg.toString(), msg.cause); - } - - @Override - public void internalError(STMessage msg) { - throw new RuntimeException(msg.toString(), msg.cause); - } - }); - - return group.getInstanceOf("report"); + return IOUtil.readFrom(input); } + } diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ProofBundleHandler.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ProofBundleHandler.java index 29fbab0450c..cb70e7e9c60 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ProofBundleHandler.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ProofBundleHandler.java @@ -17,6 +17,8 @@ import org.key_project.proofmanagement.check.PathNode; import org.key_project.proofmanagement.check.ProofManagementException; +import org.jspecify.annotations.Nullable; + /** * Provides methods to collect paths of files inside a proof bundle. * @@ -115,7 +117,7 @@ public abstract class ProofBundleHandler implements Closeable { * @return the bootclasspath or null, if none is specified * @throws IOException if the bundle can not be opened/accessed */ - public abstract Path getBootclasspath() throws IOException; + public abstract @Nullable Path getBootclasspath() throws IOException; /** * Returns a tree of the complete file hierarchy inside the bundle. diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/package-info.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/package-info.java new file mode 100644 index 00000000000..9af3e688627 --- /dev/null +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (6/18/25) + */ +@NullMarked +package org.key_project.proofmanagement.io; + +import org.jspecify.annotations.NullMarked; diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/FilesChecker.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/FilesChecker.java index 9cd4c19eb70..f4f9220c7ce 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/FilesChecker.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/FilesChecker.java @@ -21,6 +21,7 @@ * * @author Wolfram Pfeifer */ +@SuppressWarnings("CallToPrintStackTrace") public class FilesChecker { @FunctionalInterface public interface CheckedFunction { @@ -29,7 +30,7 @@ public interface CheckedFunction { static boolean listOfPathsConsistent(@NonNull List paths) { boolean res = true; - Path reference = paths.get(0); + Path reference = paths.getFirst(); for (int i = 1; i < paths.size(); i++) { Path p = paths.get(i); res &= sourcesConsistent(p, reference); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/ProofBundleMerger.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/ProofBundleMerger.java index caa02417fdb..301676a2335 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/ProofBundleMerger.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/ProofBundleMerger.java @@ -23,6 +23,8 @@ private ProofBundleMerger() { * * @param inputs the paths to the input bundles to merge * @param output the target path (will be zipped) + * @param force may the force be with you + * @param logger a logger instance to which message are reported * @throws ProofManagementException if any of the files can not be accessed */ public static void merge(List inputs, Path output, boolean force, Logger logger) diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/package-info.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/package-info.java new file mode 100644 index 00000000000..5bae37e00d5 --- /dev/null +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/merge/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (6/18/25) + */ +@NullMarked +package org.key_project.proofmanagement.merge; + +import org.jspecify.annotations.NullMarked; diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/package-info.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/package-info.java new file mode 100644 index 00000000000..8e536cd4033 --- /dev/null +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (6/18/25) + */ +@NullMarked +package org.key_project.proofmanagement; + +import org.jspecify.annotations.NullMarked; diff --git a/keyext.proofmanagement/src/main/resources/report/html/dependency/dep.st b/keyext.proofmanagement/src/main/resources/report/html/dependency/dep.st deleted file mode 100644 index 535b36e7ca0..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/dependency/dep.st +++ /dev/null @@ -1,11 +0,0 @@ - - $node.contract.name; format="xml-encode"$ - $\\$ - #$graph.node2SCC.(node).id; format="%02d"$$\\$ - $if(graph.node2SCC.(node).legal)$ (legal)$\\$ - $else$ (illegal)$\\$ - $endif$$\\$ - - ⟶ - $node.dependencies.keys:{d | $d.contract.name; format="xml-encode"$
}$ - \ No newline at end of file diff --git a/keyext.proofmanagement/src/main/resources/report/html/dependency/dependencies.st b/keyext.proofmanagement/src/main/resources/report/html/dependency/dependencies.st deleted file mode 100644 index 68a10e4b8bf..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/dependency/dependencies.st +++ /dev/null @@ -1,18 +0,0 @@ - - - - - - - - - - - $graph.nodes:{node | $dep(graph=graph, node=node)$}$ - -
ProofSCCDependencies
- - - diff --git a/keyext.proofmanagement/src/main/resources/report/html/lines/contract.st b/keyext.proofmanagement/src/main/resources/report/html/lines/contract.st deleted file mode 100644 index 335e6cd7075..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/lines/contract.st +++ /dev/null @@ -1,3 +0,0 @@ -class: $contract.KJT.javaType.name$
-target: $contract.target.name.toString; format="xml-encode"$
-type: $contract.displayName; format="xml-encode"$ diff --git a/keyext.proofmanagement/src/main/resources/report/html/lines/line.st b/keyext.proofmanagement/src/main/resources/report/html/lines/line.st deleted file mode 100644 index c3595be61ca..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/lines/line.st +++ /dev/null @@ -1,28 +0,0 @@ - - - $contract(contract=entry.contract)$ - -
$entry.shortSrc$
-
$entry.proofFile.toFile.getName$
$! using toFile is a workaround (since Path is Iterable, otherwise there is a stack overflow) !$ - #$entry.settingsId; format="%02d"$ - $entry.loadingState$ - $entry.replayState$ - $entry.proofState$ - $entry.dependencyState$ - $if(cd.checks.replay)$ - $if(entry.replaySuccess)$ - - Nodes: $entry.proof.statistics.nodes$
$!--> replay is needed to build the data structures --> else NPE in Proof.getStatistics!$ - Interactive Steps: $entry.proof.statistics.interactiveSteps$
- Automode Time: $entry.proof.statistics.autoModeTimeInMillis$ ms - - $else$ - Replay of proof failed! - $endif$ - $else$ - - Replay of proof is needed to display meaningful information here.
- Enable via --replay switch. - - $endif$ - diff --git a/keyext.proofmanagement/src/main/resources/report/html/lines/lines.st b/keyext.proofmanagement/src/main/resources/report/html/lines/lines.st deleted file mode 100644 index 5e18f404512..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/lines/lines.st +++ /dev/null @@ -1,24 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - $entries:{e | $line(entry=e, cd=cd)$}$ - -
ContractSource FileProof
FileSettings IDStatusStatistics
loadedreplayedstatedependencies
diff --git a/keyext.proofmanagement/src/main/resources/report/html/lines/prooflessContracts.st b/keyext.proofmanagement/src/main/resources/report/html/lines/prooflessContracts.st deleted file mode 100644 index 2042c2a811a..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/lines/prooflessContracts.st +++ /dev/null @@ -1,12 +0,0 @@ - - - - - - - - $cd.contractsWithoutProof:{c | - - }$ - -
Contract
$contract(contract=c)$
\ No newline at end of file diff --git a/keyext.proofmanagement/src/main/resources/report/html/overview/globalprogress.st b/keyext.proofmanagement/src/main/resources/report/html/overview/globalprogress.st deleted file mode 100644 index 75ace167341..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/overview/globalprogress.st +++ /dev/null @@ -1,22 +0,0 @@ -
- $if(cd.hasProvenContracts)$ -
proven
- $endif$ - $if(cd.hasLemmaLeftContracts)$ -
dependencies left
- $endif$ - $if(cd.hasUnprovenContracts)$ -
unproven
- $endif$ -
-
- $if(cd.hasProvenContracts)$ -
$proven$
- $endif$ - $if(cd.hasLemmaLeftContracts)$ -
$lemmaLeft$
- $endif$ - $if(cd.hasUnprovenContracts)$ -
$unproven$
- $endif$ -
\ No newline at end of file diff --git a/keyext.proofmanagement/src/main/resources/report/html/overview/overview.st b/keyext.proofmanagement/src/main/resources/report/html/overview/overview.st deleted file mode 100644 index d1262889575..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/overview/overview.st +++ /dev/null @@ -1,36 +0,0 @@ -
    -
  • Bundle: $cd.Pbh.bundleName$
    • -
  • Checks run: $cd.checks:{c | $c$}; separator=", "$
    • -
  • Date: $cd.checkDate$
    • -
  • Overall Status: $cd.globalState$
    • -
  • Contracts: - $globalprogress(data=cd, - total=cd.bundleProofCount, - proven=cd.provenCount, - lemmaLeft=cd.lemmaLeftCount, - unproven=cd.unprovenCount)$ -
    • -
  • Standard output: -
    -
    - - - - - - - - -
    -
    -
    -$cd.messages; separator={$\n$}, format="xml-encode"$ -
    -
    • -
diff --git a/keyext.proofmanagement/src/main/resources/report/html/report.ftl b/keyext.proofmanagement/src/main/resources/report/html/report.ftl new file mode 100644 index 00000000000..b7dbfe23f82 --- /dev/null +++ b/keyext.proofmanagement/src/main/resources/report/html/report.ftl @@ -0,0 +1,323 @@ +<#-- @ftlvariable name="checkerData" type="org.key_project.proofmanagement.check.CheckerData" --> +<#-- @ftlvariable name="style" type="String" --> +<#-- @ftlvariable name="scripts" type="String" --> +<#-- @ftlvariable name="title" type="String" --> +<#-- @ftlvariable name="bundleFileName" type="String" --> +<#-- @ftlvariable name="treeRoot" type="org.key_project.proofmanagement.check.PathNode" --> +<#-- @ftlvariable name="entries" type="java.util.List" --> +<#-- @ftlvariable name="graph" type="org.key_project.proofmanagement.check.dependency.DependencyGraph" --> + + + + + ${title} + + + + + +
+ Overview + Files + Contracts + Dependencies +
+ +
+ +
+ Bundle: ${checkerData.pbh.bundleName!"n/a"} +
+ + +
+ Checks run: + <#list checkerData.checks as key, c> + ${c}<#sep>, + +
+ +
Date of report: ${checkerData.checkDate}
+ +
Overall Status: ${checkerData.globalState}
+ +
+

Contracts Overview

+ <#assign total=checkerData.bundleProofCount() + proven=checkerData.provenCount() + lemmaLeft=checkerData.lemmaLeftCount() + unproven=checkerData.unprovenCount() + data=checkerData > + + <#assign provenPercent=proven/total*100 + depsLeftPercent=lemmaLeft/total*100 + unprovenPercent=unproven/total*100 > + + + + + + + + + + + + + + proven (${proven}) + + + + dependencies left (${lemmaLeft}) + + + + unproven (${unproven}) + + + + + + + + +
+ +
+

Log messages

+
+
+ + + + + + + + +
+
+
+ <#list checkerData.messages as msg> + <#escape x as x> +
+ ${msg} +
+ + +
+
+
+ +
+

Files found inside proof bundle:

+ + <#macro tree_folder f> + ${f} +
    + <#list f.children as c> + <@tree node=c /> + +
+ + + <#macro tree node> +
    +
  • + <#if node.children?has_content> + <@tree_folder node /> + <#else> + ${node} + +
    • +
+ + <@tree treeRoot /> +
+ +
+

Contracts with proof inside bundle:

+ + + + + + + + + + + + + + + + + + + + + + <#list entries as entry> + + + + + + + + + + + <#if checkerData.checks.replay??> + <#if entry.replaySuccess()> + + <#else> + + + <#else> + + + + + +
ContractSource FileProof
FileSettings IDStatusStatistics
loadedreplayedstatedependencies
+ class: ${entry.contract.KJT.javaType.name}
+ target: ${entry.contract.target.name()}
+ type: ${entry.contract.displayName} + 		+
${entry.shortSrc}
+ 		+
${entry.proofFile.toFile().name}
+ 		#${entry.settingsId()?string("00")}${entry.loadingState}${entry.replayState}${entry.proofState}${entry.dependencyState} + Nodes: ${entry.proof.statistics.nodes}
+ Interactive Steps: ${entry.proof.statistics.interactiveSteps}
+ Automode Time: ${entry.proof.statistics.autoModeTimeInMillis} ms + 		Replay of proof failed! + Replay of proof is needed to display meaningful information here.
+ Enable via --replay switch. +
+ +

Contracts declared inside bundle without proof:

+ + + + + + + + <#list checkerData.contractsWithoutProof as c> + + + + + +
Contract
+ class: ${c.KJT.javaType.name}
+ target: ${c.target.name()}
+ type: ${c.displayName} +
+

Settings comparison:

+ + + + + <#list checkerData.choiceNames as names> + + + + + + <#list checkerData.shortChoices2Id as choices , value> + + + <#list checkerData.choiceNames as name> + + + + + + +
ID${names}
${value}${choices[name]???string('yes','no')}
+
+ +
+

Dependencies between contracts:

+ <#if graph?? > + + + + + + + + + + + <#list graph.node2SCC as node, scc> + + + + + + + + +
ProofSCCDependencies
+ ${node.contract.name} + + #${scc.id?string("00")} + <#if scc.legal> + (legal) + <#else> + (illegal) + + ⟶ + <#list node.dependencies?keys as d> + ${d.contract.name}
+ +
+ + + + <#else> + Dependency check has not been enabled. Use --dependency flag to enable it. + +
+ + + + + + diff --git a/keyext.proofmanagement/src/main/resources/report/html/report.st b/keyext.proofmanagement/src/main/resources/report/html/report.st deleted file mode 100644 index 43d1dc7cb85..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/report.st +++ /dev/null @@ -1,60 +0,0 @@ - - - $title$ - - $scripts()$ - - - - -
- - - - -
- -
-$/overview/overview(cd=checkerData)$ -
- -
-

Files found inside proof bundle:

- $/tree/tree(node=treeRoot)$ -
- -
-

Contracts with proof inside bundle:

- $/lines/lines(cd=checkerData, entries=entries)$ -

Contracts declared inside bundle without proof:

- $/lines/prooflessContracts(cd=checkerData)$ -

Settings comparison:

- $/settings/settings(cd=checkerData)$ -
- -
-

Dependencies between contracts:

- $if(graph)$ - $/dependency/dependencies(graph=graph)$ - $else$ - Dependency check has not been enabled. Use --dependency flag to enable it. - $endif$ -
- - - - diff --git a/keyext.proofmanagement/src/main/resources/report/html/scripts.js b/keyext.proofmanagement/src/main/resources/report/html/scripts.js new file mode 100644 index 00000000000..5caa886c4e8 --- /dev/null +++ b/keyext.proofmanagement/src/main/resources/report/html/scripts.js @@ -0,0 +1,118 @@ +// id: name of table +// column: index of column for sortint (starting at index 0) +// headerSize: count of static headers at the top to skip +function sortTable(id, column, headerSize) { + var table, rows, switching, i, x, y, shouldSwitch, dir, switchcount = 0; + table = document.getElementById(id); + switching = true; + + // Set the sorting direction to ascending: + dir = "asc"; + + // Make a loop that will continue until no switching has been done + while (switching) { + //start by saying: no switching is done: + switching = false; + rows = table.rows; + + // Loop through all table rows (skip table headers) + for (i = headerSize; i < (rows.length - 1); i++) { + shouldSwitch = false; + + /*Get the two elements you want to compare, + one from current row and one from the next:*/ + x = rows[i].getElementsByTagName("TD")[column]; + y = rows[i + 1].getElementsByTagName("TD")[column]; + + /*check if the two rows should switch place, + based on the direction, asc or desc:*/ + if (dir == "asc") { + if (x.innerHTML.toLowerCase() > y.innerHTML.toLowerCase()) { + //if so, mark as a switch and break the loop: + shouldSwitch = true; + break; + } + } else if (dir == "desc") { + if (x.innerHTML.toLowerCase() < y.innerHTML.toLowerCase()) { + //if so, mark as a switch and break the loop: + shouldSwitch = true; + break; + } + } + } + if (shouldSwitch) { + /*If a switch has been marked, make the switch + and mark that a switch has been done:*/ + rows[i].parentNode.insertBefore(rows[i + 1], rows[i]); + switching = true; + //Each time a switch is done, increase this count by 1: + switchcount++; + } else { + /*If no switching has been done AND the direction is "asc", + set the direction to "desc" and run the while loop again.*/ + if (switchcount == 0 && dir == "asc") { + dir = "desc"; + switching = true; + } + } + } +} + +function openTab(evt, tabName) { + var i, tabcontent, tablinks; + + tabcontent = document.getElementsByClassName("tabcontent"); + for (i = 0; i < tabcontent.length; i++) { + tabcontent[i].style.display = "none"; + } + + tablinks = document.getElementsByClassName("tablinks"); + for (i = 0; i < tablinks.length; i++) { + tablinks[i].className = tablinks[i].className.replace(" active", ""); + } + + document.getElementById(tabName).style.display = "block"; + evt.currentTarget.className += " active"; +} + + +//region Toggle the visibility of log-lines using checkboxes +let chkError = document.getElementById("errors"); +let chkWarning = document.getElementById("warnings"); +let chkDebug = document.getElementById("debug"); +let chkInformation = document.getElementById("info"); + +const LOGLINE_CHECKBOXES = [chkError, chkWarning, chkInformation, chkDebug]; + +function updateLoglineVisibility() { + document.getElementById("messages"); + for (const chk of LOGLINE_CHECKBOXES) { + let value = chk.checked ? "block" : "none"; + + let className = "loglevel-" + chk.value; + let lines = document.getElementsByClassName(className); + for (let it of lines) { + it.style.display = value; + } + } +} +//endregion + +document.addEventListener("DOMContentLoaded", () => { + for (let it of LOGLINE_CHECKBOXES) { + it.addEventListener("change", updateLoglineVisibility); + } + updateLoglineVisibility(); +}); + + +// region make FileTree toggle by keyboard +document.addEventListener("DOMContentLoaded", () => { + for (let toggler of document.getElementsByClassName("caret")) { + toggler.addEventListener("click", () => { + this.parentElement.querySelector(".nested").classList.toggle("active"); + this.classList.toggle("caret-down"); + }); + } +}); +//endregion \ No newline at end of file diff --git a/keyext.proofmanagement/src/main/resources/report/html/scripts.st b/keyext.proofmanagement/src/main/resources/report/html/scripts.st deleted file mode 100644 index 9e6eef1943e..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/scripts.st +++ /dev/null @@ -1,99 +0,0 @@ - - - - - diff --git a/keyext.proofmanagement/src/main/resources/report/html/settings/choices.st b/keyext.proofmanagement/src/main/resources/report/html/settings/choices.st deleted file mode 100644 index 873da867e49..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/settings/choices.st +++ /dev/null @@ -1,5 +0,0 @@ - - #$entry.value; format="%02d"$ - $names:{name | $entry.key.(name)$ - }$ - \ No newline at end of file diff --git a/keyext.proofmanagement/src/main/resources/report/html/settings/settings.st b/keyext.proofmanagement/src/main/resources/report/html/settings/settings.st deleted file mode 100644 index 14713005818..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/settings/settings.st +++ /dev/null @@ -1,12 +0,0 @@ - - - - - $cd.choiceNames:{c | - }$ - - - - $cd.shortChoices2Id.entrySet:{entry | $choices(names=cd.choiceNames,entry=entry)$}$ - -
ID$c$
diff --git a/keyext.proofmanagement/src/main/resources/report/html/style.css b/keyext.proofmanagement/src/main/resources/report/html/style.css new file mode 100644 index 00000000000..8694e360495 --- /dev/null +++ b/keyext.proofmanagement/src/main/resources/report/html/style.css @@ -0,0 +1,162 @@ +body, html { + margin: 0; + font-family: "Arial", sans-serif; +} + +div.tabcontent { + overflow: hidden; + display: none; /* Hide all tabs */ +} + +div.tabcontent:target, /*show tabs if targeted */ +:root:not(:has(:target)) div.tabcontent.default /*if nothing targeted at all, show the default tab*/ +{ + display: block +} + +.nav { + background-color: #ccc; + padding: 1em; + margin-bottom: 2em; + border-bottom: 1px solid lightblue; + + a { + padding: 1ex; + font-size: 120%; + } + + a:hover { + background-color: #ddd; + } + + a.active { + background-color: #ccc + } +} + +.tabcontent { + padding: 6px 12px; +} + +ul, #fileTree { + list-style-type: none; +} + +#fileTree { + margin: 0; + padding: 0; +} + +.caret { + cursor: pointer; + user-select: none; +} + +.caret::before { + content: "\25B6"; + color: black; + display: inline-block; + margin-right: 6px; + transform: rotate(90deg); +} + +.caret-down::before { + transform: rotate(0deg); +} + +.nested { + display: none; +} + +.active { + display: block; +} + +table { + border-collapse: separate; + border-spacing: 1px 1px; +} + +th { + vertical-align: top; + text-align: left; +} + +th.clickable { + cursor: pointer; +} + +td { + text-align: left; + padding-left: 4px; + padding-right: 4px; +} + +tr.blue { + color: #284FA8; + background-color: #DAE7FE; +} + +td.SCCs { + text-align: left; + padding-left: 10px; + padding-right: 20px; + color: #284FA8; +} + +thead.tableHead { + text-align: center; + color: #FFFFFF; + background-color: #6688D4; + font-family: sans-serif; + font-size: 120%; + font-weight: bold; + white-space: nowrap; + padding-left: 4px; + padding-right: 4px; +} + + +#bundleTable { + font-weight: bold; + font-size: 110%; +} + + +.legend { + display: inline-block; + text-align: right; + width: 20%; +} + +.bar { + display: inline-block; + height: 1em; +} + +div#messages { + background-color: #002b36; + color: #93a1a1; + font-family: monospace; + font-size: 10pt; + padding: 10px; + .loglevel-4 /*error line*/ { + color: hsla(10 100% 50%); + } + + .loglevel-3 /*warning line*/ { + color: hsla(40 100% 50%); + } + + .loglevel-2 /*info*/ { + color: hsla(170 100% 50%); + } + + .loglevel-1 /*normal line*/ { + color:yellow; + } + + .loglevel-0t /*error line*/ { + color: #ccc; + } +} \ No newline at end of file diff --git a/keyext.proofmanagement/src/main/resources/report/html/style.st b/keyext.proofmanagement/src/main/resources/report/html/style.st deleted file mode 100644 index 5bd1c2cfd11..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/style.st +++ /dev/null @@ -1,116 +0,0 @@ -body, html { - margin: 0; - font-family: Arial; -} - -.tab { - overflow: hidden; - background-color: #f1f1f1; -} - -.tab button { - background-color: inherit; - float: left; - border: none; - outline: none; - cursor: pointer; - padding: 14px 16px; - transition: 0.3s; - font-size: 20px; -} - -.tab button:hover { - background-color: #ddd; -} - -.tab button.active { - background-color: #ccc -} - -.tabcontent { - display: none; - padding: 6px 12px; -} - -ul, #fileTree { - list-style-type: none; -} - -#fileTree { - margin: 0; - padding: 0; -} - -.caret { - cursor: pointer; - user-select: none; -} - -.caret::before { - content: "\25B6"; - color: black; - display: inline-block; - margin-right: 6px; - transform: rotate(90deg); -} - -.caret-down::before { - transform: rotate(0deg); -} - -.nested { - display: none; -} - -.active { - display: block; -} - -table { - border-collapse: separate; - border-spacing: 1px 1px; -} - -th { - vertical-align: top; - text-align: left; -} - -th.clickable { - cursor: pointer; -} - -td { - text-align: left; - padding-left: 4px; - padding-right: 4px; -} - -tr.blue { - color: #284FA8; - background-color: #DAE7FE; -} - -td.SCCs { - text-align: left; - padding-left: 10px; - padding-right: 20px; - color: #284FA8; -} - -thead.tableHead { - text-align: center; - color: #FFFFFF; - background-color: #6688D4; - font-family: sans-serif; - font-size: 120%; - font-weight: bold; - white-space: nowrap; - padding-left: 4px; - padding-right: 4px; -} - -#messages span { - display: block; - white-space: pre; -} diff --git a/keyext.proofmanagement/src/main/resources/report/html/tree/dir.st b/keyext.proofmanagement/src/main/resources/report/html/tree/dir.st deleted file mode 100644 index 031136cd4f9..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/tree/dir.st +++ /dev/null @@ -1,4 +0,0 @@ -$f$ -
    - $f.children:{c | $tree(node=c)$}$ -
\ No newline at end of file diff --git a/keyext.proofmanagement/src/main/resources/report/html/tree/tree.st b/keyext.proofmanagement/src/main/resources/report/html/tree/tree.st deleted file mode 100644 index 062062b3e86..00000000000 --- a/keyext.proofmanagement/src/main/resources/report/html/tree/tree.st +++ /dev/null @@ -1,9 +0,0 @@ -
    -
  • - $if(!node.children.empty)$ - $dir(f=node)$ - $else$ - $node$ - $endif$ -
    • -
\ No newline at end of file diff --git a/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleA(int)).JML operation contract.0.proof b/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleA(int)).JML operation contract.0.proof new file mode 100755 index 00000000000..a8e17a090a9 --- /dev/null +++ b/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleA(int)).JML operation contract.0.proof @@ -0,0 +1,626 @@ +\profile "Java Profile"; + +\settings { +"#Proof-Settings-Config-File +#Mon Mar 09 18:28:06 CET 2020 +[Labels]UseOriginLabels=true +[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON +[SMTSettings]invariantForall=false +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:off , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:off , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , methodExpansion-methodExpansion\\:modularOnly +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT +[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE +[SMTSettings]UseBuiltUniqueness=false +[SMTSettings]explicitTypeHierarchy=false +[SMTSettings]instantiateHierarchyAssumptions=true +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_COMPLETION +[SMTSettings]SelectedTaclets= +[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON +[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF +[Strategy]MaximumNumberOfAutomaticApplications=7000 +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED +[SMTSettings]useConstantsForBigOrSmallIntegers=true +[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE +[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF +[Strategy]Timeout=-1 +[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_ON +[SMTSettings]useUninterpretedMultiplication=true +[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[SMTSettings]maxGenericSorts=2 +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +[SMTSettings]integersMinimum=-2147483645 +[StrategyProperty]VBT_PHASE=VBT_SYM_EX +[SMTSettings]integersMaximum=2147483645 +" +} + +\javaSource "src"; + +\proofObligation "#Proof Obligation Settings +#Mon Mar 09 18:28:06 CET 2020 +contract=Example[Example\\:\\:cycleA(int)].JML operation contract.0 +name=Example[Example\\:\\:cycleA(int)].JML operation contract.0 +class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO +"; + +\proof { +(keyLog "0" (keyUser "Banach" ) (keyVersion "9e1d8db9a5")) + +(autoModeTime "358") + +(branch "dummy ID" + (builtin "One Step Simplification" (formula "1") (newnames "param,self_51,result_43,exc_51,heapAtPre_0,o,f")) +(rule "impRight" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "3")) +(rule "andLeft" (formula "1")) +(rule "notLeft" (formula "5")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "notLeft" (formula "2")) +(rule "assignment" (formula "8") (term "1")) + (builtin "One Step Simplification" (formula "8")) +(rule "methodBodyExpand" (formula "8") (term "1") (newnames "heapBefore_cycleA,savedHeapBefore_cycleA")) + (builtin "One Step Simplification" (formula "8")) +(rule "ifElseUnfold" (formula "8") (term "1") (inst "#boolv=x")) +(rule "variableDeclaration" (formula "8") (term "1") (newnames "x")) +(rule "compound_assignment_5_nonsimple" (formula "8") (term "1")) +(rule "ifElseUnfold" (formula "8") (term "1") (inst "#boolv=x_1")) +(rule "variableDeclaration" (formula "8") (term "1") (newnames "x_1")) +(rule "equality_comparison_simple" (formula "8") (term "1")) + (builtin "One Step Simplification" (formula "8")) +(rule "ifElseSplit" (formula "8")) +(branch "if x_1 true" + (builtin "One Step Simplification" (formula "9")) + (builtin "One Step Simplification" (formula "1")) + (rule "ifElseSkipElse" (formula "9") (term "1")) + (builtin "One Step Simplification" (formula "9")) + (rule "assignment" (formula "9") (term "1")) + (builtin "One Step Simplification" (formula "9")) + (rule "applyEq" (formula "5") (term "0") (ifseqformula "1")) + (rule "applyEq" (formula "8") (term "0") (ifseqformula "1")) + (rule "less_literals" (formula "8")) + (rule "false_right" (formula "8")) + (rule "returnUnfold" (formula "8") (term "1") (inst "#v0=x")) + (rule "variableDeclarationAssign" (formula "8") (term "1")) + (rule "variableDeclaration" (formula "8") (term "1") (newnames "x_2")) + (builtin "Use Operation Contract" (formula "8") (newnames "heapBefore_leaf,result_44,exc_52,heapAfter_leaf,anon_heap_leaf") (contract "Example[Example::leaf()].JML operation contract.0") (modality "diamond")) + (branch "Post (leaf)" + (builtin "One Step Simplification" (formula "10")) + (builtin "One Step Simplification" (formula "8")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "9")) + (rule "typeEqDerived" (formula "10") (term "0,1,1,1,1") (ifseqformula "9")) + (rule "typeEqDerived" (formula "10") (term "0,0,1,1,1") (ifseqformula "9")) + (builtin "One Step Simplification" (formula "10") (ifInst "" (formula "9")) (ifInst "" (formula "9"))) + (rule "andLeft" (formula "10")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "applyEq" (formula "13") (term "0,1,0") (ifseqformula "10")) + (rule "methodCallReturn" (formula "13") (term "1")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "methodCallEmpty" (formula "13") (term "1")) + (rule "tryEmpty" (formula "13") (term "1")) + (rule "emptyModality" (formula "13") (term "1")) + (rule "andRight" (formula "13")) + (branch "Case 1" + (rule "impRight" (formula "13")) + (rule "andRight" (formula "14")) + (branch "Case 1" + (rule "impRight" (formula "14")) + (builtin "One Step Simplification" (formula "2")) + (builtin "One Step Simplification" (formula "1")) + (builtin "One Step Simplification" (formula "15")) + (rule "closeTrue" (formula "15")) + ) + (branch "Case 2" + (builtin "One Step Simplification" (formula "14") (ifInst "" (formula "12"))) + (rule "closeTrue" (formula "14")) + ) + ) + (branch "Case 2" + (rule "impRight" (formula "13")) + (rule "andRight" (formula "14")) + (branch "Case 1" + (builtin "One Step Simplification" (formula "14") (ifInst "" (formula "12"))) + (rule "closeTrue" (formula "14")) + ) + (branch "Case 2" + (rule "orRight" (formula "14")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Exceptional Post (leaf)" + (builtin "One Step Simplification" (formula "8")) + (builtin "One Step Simplification" (formula "10")) + (rule "andLeft" (formula "8")) + (rule "selectCreatedOfAnonAsFormulaEQ" (formula "9") (term "1,0") (ifseqformula "8")) + (rule "andLeft" (formula "9")) + (rule "andLeft" (formula "9")) + (rule "andLeft" (formula "11")) + (rule "notLeft" (formula "9")) + (rule "replace_known_right" (formula "10") (term "0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "10")) + (rule "true_left" (formula "10")) + (rule "replace_known_right" (formula "10") (term "0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "10")) + (rule "andLeft" (formula "10")) + (rule "methodCallParamThrow" (formula "14") (term "1")) + (rule "tryCatchThrow" (formula "14") (term "1")) + (rule "ifElseUnfold" (formula "14") (term "1") (inst "#boolv=x")) + (rule "variableDeclaration" (formula "14") (term "1") (newnames "x_3")) + (rule "equality_comparison_simple" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "replace_known_right" (formula "14") (term "0,0,1,0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "14")) + (rule "ifElseSplit" (formula "14")) + (branch "if x_3 true" + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch "if x_3 false" + (builtin "One Step Simplification" (formula "1")) + (builtin "One Step Simplification" (formula "15")) + (rule "true_left" (formula "1")) + (rule "ifElseSplit" (formula "14")) + (branch "if exc_52 instanceof java.lang.Throwable true" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "13"))) + (rule "true_left" (formula "1")) + (rule "variableDeclaration" (formula "14") (term "1") (newnames "e")) + (rule "delete_unnecessary_cast" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "assignment" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "emptyModality" (formula "14") (term "1")) + (rule "andRight" (formula "14")) + (branch "Case 1" + (rule "impRight" (formula "14")) + (rule "andRight" (formula "15")) + (branch "Case 1" + (rule "impRight" (formula "15")) + (builtin "One Step Simplification" (formula "2") (ifInst "" (formula "14"))) + (rule "closeFalse" (formula "2")) + ) + (branch "Case 2" + (builtin "One Step Simplification" (formula "15") (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "15")) + ) + ) + (branch "Case 2" + (rule "impRight" (formula "14")) + (rule "andRight" (formula "15")) + (branch "Case 1" + (builtin "One Step Simplification" (formula "15") (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "15")) + ) + (branch "Case 2" + (rule "orRight" (formula "15")) + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "13"))) + (builtin "One Step Simplification" (formula "16")) + (rule "true_left" (formula "1")) + (rule "replace_known_right" (formula "11") (term "0") (ifseqformula "14")) + (builtin "One Step Simplification" (formula "11") (ifInst "" (formula "15"))) + (rule "closeFalse" (formula "11")) + ) + ) + ) + (branch "if exc_52 instanceof java.lang.Throwable false" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "13"))) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Pre (leaf)" + (builtin "One Step Simplification" (formula "8") (ifInst "" (formula "6")) (ifInst "" (formula "2"))) + (rule "closeTrue" (formula "8")) + ) +) +(branch "if x_1 false" + (builtin "One Step Simplification" (formula "9")) + (builtin "One Step Simplification" (formula "1")) + (rule "notLeft" (formula "1")) + (rule "equality_comparison_simple" (formula "9") (term "1")) + (builtin "One Step Simplification" (formula "9")) + (rule "blockEmpty" (formula "9") (term "1")) + (rule "ifElseSplit" (formula "9")) + (branch "if x true" + (builtin "One Step Simplification" (formula "10")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEq" (formula "7") (term "0") (ifseqformula "1")) + (rule "equal_literals" (formula "7")) + (rule "false_right" (formula "7")) + (rule "applyEq" (formula "5") (term "0") (ifseqformula "1")) + (rule "applyEq" (formula "8") (term "0") (ifseqformula "1")) + (rule "less_literals" (formula "8")) + (rule "false_right" (formula "8")) + (rule "returnUnfold" (formula "8") (term "1") (inst "#v0=x")) + (rule "variableDeclarationAssign" (formula "8") (term "1")) + (rule "variableDeclaration" (formula "8") (term "1") (newnames "x_2")) + (builtin "Use Operation Contract" (formula "8") (newnames "heapBefore_leaf,result_44,exc_52,heapAfter_leaf,anon_heap_leaf") (contract "Example[Example::leaf()].JML operation contract.0") (modality "diamond")) + (branch "Post (leaf)" + (builtin "One Step Simplification" (formula "10")) + (builtin "One Step Simplification" (formula "8")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "9")) + (rule "typeEqDerived" (formula "10") (term "0,1,1,1,1") (ifseqformula "9")) + (rule "typeEqDerived" (formula "10") (term "0,0,1,1,1") (ifseqformula "9")) + (builtin "One Step Simplification" (formula "10") (ifInst "" (formula "9")) (ifInst "" (formula "9"))) + (rule "andLeft" (formula "10")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "applyEq" (formula "13") (term "0,1,0") (ifseqformula "10")) + (rule "methodCallReturn" (formula "13") (term "1")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "methodCallEmpty" (formula "13") (term "1")) + (rule "tryEmpty" (formula "13") (term "1")) + (rule "emptyModality" (formula "13") (term "1")) + (rule "andRight" (formula "13")) + (branch "Case 1" + (rule "impRight" (formula "13")) + (rule "andRight" (formula "14")) + (branch "Case 1" + (rule "impRight" (formula "14")) + (builtin "One Step Simplification" (formula "2")) + (builtin "One Step Simplification" (formula "1")) + (builtin "One Step Simplification" (formula "15")) + (rule "closeTrue" (formula "15")) + ) + (branch "Case 2" + (builtin "One Step Simplification" (formula "14") (ifInst "" (formula "12"))) + (rule "closeTrue" (formula "14")) + ) + ) + (branch "Case 2" + (rule "impRight" (formula "13")) + (rule "andRight" (formula "14")) + (branch "Case 1" + (builtin "One Step Simplification" (formula "14") (ifInst "" (formula "12"))) + (rule "closeTrue" (formula "14")) + ) + (branch "Case 2" + (rule "orRight" (formula "14")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Exceptional Post (leaf)" + (builtin "One Step Simplification" (formula "8")) + (builtin "One Step Simplification" (formula "10")) + (rule "andLeft" (formula "8")) + (rule "selectCreatedOfAnonAsFormulaEQ" (formula "9") (term "1,0") (ifseqformula "8")) + (rule "andLeft" (formula "9")) + (rule "andLeft" (formula "9")) + (rule "andLeft" (formula "11")) + (rule "notLeft" (formula "9")) + (rule "replace_known_right" (formula "10") (term "0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "10")) + (rule "true_left" (formula "10")) + (rule "replace_known_right" (formula "10") (term "0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "10")) + (rule "andLeft" (formula "10")) + (rule "methodCallParamThrow" (formula "14") (term "1")) + (rule "tryCatchThrow" (formula "14") (term "1")) + (rule "ifElseUnfold" (formula "14") (term "1") (inst "#boolv=x")) + (rule "variableDeclaration" (formula "14") (term "1") (newnames "x_3")) + (rule "equality_comparison_simple" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "replace_known_right" (formula "14") (term "0,0,1,0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "14")) + (rule "ifElseSplit" (formula "14")) + (branch "if x_3 true" + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch "if x_3 false" + (builtin "One Step Simplification" (formula "1")) + (builtin "One Step Simplification" (formula "15")) + (rule "true_left" (formula "1")) + (rule "ifElseSplit" (formula "14")) + (branch "if exc_52 instanceof java.lang.Throwable true" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "13"))) + (rule "true_left" (formula "1")) + (rule "variableDeclaration" (formula "14") (term "1") (newnames "e")) + (rule "delete_unnecessary_cast" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "assignment" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "emptyModality" (formula "14") (term "1")) + (rule "andRight" (formula "14")) + (branch "Case 1" + (rule "impRight" (formula "14")) + (rule "andRight" (formula "15")) + (branch "Case 1" + (rule "impRight" (formula "15")) + (builtin "One Step Simplification" (formula "2") (ifInst "" (formula "14"))) + (rule "closeFalse" (formula "2")) + ) + (branch "Case 2" + (builtin "One Step Simplification" (formula "15") (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "15")) + ) + ) + (branch "Case 2" + (rule "impRight" (formula "14")) + (rule "andRight" (formula "15")) + (branch "Case 1" + (builtin "One Step Simplification" (formula "15") (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "15")) + ) + (branch "Case 2" + (rule "orRight" (formula "15")) + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "13"))) + (builtin "One Step Simplification" (formula "16")) + (rule "true_left" (formula "1")) + (rule "replace_known_right" (formula "11") (term "0") (ifseqformula "14")) + (builtin "One Step Simplification" (formula "11") (ifInst "" (formula "15"))) + (rule "closeFalse" (formula "11")) + ) + ) + ) + (branch "if exc_52 instanceof java.lang.Throwable false" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "13"))) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Pre (leaf)" + (builtin "One Step Simplification" (formula "8") (ifInst "" (formula "6")) (ifInst "" (formula "2"))) + (rule "closeTrue" (formula "8")) + ) + ) + (branch "if x false" + (builtin "One Step Simplification" (formula "10")) + (builtin "One Step Simplification" (formula "1")) + (rule "notLeft" (formula "1")) + (rule "returnUnfold" (formula "10") (term "1") (inst "#v0=x")) + (rule "variableDeclarationAssign" (formula "10") (term "1")) + (rule "variableDeclaration" (formula "10") (term "1") (newnames "x_2")) + (rule "methodCallWithAssignmentUnfoldArguments" (formula "10") (term "1")) + (rule "variableDeclarationAssign" (formula "10") (term "1")) + (rule "variableDeclaration" (formula "10") (term "1") (newnames "var")) + (rule "assignmentSubtractionInt" (formula "10") (term "1")) + (builtin "One Step Simplification" (formula "10")) + (rule "translateJavaSubInt" (formula "10") (term "0,1,0")) + (rule "polySimp_elimSub" (formula "10") (term "0,1,0")) + (rule "mul_literals" (formula "10") (term "1,0,1,0")) + (rule "polySimp_addComm0" (formula "10") (term "0,1,0")) + (builtin "Use Operation Contract" (formula "10") (newnames "heapBefore_cycleB,result_44,exc_52,heapAfter_cycleB,anon_heap_cycleB") (contract "Example[Example::cycleB(int)].JML operation contract.0") (modality "diamond")) + (branch "Post (cycleB)" + (builtin "One Step Simplification" (formula "7")) + (builtin "One Step Simplification" (formula "12")) + (rule "andLeft" (formula "7")) + (rule "andLeft" (formula "8")) + (rule "typeEqDerived" (formula "9") (term "0,1,1,1,1") (ifseqformula "8")) + (rule "typeEqDerived" (formula "9") (term "0,0,1,1,1") (ifseqformula "8")) + (builtin "One Step Simplification" (formula "9") (ifInst "" (formula "8")) (ifInst "" (formula "8"))) + (rule "andLeft" (formula "9")) + (rule "assignment" (formula "15") (term "1")) + (builtin "One Step Simplification" (formula "15")) + (rule "blockEmpty" (formula "15") (term "1")) + (rule "methodCallReturn" (formula "15") (term "1")) + (rule "assignment" (formula "15") (term "1")) + (builtin "One Step Simplification" (formula "15")) + (rule "methodCallEmpty" (formula "15") (term "1")) + (rule "tryEmpty" (formula "15") (term "1")) + (rule "emptyModality" (formula "15") (term "1")) + (rule "andRight" (formula "15")) + (branch "Case 1" + (rule "impRight" (formula "15")) + (rule "andRight" (formula "16")) + (branch "Case 1" + (rule "impRight" (formula "16")) + (builtin "One Step Simplification" (formula "2")) + (builtin "One Step Simplification" (formula "1")) + (builtin "One Step Simplification" (formula "17")) + (rule "true_left" (formula "2")) + (rule "replace_known_right" (formula "10") (term "1") (ifseqformula "16")) + (builtin "One Step Simplification" (formula "10")) + (rule "notLeft" (formula "10")) + (rule "inEqSimp_ltRight" (formula "15")) + (rule "times_zero_1" (formula "1") (term "0,0")) + (rule "add_zero_left" (formula "1") (term "0")) + (rule "inEqSimp_gtRight" (formula "11")) + (rule "times_zero_1" (formula "1") (term "0,0")) + (rule "add_zero_left" (formula "1") (term "0")) + (rule "inEqSimp_sepPosMonomial0" (formula "1")) + (rule "mul_literals" (formula "1") (term "1")) + (rule "inEqSimp_strengthen0" (formula "1") (ifseqformula "12")) + (rule "add_literals" (formula "1") (term "1")) + (rule "inEqSimp_contradEq3" (formula "12") (ifseqformula "1")) + (rule "add_zero_left" (formula "12") (term "0,0")) + (rule "mul_literals" (formula "12") (term "0,0")) + (rule "qeq_literals" (formula "12") (term "0")) + (builtin "One Step Simplification" (formula "12")) + (rule "false_right" (formula "12")) + (rule "inEqSimp_strengthen1" (formula "2") (ifseqformula "12")) + (rule "add_zero_right" (formula "2") (term "1")) + (rule "inEqSimp_contradEq7" (formula "12") (ifseqformula "2")) + (rule "times_zero_1" (formula "12") (term "1,0,0")) + (rule "add_zero_right" (formula "12") (term "0,0")) + (rule "leq_literals" (formula "12") (term "0")) + (builtin "One Step Simplification" (formula "12")) + (rule "false_right" (formula "12")) + (rule "inEqSimp_contradInEq0" (formula "2") (ifseqformula "1")) + (rule "qeq_literals" (formula "2") (term "0")) + (builtin "One Step Simplification" (formula "2")) + (rule "closeFalse" (formula "2")) + ) + (branch "Case 2" + (builtin "One Step Simplification" (formula "16") (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "16")) + ) + ) + (branch "Case 2" + (rule "impRight" (formula "15")) + (rule "andRight" (formula "16")) + (branch "Case 1" + (builtin "One Step Simplification" (formula "16") (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "16")) + ) + (branch "Case 2" + (rule "orRight" (formula "16")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Exceptional Post (cycleB)" + (builtin "One Step Simplification" (formula "7")) + (builtin "One Step Simplification" (formula "12")) + (rule "andLeft" (formula "7")) + (rule "selectCreatedOfAnonAsFormulaEQ" (formula "8") (term "1,0") (ifseqformula "7")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "9")) + (rule "andLeft" (formula "8")) + (rule "notLeft" (formula "8")) + (rule "replace_known_right" (formula "9") (term "0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "9")) + (rule "true_left" (formula "9")) + (rule "replace_known_right" (formula "9") (term "0,0") (ifseqformula "10")) + (builtin "One Step Simplification" (formula "9")) + (rule "andLeft" (formula "9")) + (rule "blockThrow" (formula "16") (term "1")) + (rule "methodCallParamThrow" (formula "16") (term "1")) + (rule "tryCatchThrow" (formula "16") (term "1")) + (rule "ifElseUnfold" (formula "16") (term "1") (inst "#boolv=x")) + (rule "variableDeclaration" (formula "16") (term "1") (newnames "x_3")) + (rule "equality_comparison_simple" (formula "16") (term "1")) + (builtin "One Step Simplification" (formula "16")) + (rule "replace_known_right" (formula "16") (term "0,0,1,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "16")) + (rule "ifElseSplit" (formula "16")) + (branch "if x_3 true" + (builtin "One Step Simplification" (formula "17")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch "if x_3 false" + (builtin "One Step Simplification" (formula "1")) + (builtin "One Step Simplification" (formula "17")) + (rule "true_left" (formula "1")) + (rule "ifElseSplit" (formula "16")) + (branch "if exc_52 instanceof java.lang.Throwable true" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12"))) + (rule "true_left" (formula "1")) + (rule "variableDeclaration" (formula "16") (term "1") (newnames "e")) + (rule "delete_unnecessary_cast" (formula "16") (term "1")) + (builtin "One Step Simplification" (formula "1")) + (builtin "One Step Simplification" (formula "17")) + (rule "true_left" (formula "1")) + (rule "assignment" (formula "16") (term "1")) + (builtin "One Step Simplification" (formula "16")) + (rule "emptyModality" (formula "16") (term "1")) + (rule "andRight" (formula "16")) + (branch "Case 1" + (rule "impRight" (formula "16")) + (rule "andRight" (formula "17")) + (branch "Case 1" + (rule "impRight" (formula "17")) + (builtin "One Step Simplification" (formula "2") (ifInst "" (formula "13"))) + (rule "closeFalse" (formula "2")) + ) + (branch "Case 2" + (builtin "One Step Simplification" (formula "17") (ifInst "" (formula "10"))) + (rule "closeTrue" (formula "17")) + ) + ) + (branch "Case 2" + (rule "impRight" (formula "16")) + (rule "andRight" (formula "17")) + (branch "Case 1" + (builtin "One Step Simplification" (formula "17") (ifInst "" (formula "10"))) + (rule "closeTrue" (formula "17")) + ) + (branch "Case 2" + (rule "orRight" (formula "17")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12"))) + (builtin "One Step Simplification" (formula "18")) + (builtin "One Step Simplification" (formula "17")) + (rule "true_left" (formula "1")) + (rule "replace_known_right" (formula "10") (term "0") (ifseqformula "16")) + (builtin "One Step Simplification" (formula "10") (ifInst "" (formula "17"))) + (rule "closeFalse" (formula "10")) + ) + ) + ) + (branch "if exc_52 instanceof java.lang.Throwable false" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12"))) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Pre (cycleB)" + (builtin "One Step Simplification" (formula "10") (ifInst "" (formula "1")) (ifInst "" (formula "5"))) + (rule "measuredByCheck" (formula "10") (term "1") (ifseqformula "4")) + (rule "precOfInt" (formula "10") (term "1")) + (rule "inEqSimp_ltRight" (formula "9")) + (rule "times_zero_1" (formula "1") (term "0,0")) + (rule "add_zero_left" (formula "1") (term "0")) + (rule "inEqSimp_ltToLeq" (formula "10") (term "1,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,1")) + (rule "polySimp_addAssoc" (formula "10") (term "0,1,1")) + (rule "polySimp_addComm1" (formula "10") (term "0,0,1,1")) + (rule "add_literals" (formula "10") (term "0,0,0,1,1")) + (rule "add_zero_left" (formula "10") (term "0,0,1,1")) + (rule "polySimp_pullOutFactor2" (formula "10") (term "0,1,1")) + (rule "add_literals" (formula "10") (term "1,0,1,1")) + (rule "times_zero_1" (formula "10") (term "0,1,1")) + (rule "leq_literals" (formula "10") (term "1,1")) + (builtin "One Step Simplification" (formula "10")) + (rule "inEqSimp_homoInEq0" (formula "10") (term "1")) + (rule "times_zero_2" (formula "10") (term "1,0,1")) + (rule "add_zero_right" (formula "10") (term "0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "10") (term "0,0")) + (rule "mul_literals" (formula "10") (term "1,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "10") (term "1")) + (rule "mul_literals" (formula "10") (term "1,1")) + (rule "inEqSimp_strengthen1" (formula "1") (ifseqformula "8")) + (rule "add_zero_right" (formula "1") (term "1")) + (rule "replace_known_left" (formula "10") (term "1") (ifseqformula "1")) + (builtin "One Step Simplification" (formula "10")) + (rule "notRight" (formula "10")) + (rule "inEqSimp_contradEq7" (formula "9") (ifseqformula "2")) + (rule "times_zero_1" (formula "9") (term "1,0,0")) + (rule "add_zero_right" (formula "9") (term "0,0")) + (rule "leq_literals" (formula "9") (term "0")) + (builtin "One Step Simplification" (formula "9")) + (rule "false_right" (formula "9")) + (rule "inEqSimp_strengthen0" (formula "1") (ifseqformula "8")) + (rule "add_literals" (formula "1") (term "1")) + (rule "inEqSimp_contradEq3" (formula "8") (ifseqformula "1")) + (rule "add_zero_left" (formula "8") (term "0,0")) + (rule "mul_literals" (formula "8") (term "0,0")) + (rule "qeq_literals" (formula "8") (term "0")) + (builtin "One Step Simplification" (formula "8")) + (rule "false_right" (formula "8")) + (rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "2")) + (rule "qeq_literals" (formula "1") (term "0")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + ) +) +) +} diff --git a/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleA(int)).JML operation contract.1.proof b/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleA(int)).JML operation contract.1.proof new file mode 100755 index 00000000000..1826af18877 --- /dev/null +++ b/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleA(int)).JML operation contract.1.proof @@ -0,0 +1,416 @@ +\profile "Java Profile"; + +\settings { +"#Proof-Settings-Config-File +#Mon Mar 09 18:28:37 CET 2020 +[Labels]UseOriginLabels=true +[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON +[SMTSettings]invariantForall=false +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:off , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:off , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , methodExpansion-methodExpansion\\:modularOnly +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT +[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE +[SMTSettings]UseBuiltUniqueness=false +[SMTSettings]explicitTypeHierarchy=false +[SMTSettings]instantiateHierarchyAssumptions=true +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_COMPLETION +[SMTSettings]SelectedTaclets= +[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON +[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF +[Strategy]MaximumNumberOfAutomaticApplications=7000 +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED +[SMTSettings]useConstantsForBigOrSmallIntegers=true +[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE +[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF +[Strategy]Timeout=-1 +[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_ON +[SMTSettings]useUninterpretedMultiplication=true +[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[SMTSettings]maxGenericSorts=2 +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +[SMTSettings]integersMinimum=-2147483645 +[StrategyProperty]VBT_PHASE=VBT_SYM_EX +[SMTSettings]integersMaximum=2147483645 +" +} + +\javaSource "src"; + +\proofObligation "#Proof Obligation Settings +#Mon Mar 09 18:28:37 CET 2020 +contract=Example[Example\\:\\:cycleA(int)].JML operation contract.1 +name=Example[Example\\:\\:cycleA(int)].JML operation contract.1 +class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO +"; + +\proof { +(keyLog "0" (keyUser "Banach" ) (keyVersion "9e1d8db9a5")) + +(autoModeTime "250") + +(branch "dummy ID" + (builtin "One Step Simplification" (formula "1") (newnames "param,self_129,result_109,exc_129,heapAtPre_0,o,f")) +(rule "impRight" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "notLeft" (formula "2")) +(rule "assignment" (formula "7") (term "1")) + (builtin "One Step Simplification" (formula "7")) +(rule "methodBodyExpand" (formula "7") (term "1") (newnames "heapBefore_cycleA,savedHeapBefore_cycleA")) + (builtin "One Step Simplification" (formula "7")) +(rule "ifElseUnfold" (formula "7") (term "1") (inst "#boolv=x")) +(rule "variableDeclaration" (formula "7") (term "1") (newnames "x")) +(rule "compound_assignment_5_nonsimple" (formula "7") (term "1")) +(rule "ifElseUnfold" (formula "7") (term "1") (inst "#boolv=x_1")) +(rule "variableDeclaration" (formula "7") (term "1") (newnames "x_1")) +(rule "equality_comparison_simple" (formula "7") (term "1")) + (builtin "One Step Simplification" (formula "7")) +(rule "ifElseSplit" (formula "7")) +(branch "if x_1 true" + (builtin "One Step Simplification" (formula "8")) + (builtin "One Step Simplification" (formula "1")) + (rule "ifElseSkipElse" (formula "8") (term "1")) + (builtin "One Step Simplification" (formula "8")) + (rule "assignment" (formula "8") (term "1")) + (builtin "One Step Simplification" (formula "8")) + (rule "applyEq" (formula "5") (term "0") (ifseqformula "1")) + (rule "returnUnfold" (formula "8") (term "1") (inst "#v0=x")) + (rule "variableDeclarationAssign" (formula "8") (term "1")) + (rule "variableDeclaration" (formula "8") (term "1") (newnames "x_2")) + (builtin "Use Operation Contract" (formula "8") (newnames "heapBefore_leaf,result_110,exc_130,heapAfter_leaf,anon_heap_leaf") (contract "Example[Example::leaf()].JML operation contract.0") (modality "box")) + (branch "Post (leaf)" + (builtin "One Step Simplification" (formula "10")) + (builtin "One Step Simplification" (formula "8")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "9")) + (rule "typeEqDerived" (formula "10") (term "0,1,1,1,1") (ifseqformula "9")) + (rule "typeEqDerived" (formula "10") (term "0,0,1,1,1") (ifseqformula "9")) + (builtin "One Step Simplification" (formula "10") (ifInst "" (formula "9")) (ifInst "" (formula "9"))) + (rule "andLeft" (formula "10")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "applyEq" (formula "13") (term "0,1,0") (ifseqformula "10")) + (rule "methodCallReturn" (formula "13") (term "1")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "methodCallEmpty" (formula "13") (term "1")) + (rule "tryEmpty" (formula "13") (term "1")) + (rule "emptyModality" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13") (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "13")) + ) + (branch "Exceptional Post (leaf)" + (builtin "One Step Simplification" (formula "10")) + (builtin "One Step Simplification" (formula "8")) + (rule "andLeft" (formula "8")) + (rule "selectCreatedOfAnonAsFormulaEQ" (formula "9") (term "1,0") (ifseqformula "8")) + (rule "andLeft" (formula "9")) + (rule "andLeft" (formula "10")) + (rule "andLeft" (formula "9")) + (rule "notLeft" (formula "9")) + (rule "replace_known_right" (formula "10") (term "0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "10")) + (rule "true_left" (formula "10")) + (rule "replace_known_right" (formula "10") (term "0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "10")) + (rule "andLeft" (formula "10")) + (rule "methodCallParamThrow" (formula "14") (term "1")) + (rule "tryCatchThrow" (formula "14") (term "1")) + (rule "ifElseUnfold" (formula "14") (term "1") (inst "#boolv=x")) + (rule "variableDeclaration" (formula "14") (term "1") (newnames "x_3")) + (rule "equality_comparison_simple" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "replace_known_right" (formula "14") (term "0,0,1,0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "14")) + (rule "ifElseSplit" (formula "14")) + (branch "if x_3 true" + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch "if x_3 false" + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "ifElseSplit" (formula "14")) + (branch "if exc_130 instanceof java.lang.Throwable true" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "13"))) + (rule "true_left" (formula "1")) + (rule "variableDeclaration" (formula "14") (term "1") (newnames "e")) + (rule "delete_unnecessary_cast" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "assignment" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "emptyModality" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14") (ifInst "" (formula "12")) (ifInst "" (formula "12")) (ifInst "" (formula "10")) (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "14")) + ) + (branch "if exc_130 instanceof java.lang.Throwable false" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "13"))) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Pre (leaf)" + (builtin "One Step Simplification" (formula "8") (ifInst "" (formula "6")) (ifInst "" (formula "2"))) + (rule "closeTrue" (formula "8")) + ) +) +(branch "if x_1 false" + (builtin "One Step Simplification" (formula "8")) + (builtin "One Step Simplification" (formula "1")) + (rule "notLeft" (formula "1")) + (rule "equality_comparison_simple" (formula "8") (term "1")) + (builtin "One Step Simplification" (formula "8")) + (rule "blockEmpty" (formula "8") (term "1")) + (rule "ifElseSplit" (formula "8")) + (branch "if x true" + (builtin "One Step Simplification" (formula "9")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEq" (formula "5") (term "0") (ifseqformula "1")) + (rule "applyEq" (formula "7") (term "0") (ifseqformula "1")) + (rule "equal_literals" (formula "7")) + (rule "false_right" (formula "7")) + (rule "returnUnfold" (formula "8") (term "1") (inst "#v0=x")) + (rule "variableDeclarationAssign" (formula "8") (term "1")) + (rule "variableDeclaration" (formula "8") (term "1") (newnames "x_2")) + (builtin "Use Operation Contract" (formula "8") (newnames "heapBefore_leaf,result_110,exc_130,heapAfter_leaf,anon_heap_leaf") (contract "Example[Example::leaf()].JML operation contract.0") (modality "box")) + (branch "Post (leaf)" + (builtin "One Step Simplification" (formula "10")) + (builtin "One Step Simplification" (formula "8")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "9")) + (rule "typeEqDerived" (formula "10") (term "0,1,1,1,1") (ifseqformula "9")) + (rule "typeEqDerived" (formula "10") (term "0,0,1,1,1") (ifseqformula "9")) + (builtin "One Step Simplification" (formula "10") (ifInst "" (formula "9")) (ifInst "" (formula "9"))) + (rule "andLeft" (formula "10")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "applyEq" (formula "13") (term "0,1,0") (ifseqformula "10")) + (rule "methodCallReturn" (formula "13") (term "1")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "methodCallEmpty" (formula "13") (term "1")) + (rule "tryEmpty" (formula "13") (term "1")) + (rule "emptyModality" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13") (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "13")) + ) + (branch "Exceptional Post (leaf)" + (builtin "One Step Simplification" (formula "10")) + (builtin "One Step Simplification" (formula "8")) + (rule "andLeft" (formula "8")) + (rule "selectCreatedOfAnonAsFormulaEQ" (formula "9") (term "1,0") (ifseqformula "8")) + (rule "andLeft" (formula "9")) + (rule "andLeft" (formula "10")) + (rule "andLeft" (formula "9")) + (rule "notLeft" (formula "9")) + (rule "replace_known_right" (formula "10") (term "0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "10")) + (rule "true_left" (formula "10")) + (rule "replace_known_right" (formula "10") (term "0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "10")) + (rule "andLeft" (formula "10")) + (rule "methodCallParamThrow" (formula "14") (term "1")) + (rule "tryCatchThrow" (formula "14") (term "1")) + (rule "ifElseUnfold" (formula "14") (term "1") (inst "#boolv=x")) + (rule "variableDeclaration" (formula "14") (term "1") (newnames "x_3")) + (rule "equality_comparison_simple" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "replace_known_right" (formula "14") (term "0,0,1,0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "14")) + (rule "ifElseSplit" (formula "14")) + (branch "if x_3 true" + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch "if x_3 false" + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "ifElseSplit" (formula "14")) + (branch "if exc_130 instanceof java.lang.Throwable true" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "13"))) + (rule "true_left" (formula "1")) + (rule "variableDeclaration" (formula "14") (term "1") (newnames "e")) + (rule "delete_unnecessary_cast" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "assignment" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "emptyModality" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14") (ifInst "" (formula "12")) (ifInst "" (formula "12")) (ifInst "" (formula "10")) (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "14")) + ) + (branch "if exc_130 instanceof java.lang.Throwable false" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "13"))) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Pre (leaf)" + (builtin "One Step Simplification" (formula "8") (ifInst "" (formula "6")) (ifInst "" (formula "2"))) + (rule "closeTrue" (formula "8")) + ) + ) + (branch "if x false" + (builtin "One Step Simplification" (formula "9")) + (builtin "One Step Simplification" (formula "1")) + (rule "notLeft" (formula "1")) + (rule "returnUnfold" (formula "9") (term "1") (inst "#v0=x")) + (rule "variableDeclarationAssign" (formula "9") (term "1")) + (rule "variableDeclaration" (formula "9") (term "1") (newnames "x_2")) + (rule "methodCallWithAssignmentUnfoldArguments" (formula "9") (term "1")) + (rule "variableDeclarationAssign" (formula "9") (term "1")) + (rule "variableDeclaration" (formula "9") (term "1") (newnames "var")) + (rule "assignmentSubtractionInt" (formula "9") (term "1")) + (builtin "One Step Simplification" (formula "9")) + (rule "translateJavaSubInt" (formula "9") (term "0,1,0")) + (rule "polySimp_elimSub" (formula "9") (term "0,1,0")) + (rule "mul_literals" (formula "9") (term "1,0,1,0")) + (rule "polySimp_addComm0" (formula "9") (term "0,1,0")) + (builtin "Use Operation Contract" (formula "9") (newnames "heapBefore_cycleB,result_110,exc_130,heapAfter_cycleB,anon_heap_cycleB") (contract "Example[Example::cycleB(int)].JML operation contract.0#Example[Example::cycleB(int)].JML operation contract.1") (modality "box")) + (branch "Post (cycleB)" + (builtin "One Step Simplification" (formula "11")) + (builtin "One Step Simplification" (formula "7") (ifInst "" (formula "5")) (ifInst "" (formula "5"))) + (rule "andLeft" (formula "7")) + (rule "andLeft" (formula "8")) + (rule "typeEqDerived" (formula "9") (term "0,1,1,1,1,1") (ifseqformula "8")) + (rule "typeEqDerived" (formula "9") (term "0,0,1,1,1,1") (ifseqformula "8")) + (rule "typeEqDerived" (formula "9") (term "0,0,1,1,1,1,0") (ifseqformula "8")) + (rule "typeEqDerived" (formula "9") (term "0,1,1,1,1,1,0") (ifseqformula "8")) + (builtin "One Step Simplification" (formula "9") (ifInst "" (formula "8")) (ifInst "" (formula "8")) (ifInst "" (formula "8")) (ifInst "" (formula "8"))) + (rule "andLeft" (formula "9")) + (rule "andLeft" (formula "10")) + (rule "replace_known_left" (formula "9") (term "0,1") (ifseqformula "10")) + (builtin "One Step Simplification" (formula "9") (ifInst "" (formula "11"))) + (rule "true_left" (formula "9")) + (rule "inEqSimp_gtToGeq" (formula "9") (term "0")) + (rule "times_zero_1" (formula "9") (term "1,0,0,0")) + (rule "add_zero_right" (formula "9") (term "0,0,0")) + (rule "polySimp_addAssoc" (formula "9") (term "0,0")) + (rule "add_literals" (formula "9") (term "0,0,0")) + (rule "assignment" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "blockEmpty" (formula "14") (term "1")) + (rule "inEqSimp_sepPosMonomial1" (formula "9") (term "0")) + (rule "mul_literals" (formula "9") (term "1,0")) + (rule "methodCallReturn" (formula "14") (term "1")) + (rule "assignment" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "methodCallEmpty" (formula "14") (term "1")) + (rule "tryEmpty" (formula "14") (term "1")) + (rule "emptyModality" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14") (ifInst "" (formula "10"))) + (rule "impRight" (formula "14")) + (rule "replace_known_right" (formula "10") (term "1") (ifseqformula "15")) + (builtin "One Step Simplification" (formula "10")) + (rule "notLeft" (formula "10")) + (rule "inEqSimp_geqRight" (formula "11")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_literals" (formula "1") (term "0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "1")) + (rule "mul_literals" (formula "1") (term "1")) + (rule "inEqSimp_strengthen0" (formula "1") (ifseqformula "12")) + (rule "add_literals" (formula "1") (term "1")) + (rule "inEqSimp_contradEq3" (formula "12") (ifseqformula "1")) + (rule "add_zero_left" (formula "12") (term "0,0")) + (rule "mul_literals" (formula "12") (term "0,0")) + (rule "qeq_literals" (formula "12") (term "0")) + (builtin "One Step Simplification" (formula "12")) + (rule "false_right" (formula "12")) + (rule "inEqSimp_strengthen1" (formula "2") (ifseqformula "12")) + (rule "add_zero_right" (formula "2") (term "1")) + (rule "inEqSimp_contradEq7" (formula "12") (ifseqformula "2")) + (rule "times_zero_1" (formula "12") (term "1,0,0")) + (rule "add_zero_right" (formula "12") (term "0,0")) + (rule "leq_literals" (formula "12") (term "0")) + (builtin "One Step Simplification" (formula "12")) + (rule "false_right" (formula "12")) + (rule "inEqSimp_contradInEq0" (formula "2") (ifseqformula "1")) + (rule "qeq_literals" (formula "2") (term "0")) + (builtin "One Step Simplification" (formula "2")) + (rule "closeFalse" (formula "2")) + ) + (branch "Exceptional Post (cycleB)" + (builtin "One Step Simplification" (formula "11")) + (builtin "One Step Simplification" (formula "7") (ifInst "" (formula "5")) (ifInst "" (formula "5"))) + (rule "andLeft" (formula "7")) + (rule "selectCreatedOfAnonAsFormulaEQ" (formula "8") (term "1,0") (ifseqformula "7")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "10")) + (rule "notLeft" (formula "8")) + (rule "andLeft" (formula "10")) + (rule "replace_known_right" (formula "10") (term "0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "10")) + (rule "true_left" (formula "10")) + (rule "replace_known_right" (formula "10") (term "0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "10")) + (rule "andLeft" (formula "10")) + (rule "replace_known_right" (formula "9") (term "0,0,1") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "9") (ifInst "" (formula "10")) (ifInst "" (formula "12")) (ifInst "" (formula "10")) (ifInst "" (formula "11"))) + (rule "true_left" (formula "9")) + (rule "blockThrow" (formula "15") (term "1")) + (rule "methodCallParamThrow" (formula "15") (term "1")) + (rule "tryCatchThrow" (formula "15") (term "1")) + (rule "ifElseUnfold" (formula "15") (term "1") (inst "#boolv=x")) + (rule "variableDeclaration" (formula "15") (term "1") (newnames "x_3")) + (rule "equality_comparison_simple" (formula "15") (term "1")) + (builtin "One Step Simplification" (formula "15")) + (rule "replace_known_right" (formula "15") (term "0,0,1,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "15")) + (rule "ifElseSplit" (formula "15")) + (branch "if x_3 true" + (builtin "One Step Simplification" (formula "16")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch "if x_3 false" + (builtin "One Step Simplification" (formula "16")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "ifElseSplit" (formula "15")) + (branch "if exc_130 instanceof java.lang.Throwable true" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12"))) + (rule "true_left" (formula "1")) + (rule "variableDeclaration" (formula "15") (term "1") (newnames "e")) + (rule "delete_unnecessary_cast" (formula "15") (term "1")) + (builtin "One Step Simplification" (formula "16")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "assignment" (formula "15") (term "1")) + (builtin "One Step Simplification" (formula "15")) + (rule "emptyModality" (formula "15") (term "1")) + (builtin "One Step Simplification" (formula "15") (ifInst "" (formula "11")) (ifInst "" (formula "11")) (ifInst "" (formula "9")) (ifInst "" (formula "10"))) + (rule "closeTrue" (formula "15")) + ) + (branch "if exc_130 instanceof java.lang.Throwable false" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12"))) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Pre (cycleB)" + (builtin "One Step Simplification" (formula "9") (ifInst "" (formula "1")) (ifInst "" (formula "5"))) + (rule "closeTrue" (formula "9")) + ) + ) +) +) +} diff --git a/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleB(int)).JML operation contract.0.proof b/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleB(int)).JML operation contract.0.proof new file mode 100755 index 00000000000..e03d39c6148 --- /dev/null +++ b/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleB(int)).JML operation contract.0.proof @@ -0,0 +1,265 @@ +\profile "Java Profile"; + +\settings { +"#Proof-Settings-Config-File +#Mon Mar 09 18:27:59 CET 2020 +[Labels]UseOriginLabels=true +[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON +[SMTSettings]invariantForall=false +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:off , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:off , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , methodExpansion-methodExpansion\\:modularOnly +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT +[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE +[SMTSettings]UseBuiltUniqueness=false +[SMTSettings]explicitTypeHierarchy=false +[SMTSettings]instantiateHierarchyAssumptions=true +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_COMPLETION +[SMTSettings]SelectedTaclets= +[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON +[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF +[Strategy]MaximumNumberOfAutomaticApplications=7000 +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED +[SMTSettings]useConstantsForBigOrSmallIntegers=true +[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE +[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF +[Strategy]Timeout=-1 +[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_ON +[SMTSettings]useUninterpretedMultiplication=true +[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[SMTSettings]maxGenericSorts=2 +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +[SMTSettings]integersMinimum=-2147483645 +[StrategyProperty]VBT_PHASE=VBT_SYM_EX +[SMTSettings]integersMaximum=2147483645 +" +} + +\javaSource "src"; + +\proofObligation "#Proof Obligation Settings +#Mon Mar 09 18:27:59 CET 2020 +contract=Example[Example\\:\\:cycleB(int)].JML operation contract.0 +name=Example[Example\\:\\:cycleB(int)].JML operation contract.0 +class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO +"; + +\proof { +(keyLog "0" (keyUser "Banach" ) (keyVersion "9e1d8db9a5")) + +(autoModeTime "98") + +(branch "dummy ID" + (builtin "One Step Simplification" (formula "1") (newnames "param,self_25,result_21,exc_25,heapAtPre_0,o,f")) +(rule "impRight" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "3")) +(rule "andLeft" (formula "1")) +(rule "notLeft" (formula "5")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "notLeft" (formula "2")) +(rule "assignment" (formula "8") (term "1")) + (builtin "One Step Simplification" (formula "8")) +(rule "methodBodyExpand" (formula "8") (term "1") (newnames "heapBefore_cycleB,savedHeapBefore_cycleB")) + (builtin "One Step Simplification" (formula "8")) +(rule "returnUnfold" (formula "8") (term "1") (inst "#v0=x")) +(rule "variableDeclarationAssign" (formula "8") (term "1")) +(rule "variableDeclaration" (formula "8") (term "1") (newnames "x")) +(rule "methodCallWithAssignmentUnfoldArguments" (formula "8") (term "1")) +(rule "variableDeclarationAssign" (formula "8") (term "1")) +(rule "variableDeclaration" (formula "8") (term "1") (newnames "var")) +(rule "assignmentSubtractionInt" (formula "8") (term "1")) + (builtin "One Step Simplification" (formula "8")) +(rule "translateJavaSubInt" (formula "8") (term "0,1,0")) +(rule "polySimp_elimSub" (formula "8") (term "0,1,0")) +(rule "mul_literals" (formula "8") (term "1,0,1,0")) +(rule "polySimp_addComm0" (formula "8") (term "0,1,0")) + (builtin "Use Operation Contract" (formula "8") (newnames "heapBefore_cycleA,result_22,exc_26,heapAfter_cycleA,anon_heap_cycleA") (contract "Example[Example::cycleA(int)].JML operation contract.0") (modality "diamond")) +(branch "Post (cycleA)" + (builtin "One Step Simplification" (formula "7")) + (builtin "One Step Simplification" (formula "10")) + (rule "andLeft" (formula "7")) + (rule "andLeft" (formula "8")) + (rule "typeEqDerived" (formula "9") (term "0,1,1,1,1") (ifseqformula "8")) + (rule "typeEqDerived" (formula "9") (term "0,0,1,1,1") (ifseqformula "8")) + (builtin "One Step Simplification" (formula "9") (ifInst "" (formula "8")) (ifInst "" (formula "8"))) + (rule "andLeft" (formula "9")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "blockEmpty" (formula "13") (term "1")) + (rule "methodCallReturn" (formula "13") (term "1")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "methodCallEmpty" (formula "13") (term "1")) + (rule "tryEmpty" (formula "13") (term "1")) + (rule "emptyModality" (formula "13") (term "1")) + (rule "andRight" (formula "13")) + (branch "Case 1" + (rule "impRight" (formula "13")) + (rule "andRight" (formula "14")) + (branch "Case 1" + (rule "impRight" (formula "14")) + (builtin "One Step Simplification" (formula "2")) + (builtin "One Step Simplification" (formula "1")) + (builtin "One Step Simplification" (formula "15")) + (rule "true_left" (formula "2")) + (rule "replace_known_right" (formula "10") (term "1") (ifseqformula "14")) + (builtin "One Step Simplification" (formula "10")) + (rule "notLeft" (formula "10")) + (rule "inEqSimp_leqRight" (formula "13")) + (rule "times_zero_1" (formula "1") (term "1,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0")) + (rule "close" (formula "12") (ifseqformula "1")) + ) + (branch "Case 2" + (builtin "One Step Simplification" (formula "14") (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "14")) + ) + ) + (branch "Case 2" + (rule "impRight" (formula "13")) + (rule "andRight" (formula "14")) + (branch "Case 1" + (builtin "One Step Simplification" (formula "14") (ifInst "" (formula "11"))) + (rule "closeTrue" (formula "14")) + ) + (branch "Case 2" + (rule "orRight" (formula "14")) + (builtin "One Step Simplification" (formula "14")) + (rule "closeTrue" (formula "14")) + ) + ) +) +(branch "Exceptional Post (cycleA)" + (builtin "One Step Simplification" (formula "10")) + (builtin "One Step Simplification" (formula "7")) + (rule "andLeft" (formula "7")) + (rule "selectCreatedOfAnonAsFormulaEQ" (formula "8") (term "1,0") (ifseqformula "7")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "10")) + (rule "notLeft" (formula "8")) + (rule "replace_known_right" (formula "9") (term "0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "9")) + (rule "true_left" (formula "9")) + (rule "replace_known_right" (formula "9") (term "0,0") (ifseqformula "10")) + (builtin "One Step Simplification" (formula "9")) + (rule "andLeft" (formula "9")) + (rule "blockThrow" (formula "14") (term "1")) + (rule "methodCallParamThrow" (formula "14") (term "1")) + (rule "tryCatchThrow" (formula "14") (term "1")) + (rule "ifElseUnfold" (formula "14") (term "1") (inst "#boolv=x")) + (rule "variableDeclaration" (formula "14") (term "1") (newnames "x_1")) + (rule "equality_comparison_simple" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "replace_known_right" (formula "14") (term "0,0,1,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "14")) + (rule "ifElseSplit" (formula "14")) + (branch "if x_1 true" + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch "if x_1 false" + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "ifElseSplit" (formula "14")) + (branch "if exc_26 instanceof java.lang.Throwable true" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12"))) + (rule "true_left" (formula "1")) + (rule "variableDeclaration" (formula "14") (term "1") (newnames "e")) + (rule "delete_unnecessary_cast" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "15")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "assignment" (formula "14") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (rule "emptyModality" (formula "14") (term "1")) + (rule "andRight" (formula "14")) + (branch "Case 1" + (rule "impRight" (formula "14")) + (rule "andRight" (formula "15")) + (branch "Case 1" + (rule "impRight" (formula "15")) + (builtin "One Step Simplification" (formula "2") (ifInst "" (formula "13"))) + (rule "closeFalse" (formula "2")) + ) + (branch "Case 2" + (builtin "One Step Simplification" (formula "15") (ifInst "" (formula "10"))) + (rule "closeTrue" (formula "15")) + ) + ) + (branch "Case 2" + (rule "impRight" (formula "14")) + (rule "andRight" (formula "15")) + (branch "Case 1" + (builtin "One Step Simplification" (formula "15") (ifInst "" (formula "10"))) + (rule "closeTrue" (formula "15")) + ) + (branch "Case 2" + (rule "orRight" (formula "15")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12"))) + (builtin "One Step Simplification" (formula "16")) + (builtin "One Step Simplification" (formula "15")) + (rule "true_left" (formula "1")) + (rule "replace_known_right" (formula "10") (term "1") (ifseqformula "15")) + (builtin "One Step Simplification" (formula "10") (ifInst "" (formula "14"))) + (rule "closeFalse" (formula "10")) + ) + ) + ) + (branch "if exc_26 instanceof java.lang.Throwable false" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12"))) + (rule "closeFalse" (formula "1")) + ) + ) +) +(branch "Pre (cycleA)" + (builtin "One Step Simplification" (formula "8") (ifInst "" (formula "1")) (ifInst "" (formula "5"))) + (rule "measuredByCheck" (formula "8") (term "1") (ifseqformula "4")) + (rule "precOfInt" (formula "8") (term "1")) + (rule "inEqSimp_leqRight" (formula "7")) + (rule "times_zero_1" (formula "1") (term "1,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0")) + (rule "inEqSimp_ltToLeq" (formula "8") (term "0,0")) + (rule "times_zero_1" (formula "8") (term "1,0,0,0,0")) + (rule "add_zero_right" (formula "8") (term "0,0,0,0")) + (rule "polySimp_addAssoc" (formula "8") (term "0,0,0")) + (rule "add_literals" (formula "8") (term "0,0,0,0")) + (rule "add_zero_left" (formula "8") (term "0,0,0")) + (rule "inEqSimp_ltToLeq" (formula "8") (term "1,1")) + (rule "polySimp_mulComm0" (formula "8") (term "1,0,0,1,1")) + (rule "polySimp_addAssoc" (formula "8") (term "0,1,1")) + (rule "polySimp_addComm1" (formula "8") (term "0,0,1,1")) + (rule "add_literals" (formula "8") (term "0,0,0,1,1")) + (rule "add_zero_left" (formula "8") (term "0,0,1,1")) + (rule "polySimp_pullOutFactor2" (formula "8") (term "0,1,1")) + (rule "add_literals" (formula "8") (term "1,0,1,1")) + (rule "times_zero_1" (formula "8") (term "0,1,1")) + (rule "leq_literals" (formula "8") (term "1,1")) + (builtin "One Step Simplification" (formula "8")) + (rule "inEqSimp_homoInEq0" (formula "8") (term "1")) + (rule "times_zero_2" (formula "8") (term "1,0,1")) + (rule "add_zero_right" (formula "8") (term "0,1")) + (rule "replace_known_left" (formula "8") (term "1") (ifseqformula "1")) + (builtin "One Step Simplification" (formula "8")) + (rule "notRight" (formula "8")) + (rule "inEqSimp_sepPosMonomial1" (formula "2")) + (rule "mul_literals" (formula "2") (term "1")) + (rule "inEqSimp_contradInEq0" (formula "2") (ifseqformula "1")) + (rule "qeq_literals" (formula "2") (term "0")) + (builtin "One Step Simplification" (formula "2")) + (rule "closeFalse" (formula "2")) +) +) +} diff --git a/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleB(int)).JML operation contract.1.proof b/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleB(int)).JML operation contract.1.proof new file mode 100755 index 00000000000..0d0f18980d8 --- /dev/null +++ b/keyext.proofmanagement/src/test/pmexample2/Example(Example__cycleB(int)).JML operation contract.1.proof @@ -0,0 +1,182 @@ +\profile "Java Profile"; + +\settings { +"#Proof-Settings-Config-File +#Mon Mar 09 18:28:33 CET 2020 +[Labels]UseOriginLabels=true +[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON +[SMTSettings]invariantForall=false +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:off , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:off , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , methodExpansion-methodExpansion\\:modularOnly +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT +[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE +[SMTSettings]UseBuiltUniqueness=false +[SMTSettings]explicitTypeHierarchy=false +[SMTSettings]instantiateHierarchyAssumptions=true +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_COMPLETION +[SMTSettings]SelectedTaclets= +[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON +[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF +[Strategy]MaximumNumberOfAutomaticApplications=7000 +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED +[SMTSettings]useConstantsForBigOrSmallIntegers=true +[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE +[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF +[Strategy]Timeout=-1 +[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_ON +[SMTSettings]useUninterpretedMultiplication=true +[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[SMTSettings]maxGenericSorts=2 +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +[SMTSettings]integersMinimum=-2147483645 +[StrategyProperty]VBT_PHASE=VBT_SYM_EX +[SMTSettings]integersMaximum=2147483645 +" +} + +\javaSource "src"; + +\proofObligation "#Proof Obligation Settings +#Mon Mar 09 18:28:33 CET 2020 +contract=Example[Example\\:\\:cycleB(int)].JML operation contract.1 +name=Example[Example\\:\\:cycleB(int)].JML operation contract.1 +class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO +"; + +\proof { +(keyLog "0" (keyUser "Banach" ) (keyVersion "9e1d8db9a5")) + +(autoModeTime "94") + +(branch "dummy ID" + (builtin "One Step Simplification" (formula "1") (newnames "param,self_103,result_87,exc_103,heapAtPre_0,o,f")) +(rule "impRight" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "notLeft" (formula "2")) +(rule "inEqSimp_gtToGeq" (formula "7") (term "0,0,1,0,0,1")) +(rule "times_zero_1" (formula "7") (term "1,0,0,0,0,1,0,0,1")) +(rule "add_literals" (formula "7") (term "0,0,0,0,1,0,0,1")) +(rule "assignment" (formula "7") (term "1")) + (builtin "One Step Simplification" (formula "7")) +(rule "inEqSimp_sepPosMonomial1" (formula "7") (term "0,0,1,0,0,1")) +(rule "mul_literals" (formula "7") (term "1,0,0,1,0,0,1")) +(rule "methodBodyExpand" (formula "7") (term "1") (newnames "heapBefore_cycleB,savedHeapBefore_cycleB")) + (builtin "One Step Simplification" (formula "7")) +(rule "returnUnfold" (formula "7") (term "1") (inst "#v0=x")) +(rule "variableDeclarationAssign" (formula "7") (term "1")) +(rule "variableDeclaration" (formula "7") (term "1") (newnames "x")) +(rule "methodCallWithAssignmentUnfoldArguments" (formula "7") (term "1")) +(rule "variableDeclarationAssign" (formula "7") (term "1")) +(rule "variableDeclaration" (formula "7") (term "1") (newnames "var")) +(rule "assignmentSubtractionInt" (formula "7") (term "1")) + (builtin "One Step Simplification" (formula "7")) +(rule "translateJavaSubInt" (formula "7") (term "0,1,0")) +(rule "polySimp_elimSub" (formula "7") (term "0,1,0")) +(rule "mul_literals" (formula "7") (term "1,0,1,0")) +(rule "polySimp_addComm0" (formula "7") (term "0,1,0")) + (builtin "Use Operation Contract" (formula "7") (newnames "heapBefore_cycleA,result_88,exc_104,heapAfter_cycleA,anon_heap_cycleA") (contract "Example[Example::cycleA(int)].JML operation contract.0#Example[Example::cycleA(int)].JML operation contract.1") (modality "box")) +(branch "Post (cycleA)" + (builtin "One Step Simplification" (formula "9")) + (builtin "One Step Simplification" (formula "7") (ifInst "" (formula "5")) (ifInst "" (formula "5"))) + (rule "andLeft" (formula "7")) + (rule "andLeft" (formula "8")) + (rule "typeEqDerived" (formula "9") (term "0,1,1,1,1,1") (ifseqformula "8")) + (rule "typeEqDerived" (formula "9") (term "0,0,1,1,1,1") (ifseqformula "8")) + (rule "typeEqDerived" (formula "9") (term "0,1,1,1,1,1,0") (ifseqformula "8")) + (rule "typeEqDerived" (formula "9") (term "0,0,1,1,1,1,0") (ifseqformula "8")) + (builtin "One Step Simplification" (formula "9") (ifInst "" (formula "8")) (ifInst "" (formula "8")) (ifInst "" (formula "8")) (ifInst "" (formula "8"))) + (rule "andLeft" (formula "9")) + (rule "andLeft" (formula "10")) + (rule "replace_known_left" (formula "9") (term "1,1") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "9") (ifInst "" (formula "10"))) + (rule "true_left" (formula "9")) + (rule "assignment" (formula "12") (term "1")) + (builtin "One Step Simplification" (formula "12")) + (rule "blockEmpty" (formula "12") (term "1")) + (rule "inEqSimp_sepPosMonomial1" (formula "9") (term "0")) + (rule "mul_literals" (formula "9") (term "1,0")) + (rule "methodCallReturn" (formula "12") (term "1")) + (rule "assignment" (formula "12") (term "1")) + (builtin "One Step Simplification" (formula "12")) + (rule "methodCallEmpty" (formula "12") (term "1")) + (rule "tryEmpty" (formula "12") (term "1")) + (rule "emptyModality" (formula "12") (term "1")) + (builtin "One Step Simplification" (formula "12") (ifInst "" (formula "9")) (ifInst "" (formula "10"))) + (rule "closeTrue" (formula "12")) +) +(branch "Exceptional Post (cycleA)" + (builtin "One Step Simplification" (formula "7") (ifInst "" (formula "5")) (ifInst "" (formula "5"))) + (builtin "One Step Simplification" (formula "9")) + (rule "andLeft" (formula "7")) + (rule "selectCreatedOfAnonAsFormulaEQ" (formula "8") (term "1,0") (ifseqformula "7")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "9")) + (rule "andLeft" (formula "8")) + (rule "andLeft" (formula "11")) + (rule "notLeft" (formula "8")) + (rule "replace_known_right" (formula "11") (term "0,0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "11")) + (rule "andLeft" (formula "11")) + (rule "replace_known_right" (formula "10") (term "0") (ifseqformula "13")) + (builtin "One Step Simplification" (formula "10") (ifInst "" (formula "11"))) + (rule "true_left" (formula "10")) + (rule "replace_known_left" (formula "9") (term "1,1,0,1") (ifseqformula "10")) + (builtin "One Step Simplification" (formula "9") (ifInst "" (formula "12")) (ifInst "" (formula "12")) (ifInst "" (formula "10")) (ifInst "" (formula "11"))) + (rule "true_left" (formula "9")) + (rule "blockThrow" (formula "13") (term "1")) + (rule "methodCallParamThrow" (formula "13") (term "1")) + (rule "tryCatchThrow" (formula "13") (term "1")) + (rule "ifElseUnfold" (formula "13") (term "1") (inst "#boolv=x")) + (rule "variableDeclaration" (formula "13") (term "1") (newnames "x_1")) + (rule "equality_comparison_simple" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "replace_known_right" (formula "13") (term "0,0,1,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "13")) + (rule "ifElseSplit" (formula "13")) + (branch "if x_1 true" + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch "if x_1 false" + (builtin "One Step Simplification" (formula "14")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "ifElseSplit" (formula "13")) + (branch "if exc_104 instanceof java.lang.Throwable true" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12"))) + (rule "true_left" (formula "1")) + (rule "variableDeclaration" (formula "13") (term "1") (newnames "e")) + (rule "delete_unnecessary_cast" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "14")) + (builtin "One Step Simplification" (formula "1")) + (rule "true_left" (formula "1")) + (rule "assignment" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13")) + (rule "emptyModality" (formula "13") (term "1")) + (builtin "One Step Simplification" (formula "13") (ifInst "" (formula "11")) (ifInst "" (formula "11")) (ifInst "" (formula "9")) (ifInst "" (formula "10"))) + (rule "closeTrue" (formula "13")) + ) + (branch "if exc_104 instanceof java.lang.Throwable false" + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12"))) + (rule "closeFalse" (formula "1")) + ) + ) +) +(branch "Pre (cycleA)" + (builtin "One Step Simplification" (formula "7") (ifInst "" (formula "1")) (ifInst "" (formula "5"))) + (rule "closeTrue" (formula "7")) +) +) +} diff --git a/keyext.proofmanagement/src/test/pmexample2/src/Example.java b/keyext.proofmanagement/src/test/pmexample2/src/Example.java new file mode 100755 index 00000000000..ce1062608e0 --- /dev/null +++ b/keyext.proofmanagement/src/test/pmexample2/src/Example.java @@ -0,0 +1,78 @@ +import java.util.ArrayList; + +class Example { + /*@ ensures param != 7 && param >= 0 ==> \result == 42; + @ diverges param == 7 || param < 1; + @*/ + int root(final int param) { + new java.util.ArrayList(); + return left(param) + right(); + } + + /*@ + @ ensures \result == 21; + @*/ + int right() { + return recursive(42); + } + + /*@ ensures \result == 21; + @ measured_by i; + @*/ + int recursive(final int i) { + if (i <= 0) + return result(); + else + return recursive(i-1); + } + + /*@ + @ ensures \result == 21; + @*/ + int result() { + return 21; + } + + /*@ ensures param != 7 && param >= 0 ==> \result == 21; + @ diverges param == 7 || param < 0; + @*/ + int left(final int param) { + if (param == 7) + block(); + else + return cycleA(param); + } + + /*@ + @ diverges true; + @*/ + void block() { + block(); + } + + /*@ ensures param >= 0 ==> \result == 21; + @ measured_by param; + @ diverges param < 0; + @*/ + int cycleA(final int param) { + if (param == 0 || param == 1) + return leaf(); + else + return cycleB(param-1); + } + + /*@ ensures param > 0 ==> \result == 21; + @ measured_by param; + @ diverges param <= 0; + @*/ + int cycleB(final int param) { + return cycleA(param-1); + } + + /*@ + @ ensures \result == 21; + @*/ + int leaf() { + return 21; + } +}