Skip to content

Commit

Permalink
Fixed some smaller issues.
Browse files Browse the repository at this point in the history
  • Loading branch information
@fynndemmler
fynndemmler committed Mar 6, 2024
1 parent c772465 commit 3368f36
Show file tree
Hide file tree
Showing 5 changed files with 84 additions and 37 deletions.
2 changes: 1 addition & 1 deletion de.tu-bs.cs.isf.cbc.mutation/META-INF/MANIFEST.MF
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
25 changes: 17 additions & 8 deletions de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYFileContent.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 = "(?<![a-zA-Z0-9_\\.]|self\\.)(";
public static final String REGEX_AFTER_VARIABLE_KEYWORD = ")(?![a-zA-Z0-9_])";
public static final Pattern REGEX_THIS_KEYWORD = Pattern.compile("(?<![a-zA-Z0-9_])(this)(?![a-zA-Z0-9_])");
public static final Pattern REGEX_THIS_KEYWORD = Pattern.compile("\\b(this)\\b");//("(?<![a-zA-Z0-9_])(this)(?![a-zA-Z0-9_])");
public static final String OLD_VARS_SUFFIX = "_oldVal";
public static final Pattern REGEX_RESULT_KEYWORD = Pattern.compile("(\\\\result)");

Expand Down Expand Up @@ -274,6 +272,7 @@ public String getKeYCImpliesCContent() {
}

public String getKeYContent(boolean withStatement) {
replaceThisForSelfInStatement();
addSelfForFields();

Set<String> oldKeywords = extractOldKeywordVariables();
Expand All @@ -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())));
Expand Down Expand Up @@ -328,15 +330,21 @@ private String getKeyProblem(Map<String, OldReplacement> oldReplacements) {
private String getProgramVariablesString(Map<String, OldReplacement> 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()) {
Expand Down Expand Up @@ -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;
}
Expand Down
35 changes: 32 additions & 3 deletions de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/ProveWithKey.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down Expand Up @@ -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));
Expand Down
1 change: 1 addition & 0 deletions de.tu_bs.cs.isf.cbc.statistics/META-INF/MANIFEST.MF
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
58 changes: 33 additions & 25 deletions ....isf.commands.toolbar/src/de/tu_bs/cs/isf/commands/toolbar/handler/family/MetaMethod.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();

Expand Down

0 comments on commit 3368f36

Please sign in to comment.