Merge branch 'proofautomation' of https://github.com/kruegers/FeatureIDE

into proofautomation
kruegers · May 20, 2017 · d942ea5 · d942ea5
2 parents 722e9bf + 57355b7
commit d942ea5
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/...src/de/ovgu/featureide/core/featurehouse/proofautomation/configuration/Configuration.java b/...src/de/ovgu/featureide/core/featurehouse/proofautomation/configuration/Configuration.java
@@ -32,4 +32,5 @@ public class Configuration {
 	public static boolean excludeMain = true; //excludes the proofs of class main
 	public static String excludedClass ="Main";
 	public static boolean excludeFailedProofs = true; //if true the failed Proofs are removed from the total results
+	public static boolean proveDispatcher = false; //if true, the dispatcher Methods are proven else not
 }
diff --git a/...ation/src/de/ovgu/featureide/core/featurehouse/proofautomation/key/AutomatingProject.java b/...ation/src/de/ovgu/featureide/core/featurehouse/proofautomation/key/AutomatingProject.java
@@ -444,7 +444,10 @@ public int compare(KeYJavaType o1, KeYJavaType o2) {
                 ImmutableSet<Contract> contracts = environment.getSpecificationRepository().getContracts(type, target);
                 for (Contract contract : contracts) {
                 	if(!type.getFullName().equals(Configuration.excludedClass)||!Configuration.excludeMain){
-                    proofs.add(new AutomatingProof(type.getFullName(), ClassTree.getDisplayName(environment.getServices(), contract.getTarget()), contract.getDisplayName(), environment, contract));
+                		AutomatingProof a =new AutomatingProof(type.getFullName(), ClassTree.getDisplayName(environment.getServices(), contract.getTarget()), contract.getDisplayName(), environment, contract);
+                		if(!a.getTargetName().contains("dispatch")||Configuration.proveDispatcher){
+                			proofs.add(a);
+                		}
                 	}
                 }
             }
@@ -453,6 +456,9 @@ public int compare(KeYJavaType o1, KeYJavaType o2) {
 
 	}
 
+	private void removeDispatcher(List<AutomatingProof> proofs){
+
+	}