From 2e11a0bc9ceeee0b2014dd3c08f9f8dc53019888 Mon Sep 17 00:00:00 2001
From: Timm Reinstorf <timm.reinstorf@andrena.de>
Date: Mon, 20 Nov 2017 15:28:28 +0100
Subject: [PATCH] fixes #54: allow a precondition in sub-contracts if no
 precondition is given in super-contract and default-precondition
 configuration is undefined

---
 ...ndefinedInExternalContractsSystemTest.java | 42 +++++++++++++++++++
 .../src/test/resources/c4j-local.xml          |  4 ++
 .../editor/ContractMethodConditionEditor.java | 23 ++++++++--
 3 files changed, 66 insertions(+), 3 deletions(-)
 create mode 100644 c4j-systemtest/src/test/java/de/vksi/c4j/systemtest/config/defaultpreconditionundefinedexternalclass/DefaultPreConditionShouldBeUndefinedInExternalContractsSystemTest.java

diff --git a/c4j-systemtest/src/test/java/de/vksi/c4j/systemtest/config/defaultpreconditionundefinedexternalclass/DefaultPreConditionShouldBeUndefinedInExternalContractsSystemTest.java b/c4j-systemtest/src/test/java/de/vksi/c4j/systemtest/config/defaultpreconditionundefinedexternalclass/DefaultPreConditionShouldBeUndefinedInExternalContractsSystemTest.java
new file mode 100644
index 0000000..2c4ca01
--- /dev/null
+++ b/c4j-systemtest/src/test/java/de/vksi/c4j/systemtest/config/defaultpreconditionundefinedexternalclass/DefaultPreConditionShouldBeUndefinedInExternalContractsSystemTest.java
@@ -0,0 +1,42 @@
+package de.vksi.c4j.systemtest.config.defaultpreconditionundefinedexternalclass;
+
+import static de.vksi.c4j.Condition.preCondition;
+
+import org.junit.Rule;
+import org.junit.Test;
+
+import de.vksi.c4j.Contract;
+import de.vksi.c4j.systemtest.TransformerAwareRule;
+
+public class DefaultPreConditionShouldBeUndefinedInExternalContractsSystemTest {
+	@Rule
+	public TransformerAwareRule transformerAwareRule = new TransformerAwareRule();
+
+	@Test(expected = AssertionError.class)
+	public void testPreConditionUndefinedWithExternalContract() {
+		new TargetClass().method(-1);
+	}
+
+	private static class TargetClass extends SuperClass {
+	}
+
+	@Contract(forTarget = TargetClass.class)
+	private static class ContractClass extends TargetClass {
+		public void method(int arg) {
+			if (preCondition()) {
+				assert arg > 0;
+			}
+		}
+	}
+
+	@Contract(forTarget = SuperClass.class)
+	private static class SuperContractClass extends SuperClass {
+		public void method(int arg) {
+		}
+	}
+	
+	private static class SuperClass {
+		public void method(int arg) {
+		}
+	}
+}
diff --git a/c4j-systemtest/src/test/resources/c4j-local.xml b/c4j-systemtest/src/test/resources/c4j-local.xml
index e57172b..7775d59 100644
--- a/c4j-systemtest/src/test/resources/c4j-local.xml
+++ b/c4j-systemtest/src/test/resources/c4j-local.xml
@@ -31,6 +31,10 @@
 		<root-package>de.vksi.c4j.systemtest.config.contractsdirectoryasjarfile</root-package>
 		<contract-scan-package>de.vksi.c4j.systemtest.config.contractsdirectoryasjarfile</contract-scan-package>
 	</configuration>
+	<configuration>
+		<root-package>de.vksi.c4j.systemtest.config.defaultpreconditionundefinedexternalclass</root-package>
+		<contract-scan-package>de.vksi.c4j.systemtest.config.defaultpreconditionundefinedexternalclass</contract-scan-package>
+	</configuration>
 	<configuration>
 		<root-package>singlepackage</root-package>
 		<pure-validate>true</pure-validate>
diff --git a/c4j/src/main/java/de/vksi/c4j/internal/transformer/editor/ContractMethodConditionEditor.java b/c4j/src/main/java/de/vksi/c4j/internal/transformer/editor/ContractMethodConditionEditor.java
index f4b40f2..60762e3 100644
--- a/c4j/src/main/java/de/vksi/c4j/internal/transformer/editor/ContractMethodConditionEditor.java
+++ b/c4j/src/main/java/de/vksi/c4j/internal/transformer/editor/ContractMethodConditionEditor.java
@@ -2,10 +2,14 @@
 
 import static de.vksi.c4j.internal.classfile.ClassAnalyzer.getDeclaredMethod;
 import static de.vksi.c4j.internal.classfile.ClassAnalyzer.getField;
+
+import java.util.Set;
+
 import javassist.CannotCompileException;
 import javassist.CtBehavior;
 import javassist.CtClass;
 import javassist.CtField;
+import javassist.CtMethod;
 import javassist.NotFoundException;
 import javassist.expr.FieldAccess;
 import javassist.expr.MethodCall;
@@ -20,6 +24,7 @@
 import de.vksi.c4j.internal.configuration.DefaultPreconditionType;
 import de.vksi.c4j.internal.configuration.XmlConfigurationManager;
 import de.vksi.c4j.internal.contracts.ContractInfo;
+import de.vksi.c4j.internal.contracts.ContractMethod;
 import de.vksi.c4j.internal.contracts.ContractRegistry;
 import de.vksi.c4j.internal.contracts.InvolvedTypeInspector;
 import de.vksi.c4j.internal.types.ListOrderedSet;
@@ -112,9 +117,21 @@ private void handleUndefinedDefaultPreCondition(MethodCall methodCall, CtBehavio
 				getContract().getTargetClass());
 		contracts.remove(getContract());
 		for (ContractInfo otherContract : contracts) {
-			if (getDeclaredMethod(otherContract.getTargetClass(), method.getName(), method.getParameterTypes()) != null) {
-				preConditionStrengthening(methodCall, method, otherContract.getContractClass());
-				return;
+			CtMethod otherMethod = getDeclaredMethod(otherContract.getTargetClass(), method.getName(), method.getParameterTypes());
+			if (otherMethod != null) {
+				boolean superPreconditionDefined = false;
+				Set<ContractMethod> methods = otherContract.getMethods();
+				for (ContractMethod otherContractMethod : methods) {
+					if (otherContractMethod.getMethod().equals(otherMethod)) {
+						if (otherContractMethod.hasPreConditionOrDependencies()) {
+							superPreconditionDefined = true;
+						}
+					}
+				}
+				if (superPreconditionDefined) {
+					preConditionStrengthening(methodCall, method, otherContract.getContractClass());
+					return;
+				}
 			}
 		}
 		preConditionAvailable = true;