fix CreatingASTVisitor

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/Modifier.java

@@ -6,14 +6,13 @@
 import java.util.List;
 
 import de.uka.ilkd.key.java.ast.*;
-import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator;
 import de.uka.ilkd.key.java.visitor.Visitor;
-
 import de.uka.ilkd.key.rule.MatchConditions;
-import org.jspecify.annotations.Nullable;
+
 import org.key_project.logic.SyntaxElement;
 
 import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
 
 /**
  *
@@ -56,7 +55,7 @@ public void visit(Visitor v) {
     @Override
     public @Nullable MatchConditions match(SourceData source, MatchConditions matchCond) {
         final ProgramElement src = source.getSource();
-        if(src instanceof Modifier other) {
+        if (src instanceof Modifier other) {
             if (this.keyword.equals(other.getKind())) {
                 return super.match(source, matchCond);
             }

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/Assignment.java

@@ -13,16 +13,15 @@
 import de.uka.ilkd.key.java.ast.SourceData;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.ast.expression.literal.BooleanLiteral;
-import de.uka.ilkd.key.java.ast.expression.operator.LogicFunctionalOperator;
 import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
 import de.uka.ilkd.key.java.visitor.Visitor;
-
 import de.uka.ilkd.key.rule.MatchConditions;
-import org.jspecify.annotations.Nullable;
+
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 
 import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
 
 import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.COPY;
 
@@ -32,6 +31,11 @@
  */
 @NullMarked
 public final class Assignment extends Operator implements ExpressionStatement {
+    public Assignment(AssignmentKind kind, ExtList changeList) {
+        super(changeList);
+        this.kind = kind;
+    }
+
     @Override
     public void visit(Visitor v) {
         v.performActionOnAssignment(this);
@@ -109,7 +113,7 @@ public boolean isLeftAssociative() {
     @Override
     public @Nullable MatchConditions match(SourceData source, MatchConditions matchCond) {
         final ProgramElement src = source.getSource();
-        if(src instanceof Assignment other) {
+        if (src instanceof Assignment other) {
             if (getKind().equals(other.getKind())) {
                 return super.match(source, matchCond);
             }

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java

@@ -17,8 +17,8 @@
 import de.uka.ilkd.key.java.ast.expression.Operator;
 import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
 import de.uka.ilkd.key.java.visitor.Visitor;
-
 import de.uka.ilkd.key.rule.MatchConditions;
+
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 
@@ -79,8 +79,8 @@ public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
 
     @Override
     public MatchConditions match(SourceData source, MatchConditions matchCond) {
-        final ProgramElement src = source.getSource(); // [ left, right ]
-        if(src instanceof BinaryOperator other) {
+        final ProgramElement src = source.getSource();
+        if (src instanceof BinaryOperator other) {
             if (this.kind.equals(other.getKind())) {
                 return super.match(source, matchCond);
             }

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperatorKind.java

@@ -1,3 +1,6 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java.ast.expression.operator;
 
 /**

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/LogicFunctionalOperator.java

@@ -18,11 +18,13 @@
 import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.pp.PrettyPrinter;
-
 import de.uka.ilkd.key.rule.MatchConditions;
-import org.jspecify.annotations.Nullable;
+
+import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 
+import org.jspecify.annotations.Nullable;
+
 import static de.uka.ilkd.key.pp.PrettyPrinter.*;
 
 /**
@@ -49,6 +51,11 @@ public LogicFunctionalOperator(PositionInfo pi, List<Comment> c, LogicFunction f
         this.function = fn;
     }
 
+    public LogicFunctionalOperator(LogicFunction function, ExtList changeList) {
+        super(changeList);
+        this.function = function;
+    }
+
 
     public enum LogicFunction {
         Intersect(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\intersect")),
@@ -109,7 +116,7 @@ public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
     @Override
     public @Nullable MatchConditions match(SourceData source, MatchConditions matchCond) {
         final ProgramElement src = source.getSource();
-        if(src instanceof LogicFunctionalOperator other) {
+        if (src instanceof LogicFunctionalOperator other) {
             if (getFunction().equals(other.getFunction())) {
                 return super.match(source, matchCond);
             }

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/UnaryOperator.java

@@ -16,6 +16,7 @@
 import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.rule.MatchConditions;
+import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 
 import java.util.List;
@@ -39,6 +40,16 @@ public UnaryOperator(PositionInfo pi, List<Comment> c, UnaryOperatorKind op, Exp
         this.kind = op;
     }
 
+    public UnaryOperator(ExtList changeList) {
+        super(changeList);
+        kind = changeList.get(UnaryOperatorKind.class);
+    }
+
+    public UnaryOperator(UnaryOperatorKind kind, ExtList changeList) {
+        super(changeList);
+        this.kind = kind;
+    }
+
     public UnaryOperatorKind getKind() {
         return kind;
     }
@@ -77,10 +88,8 @@ public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
         try {
             return switch (kind) {
                 case POST_DECREMENT, POST_INCREMENT,
-                     PRE_DECREMENT, PRE_INCREMENT ->
-                        tc.getKeYJavaType((Expression) getChildAt(0), ec);
-                default ->
-                        tc.getPromotedType(tc.getKeYJavaType((Expression) getChildAt(0), ec));
+                     PRE_DECREMENT, PRE_INCREMENT -> tc.getKeYJavaType((Expression) getChildAt(0), ec);
+                default -> tc.getPromotedType(tc.getKeYJavaType((Expression) getChildAt(0), ec));
             };
         } catch (Exception e) {
             throw new RuntimeException("Type promotion failed (see below). Operator was " + this,

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/UnaryOperatorKind.java

@@ -1,3 +1,6 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java.ast.expression.operator;
 
 import de.uka.ilkd.key.java.ast.expression.Operator;

key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java

@@ -964,22 +964,45 @@ ProgramElement createNewElement(ExtList changeList) {
 
     @Override
     public void performActionOnBinaryOperator(BinaryOperator x) {
-        super.performActionOnBinaryOperator(x);
+        DefaultAction def = new DefaultAction(x) {
+            @Override
+            ProgramElement createNewElement(ExtList changeList) {
+                return new BinaryOperator(x.getKind(), changeList);
+            }
+        };
+        def.doAction(x);
     }
 
     @Override
     public void performActionOnUnaryOperator(UnaryOperator x) {
-        super.performActionOnUnaryOperator(x);
+        DefaultAction def = new DefaultAction(x) {
+            @Override
+            ProgramElement createNewElement(ExtList changeList) {
+                return new UnaryOperator(x.kind, changeList);
+            }
+        };
+        def.doAction(x);
     }
 
     @Override
     public void performActionOnLogicFunctionalOperator(LogicFunctionalOperator x) {
-        super.performActionOnLogicFunctionalOperator(x);
-    }
+        DefaultAction def = new DefaultAction(x) {
+            @Override
+            ProgramElement createNewElement(ExtList changeList) {
+                return new LogicFunctionalOperator(x.getFunction(), changeList);
+            }
+        };
+        def.doAction(x);    }
 
     @Override
     public void performActionOnAssignment(Assignment x) {
-        super.performActionOnAssignment(x);
+        DefaultAction def = new DefaultAction(x) {
+            @Override
+            ProgramElement createNewElement(ExtList changeList) {
+                return new Assignment(x.getKind(), changeList);
+            }
+        };
+        def.doAction(x);
     }
 
     @Override