From 3368f36ca93f88895829d82b517054548daee49a Mon Sep 17 00:00:00 2001 From: Fynn Demmler Date: Wed, 6 Mar 2024 12:25:05 +0100 Subject: [PATCH] Fixed some smaller issues. --- .../META-INF/MANIFEST.MF | 2 +- .../tu_bs/cs/isf/cbc/util/KeYFileContent.java | 25 +++++--- .../tu_bs/cs/isf/cbc/util/ProveWithKey.java | 35 ++++++++++- .../META-INF/MANIFEST.MF | 1 + .../toolbar/handler/family/MetaMethod.java | 58 +++++++++++-------- 5 files changed, 84 insertions(+), 37 deletions(-) diff --git a/de.tu-bs.cs.isf.cbc.mutation/META-INF/MANIFEST.MF b/de.tu-bs.cs.isf.cbc.mutation/META-INF/MANIFEST.MF index b56479baf..7aaea84f6 100644 --- a/de.tu-bs.cs.isf.cbc.mutation/META-INF/MANIFEST.MF +++ b/de.tu-bs.cs.isf.cbc.mutation/META-INF/MANIFEST.MF @@ -9,7 +9,7 @@ Require-Bundle: org.junit, org.eclipse.graphiti.ui;bundle-version="0.18.0", org.eclipse.ui.views.properties.tabbed, org.eclipse.graphiti;bundle-version="0.18.0", - org.apache.commons.io;bundle-version="2.8.0" + org.apache.commons.commons-io Import-Package: de.tu_bs.cs.isf.cbc.cbcclass, de.tu_bs.cs.isf.cbc.cbcmodel, de.tu_bs.cs.isf.cbc.exceptions, diff --git a/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYFileContent.java b/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYFileContent.java index 95021fa12..3268fc65b 100644 --- a/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYFileContent.java +++ b/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYFileContent.java @@ -35,9 +35,7 @@ import de.tu_bs.cs.isf.cbc.cbcmodel.impl.ReturnStatementImpl; public class KeYFileContent { - public static final String REGEX_BEFORE_VARIABLE_KEYWORD = "(? oldKeywords = extractOldKeywordVariables(); @@ -289,11 +288,14 @@ public String getKeYContent(boolean withStatement) { return builder.toString(); } + private void replaceThisForSelfInStatement() { + statement = statement.replaceAll("\\b(this.)\\b", "self."); + } + private void addSelfForFields() { for (Field field : programVariables.getFields()) { if (!nameOfLocalVars.contains(field.getName()) /*&& !field.isIsStatic()*/) { - Pattern pattern = Pattern.compile(REGEX_BEFORE_VARIABLE_KEYWORD + field.getName() + REGEX_AFTER_VARIABLE_KEYWORD); - statement = statement.replaceAll(pattern.pattern(), "self." + field.getName()); + Pattern pattern = Pattern.compile("\\b(this\\." + field.getName() + ")\\b"); preConditions.forEach(c -> c.setName(c.getName().replaceAll(pattern.pattern(), "self." + field.getName()))); postConditions.forEach(c -> c.setName(c.getName().replaceAll(pattern.pattern(), "self." + field.getName()))); globalConditions.forEach(c -> c.setName(c.getName().replaceAll(pattern.pattern(), "self." + field.getName()))); @@ -328,15 +330,21 @@ private String getKeyProblem(Map oldReplacements) { private String getProgramVariablesString(Map oldReplacements) { StringBuilder builder = new StringBuilder(); for (JavaVariable var : programVariables.getVariables()) { - builder.append(removeStaticNonNull(var.getName()) + ";\n"); + if (!builder.toString().contains(var.getName())) { + builder.append(removeStaticNonNull(var.getName()) + ";\n"); + } } for (Parameter param : programVariables.getParams()) { - builder.append(removeStaticNonNull(param.getType() + " " + param.getName()) + ";\n"); + if (!builder.toString().contains(param.getType() + " " + param.getName())) { + builder.append(removeStaticNonNull(param.getType() + " " + param.getName()) + ";\n"); + } } for (String unmodifiableVar : getUnmodifiableProgramVars()) { - builder.append(removeStaticNonNull(unmodifiableVar) + ";\n"); + if (!builder.toString().contains(unmodifiableVar)) { + builder.append(removeStaticNonNull(unmodifiableVar) + ";\n"); + } } // for (String var : oldReplacements.keySet()) { @@ -793,6 +801,7 @@ private static class OldReplacement { private int index; OldReplacement(String var, int index) { + var = var.replaceAll("this\\.", "self."); this.var = var; this.index = index; } diff --git a/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/ProveWithKey.java b/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/ProveWithKey.java index 477bcb584..d284ec825 100644 --- a/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/ProveWithKey.java +++ b/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/ProveWithKey.java @@ -94,7 +94,7 @@ public ProveWithKey(AbstractStatement statement, Diagram diagram, IProgressMonit if (uri.contains(MetaNames.FOLDER_NAME)) { String className = uri.substring(0, uri.lastIndexOf("/")); className = className.substring(className.lastIndexOf("/") + 1, className.length()); - this.sourceFolder = MetaNames.FOLDER_NAME; /*+ "/" + className;*/ + this.sourceFolder = "/" + MetaNames.FOLDER_NAME; /*+ "/" + className;*/ } else { this.sourceFolder = srcFolder; } @@ -607,11 +607,40 @@ private String getMethodName(String uri) { private void addExistingVarsTo(JavaVariables targetVars) { JavaVariables copyVars = EcoreUtil.copy(vars); var callingClass = FeatureUtil.getInstance().getCallingClass(uri); - targetVars.getVariables().addAll(copyVars.getVariables()); - targetVars.getFields().addAll(copyVars.getFields()); + addNewVars(targetVars, copyVars); if (callingClass.isEmpty()) return; targetVars.getParams().addAll(copyMethodParams(uri, getMethodName(uri), callingClass)); } + + private void addNewVars(final JavaVariables target, final JavaVariables source) { + boolean found = false; + for (int i = 0; i < source.getVariables().size(); i++) { + for (int j = 0; j < target.getVariables().size(); j++) { + if (target.getVariables().get(j).getName().equals(source.getVariables().get(i).getName())) { + found = true; + break; + } + } + if (!found) { + target.getVariables().add(source.getVariables().get(i)); + i--; + } + found = false; + } + for (int i = 0; i < source.getFields().size(); i++) { + for (int j = 0; j < target.getFields().size(); j++) { + if (target.getFields().get(j).getName().equals(source.getFields().get(i).getName())) { + found = true; + break; + } + } + if (!found) { + target.getFields().add(source.getFields().get(i)); + i--; + } + found = false; + } + } public File createProveCImpliesCWithKey(String preCondition, String postCondition, boolean override) { KeYFileContent content = new KeYFileContent(fileHandler.getProjectLocation(uri)); diff --git a/de.tu_bs.cs.isf.cbc.statistics/META-INF/MANIFEST.MF b/de.tu_bs.cs.isf.cbc.statistics/META-INF/MANIFEST.MF index 03f5b4f2f..65d94560f 100644 --- a/de.tu_bs.cs.isf.cbc.statistics/META-INF/MANIFEST.MF +++ b/de.tu_bs.cs.isf.cbc.statistics/META-INF/MANIFEST.MF @@ -9,6 +9,7 @@ Bundle-Localization: plugin Automatic-Module-Name: de.tu_bs.cs.isf.cbc.statistics Bundle-RequiredExecutionEnvironment: J2SE-1.5 Require-Bundle: org.eclipse.core.runtime, + org.eclipse.emf.ecore;visibility:=reexport, de.tu-bs.cs.isf.cbc.model, org.eclipse.core.resources, com.google.guava, diff --git a/de.tu_bs.cs.isf.commands.toolbar/src/de/tu_bs/cs/isf/commands/toolbar/handler/family/MetaMethod.java b/de.tu_bs.cs.isf.commands.toolbar/src/de/tu_bs/cs/isf/commands/toolbar/handler/family/MetaMethod.java index f35cb14dd..204fc3f95 100644 --- a/de.tu_bs.cs.isf.commands.toolbar/src/de/tu_bs/cs/isf/commands/toolbar/handler/family/MetaMethod.java +++ b/de.tu_bs.cs.isf.commands.toolbar/src/de/tu_bs/cs/isf/commands/toolbar/handler/family/MetaMethod.java @@ -318,48 +318,56 @@ private void addMethodModifiables(AbstractStatement formulaStatement, JavaVariab } private void addFields(JavaVariables metaJavaVariables) { - metaJavaVariables.getFields().addAll(this.metaClass.getModel().getFields()); + boolean found = false; + for (int i = 0; i < this.metaClass.getModel().getFields().size(); i++) { + for (int j = 0; j < metaJavaVariables.getFields().size(); j++) { + if (metaJavaVariables.getFields().get(j).getName().equals(this.metaClass.getModel().getFields().get(i).getName())) { + found = true; + break; + } + } + if (!found) { + metaJavaVariables.getFields().add(this.metaClass.getModel().getFields().get(i)); + i--; + } + found = false; + } + //metaJavaVariables.getFields().addAll(this.metaClass.getModel().getFields()); } private void addVariables(MethodStruct method, JavaVariables metaJavaVariables) { - for(int j = 0 ; j < method.javaVariables.getVariables().size(); j++) { - boolean alreadyInList = false; - JavaVariable variableToAdd = method.javaVariables.getVariables().get(j); - String variableNameToAdd = variableToAdd.getDisplayedName(); - - for(int k = 0 ; k < metaJavaVariables.getVariables().size(); k++) { - - if(metaJavaVariables.getVariables().get(k).getDisplayedName().equals(variableNameToAdd)) { - alreadyInList = true; + boolean found = false; + for (int i = 0; i < method.javaVariables.getVariables().size(); i++) { + for (int j = 0; j < metaJavaVariables.getVariables().size(); j++) { + if (metaJavaVariables.getVariables().get(j).getName().equals(method.javaVariables.getVariables().get(i).getName())) { + found = true; + break; } } - if(!alreadyInList) { - metaJavaVariables.getVariables().add(CopyCbCFormula.copyJavaVariable(variableToAdd)); + if (!found) { + metaJavaVariables.getVariables().add(CopyCbCFormula.copyJavaVariable(method.javaVariables.getVariables().get(i))); } + found = false; } } private void addParameters(MethodStruct method, JavaVariables metaJavaVariables) throws Exception { var metaMethod = metaClass.getMethod(method.nameOfMethod); - for(int j = 0 ; j < metaMethod.getParameters().size(); j++) { - boolean alreadyInList = false; - Parameter variableToAdd = metaMethod.getParameters().get(j); - String variableNameToAdd = variableToAdd.getName(); - - for(int k = 0 ; k < metaJavaVariables.getVariables().size(); k++) { - if(metaJavaVariables.getVariables().get(k).getDisplayedName().equals(variableNameToAdd)) { - alreadyInList = true; + boolean found = false; + for (int i = 0; i < metaMethod.getParameters().size(); i++) { + for (int j = 0; j < metaJavaVariables.getVariables().size(); j++) { + if (metaJavaVariables.getVariables().get(j).getName().equals(metaMethod.getParameters().get(i).getType() + " " + metaMethod.getParameters().get(i).getName())) { + found = true; + break; } } - if(!alreadyInList) { - metaJavaVariables.getVariables().add(CopyCbCFormula.copyParameter(variableToAdd)); + if (!found) { + metaJavaVariables.getVariables().add(CopyCbCFormula.copyParameter(metaMethod.getParameters().get(i))); } + found = false; } } - - - private GlobalConditions createMetaInvariants() { GlobalConditions globalConditions = CbcmodelFactory.eINSTANCE.createGlobalConditions();