Skip to content

Commit

Permalink
fix merge errors
Browse files Browse the repository at this point in the history
  • Loading branch information
wadoon committed Apr 7, 2024
1 parent 247bd92 commit 39684ce
Show file tree
Hide file tree
Showing 24 changed files with 89 additions and 296 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@

import java.util.Objects;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.ast.PositionInfo;
import de.uka.ilkd.key.java.ast.ProgramElement;
import de.uka.ilkd.key.java.visitor.Visitor;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -514,7 +514,7 @@ public Object visit(EmptyStmt n, Void arg) {
var construct = n.getData(JMLTransformer.KEY_CONSTRUCT);
if (construct instanceof TextualJMLAssertStatement) {
var a = (TextualJMLAssertStatement) construct;
return new JmlAssert(a.getKind(), a.getContext(), pi, services);
return new JmlAssert(a.getKind(), a.getContext(), pi);
}
if (construct instanceof TextualJMLMergePointDecl) {
var a = (TextualJMLMergePointDecl) construct;
Expand Down

This file was deleted.

This file was deleted.

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -12,13 +12,11 @@
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.ast.Label;
import de.uka.ilkd.key.java.ast.ProgramElement;
import de.uka.ilkd.key.java.ast.Statement;
import de.uka.ilkd.key.java.ast.StatementBlock;
import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration;
import de.uka.ilkd.key.java.ast.declaration.VariableSpecification;
import de.uka.ilkd.key.java.ast.statement.JavaStatement;
import de.uka.ilkd.key.java.ast.statement.JmlAssert;
import de.uka.ilkd.key.java.ast.statement.LoopStatement;
import de.uka.ilkd.key.java.ast.statement.MergePointStatement;
import de.uka.ilkd.key.java.ast.statement.*;
import de.uka.ilkd.key.logic.ProgramElementName;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
Expand Down Expand Up @@ -608,44 +606,6 @@ public void performActionOnJmlAssert(final JmlAssert x) {

@Override
public void performActionOnSetStatement(final SetStatement x) {
/*
* var spec =
* Objects.requireNonNull(services.getSpecificationRepository().getStatementSpec(x));
* ProgramVariableCollection vars = spec.vars();
* Map<LocationVariable, Term> atPres = vars.atPres;
* Map<LocationVariable, Term> newAtPres = new LinkedHashMap<>(atPres);
* Map<LocationVariable, LocationVariable> atPreVars = vars.atPreVars;
* Map<LocationVariable, LocationVariable> newAtPreVars = new LinkedHashMap<>(atPreVars);
*
* for (Entry<LocationVariable, Term> e : atPres.entrySet()) {
* LocationVariable pv = e.getKey();
* final Term t = e.getValue();
* if (t == null) {
* continue;
* }
* if (replaceMap.containsKey(pv)) {
* newAtPres.remove(pv);
* pv = (LocationVariable) replaceMap.get(pv);
* newAtPreVars.put(pv, atPreVars.get(e.getKey()));
* }
* newAtPres.put(pv, replaceVariablesInTerm(t));
* }
* final ProgramVariableCollection newVars =
* new ProgramVariableCollection(vars.selfVar, vars.paramVars, vars.resultVar, vars.excVar,
* newAtPreVars, newAtPres, vars.atBeforeVars, vars.atBefores);
*
*
* var newTerms = spec.terms().map(this::replaceVariablesInTerm);
* var newSpec = new SpecificationRepository.JmlStatementSpec(newVars, newTerms);
*
* services.getSpecificationRepository().addStatementSpec(x, newSpec);
*
* /*
* if (!newAtPres.equals(vars.atPres)) {
* changed();
* }
* doDefaultAction(x);
*/
handleJmlStatements(x, SetStatement::new);
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,9 @@
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.ast.ProgramElement;
import de.uka.ilkd.key.java.ast.SourceElement;
import de.uka.ilkd.key.java.ast.Statement;
import de.uka.ilkd.key.java.ast.statement.JmlAssert;
import de.uka.ilkd.key.java.ast.statement.SetStatement;
import de.uka.ilkd.key.ldt.HeapLDT;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.LocationVariable;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@
import de.uka.ilkd.key.java.ast.expression.operator.adt.*;
import de.uka.ilkd.key.java.ast.reference.*;
import de.uka.ilkd.key.java.ast.statement.*;
import de.uka.ilkd.key.java.statement.SetStatement;
import de.uka.ilkd.key.logic.ProgramElementName;
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.logic.op.IProgramVariable;
Expand Down Expand Up @@ -81,7 +80,7 @@ public interface Visitor {

void performActionOnSeqReverse(SeqReverse x);

//void performActionOnSeqPut(SeqPut seqPut);
void performActionOnSeqPut(SeqPut seqPut);

void performActionOnDLEmbeddedExpression(DLEmbeddedExpression x);

Expand Down Expand Up @@ -185,7 +184,7 @@ public interface Visitor {

void performActionOnCopyAssignment(CopyAssignment x);

//void performActionOnSetStatement(SetStatement x);
void performActionOnSetStatement(SetStatement x);

void performActionOnDivideAssignment(DivideAssignment x);

Expand Down
3 changes: 1 addition & 2 deletions key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,14 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.ldt;

import de.uka.ilkd.key.java.Expression;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.ast.abstraction.Type;
import de.uka.ilkd.key.java.ast.expression.Expression;
import de.uka.ilkd.key.java.ast.expression.Operator;
import de.uka.ilkd.key.java.ast.expression.literal.EmptySeqLiteral;
import de.uka.ilkd.key.java.ast.expression.literal.Literal;
import de.uka.ilkd.key.java.ast.expression.operator.adt.*;
import de.uka.ilkd.key.java.expression.operator.adt.SeqPut;
import de.uka.ilkd.key.java.ast.expression.operator.adt.SeqPut;
import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermServices;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.logic;

import de.uka.ilkd.key.java.NameAbstractionTable;
import de.uka.ilkd.key.java.ast.JavaProgramElement;
import de.uka.ilkd.key.java.ast.StatementBlock;
import de.uka.ilkd.key.pp.PrettyPrinter;
Expand Down
2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@

import java.util.concurrent.atomic.AtomicInteger;

import de.uka.ilkd.key.java.PositionInfo;
import de.uka.ilkd.key.java.ast.PositionInfo;
import de.uka.ilkd.key.logic.equality.TermProperty;
import de.uka.ilkd.key.logic.label.TermLabel;
import de.uka.ilkd.key.logic.op.*;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.logic.equality;

import de.uka.ilkd.key.java.JavaProgramElement;
import de.uka.ilkd.key.java.NameAbstractionTable;
import de.uka.ilkd.key.java.ast.JavaProgramElement;
import de.uka.ilkd.key.logic.JavaBlock;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.*;
Expand Down
Loading

0 comments on commit 39684ce

Please sign in to comment.