make Operators to enum

Author: wadoon

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicLoopExecutionSnippet.java

@@ -9,7 +9,6 @@
 import de.uka.ilkd.key.java.ast.Statement;
 import de.uka.ilkd.key.java.ast.StatementBlock;
 import de.uka.ilkd.key.java.ast.expression.Assignment;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
 import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
 import de.uka.ilkd.key.java.ast.statement.MethodFrame;
 import de.uka.ilkd.key.logic.JTerm;
@@ -23,6 +22,8 @@
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.Pair;
 
+import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.Copy;
+
 public class BasicLoopExecutionSnippet extends ReplaceAndRegisterMethod implements FactoryMethod {
 
     @Override
@@ -102,8 +103,9 @@ private Pair<JavaBlock, JavaBlock> buildJavaBlock(BasicSnippetData d) {
         LoopSpecification inv = (LoopSpecification) d.get(BasicSnippetData.Key.LOOP_INVARIANT);
         StatementBlock sb = (StatementBlock) inv.getLoop().getBody();
 
-        final Assignment guardVarDecl = new CopyAssignment((LocationVariable) d.origVars.guard.op(),
-            inv.getLoop().getGuardExpression());
+        final Assignment guardVarDecl =
+            new Assignment(Copy, (LocationVariable) d.origVars.guard.op(),
+                inv.getLoop().getGuardExpression());
         final Statement guardVarMethodFrame = context == null ? guardVarDecl
                 : new MethodFrame(null, context, new StatementBlock(guardVarDecl));
 

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSymbolicExecutionSnippet.java

@@ -12,9 +12,9 @@
 import de.uka.ilkd.key.java.ast.declaration.Modifier;
 import de.uka.ilkd.key.java.ast.declaration.ParameterDeclaration;
 import de.uka.ilkd.key.java.ast.declaration.VariableSpecification;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.ast.expression.literal.NullLiteral;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
 import de.uka.ilkd.key.java.ast.expression.operator.New;
 import de.uka.ilkd.key.java.ast.reference.TypeRef;
 import de.uka.ilkd.key.java.ast.reference.TypeReference;
@@ -124,7 +124,7 @@ private JavaBlock buildJavaBlock(BasicSnippetData d, ImmutableList<JTerm> formal
                 formalArray.toArray(new Expression[formalArray.size()]);
             KeYJavaType forClass = (KeYJavaType) d.get(BasicSnippetData.Key.FOR_CLASS);
             final New n = new New(formalArray2, new TypeRef(forClass), null);
-            final CopyAssignment ca = new CopyAssignment(selfVar, n);
+            final Assignment ca = new Assignment(selfVar, n);
             sb = new StatementBlock(ca);
         } else {
             final MethodBodyStatement call =
@@ -137,19 +137,17 @@ private JavaBlock buildJavaBlock(BasicSnippetData d, ImmutableList<JTerm> formal
         final TypeReference excTypeRef = javaInfo.createTypeReference(eType);
 
         // create try statement
-        final CopyAssignment nullStat = new CopyAssignment(exceptionVar, NullLiteral.NULL);
+        final Assignment nullStat = new Assignment(exceptionVar, NullLiteral.NULL);
         final VariableSpecification eSpec = new VariableSpecification(eVar);
         final ParameterDeclaration excDecl =
             new ParameterDeclaration(new Modifier[0], excTypeRef, eSpec, false);
-        final CopyAssignment assignStat = new CopyAssignment(exceptionVar, eVar);
+        final Assignment assignStat = new Assignment(exceptionVar, eVar);
         final Catch catchStat = new Catch(excDecl, new StatementBlock(assignStat));
         final Try tryStat = new Try(sb, new Branch[] { catchStat });
         final StatementBlock sb2 = new StatementBlock(nullStat, tryStat);
 
         // create java block
-        JavaBlock result = JavaBlock.createJavaBlock(sb2);
-
-        return result;
+        return JavaBlock.createJavaBlock(sb2);
     }
 
 

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java

@@ -9,7 +9,7 @@
 import de.uka.ilkd.key.java.ast.ExpressionContainer;
 import de.uka.ilkd.key.java.ast.ProgramElement;
 import de.uka.ilkd.key.java.ast.SourceElement;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.reference.FieldReference;
 import de.uka.ilkd.key.java.ast.reference.ReferencePrefix;
 import de.uka.ilkd.key.java.ast.statement.If;
@@ -20,6 +20,8 @@
 import de.uka.ilkd.key.proof_references.reference.DefaultProofReference;
 import de.uka.ilkd.key.proof_references.reference.IProofReference;
 
+import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.Copy;
+
 /**
  * Extracts read and write access to fields ({@link IProgramVariable}) via assignments.
  *
@@ -33,9 +35,9 @@ public class ProgramVariableReferencesAnalyst implements IProofReferencesAnalyst
     public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
         if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) {
             SourceElement statement = node.getNodeInfo().getActiveStatement();
-            if (statement instanceof CopyAssignment) {
+            if (statement instanceof Assignment a && a.getKind() == Copy) {
                 LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
-                listReferences(node, (CopyAssignment) statement,
+                listReferences(node, a,
                     services.getJavaInfo().getArrayLength(), result, true);
                 return result;
             } else if (statement instanceof If) {
@@ -66,7 +68,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
             if (pv.isMember()) {
                 DefaultProofReference<ProgramVariable> reference =
                     new DefaultProofReference<>(IProofReference.ACCESS, node,
-                        (ProgramVariable) pe);
+                        pv);
                 ProofReferenceUtil.merge(toFill, reference);
             }
         } else if (pe instanceof FieldReference fr) {

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java

@@ -11,7 +11,7 @@
 import de.uka.ilkd.key.java.ast.ProgramElement;
 import de.uka.ilkd.key.java.ast.SourceElement;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.statement.MethodFrame;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
@@ -305,7 +305,7 @@ protected static LocationVariable extractResultVariableFromPostBranch(Node node,
         postModality = TermBuilder.goBelowUpdates(postModality);
         MethodFrame mf = JavaTools.getInnermostMethodFrame(postModality.javaBlock(), services);
         SourceElement firstElement = NodeInfo.computeActiveStatement(mf.getFirstElement());
-        if (!(firstElement instanceof CopyAssignment assignment)) {
+        if (!(firstElement instanceof Assignment assignment)) {
             return null;
         }
         ProgramElement rightChild = assignment.getChildAt(1);

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java

@@ -14,8 +14,8 @@
 import de.uka.ilkd.key.java.ast.NonTerminalProgramElement;
 import de.uka.ilkd.key.java.ast.ProgramElement;
 import de.uka.ilkd.key.java.ast.SourceElement;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.expression.Expression;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
 import de.uka.ilkd.key.java.ast.reference.ReferencePrefix;
 import de.uka.ilkd.key.java.ast.reference.ThisReference;
 import de.uka.ilkd.key.proof.Node;
@@ -64,9 +64,8 @@ public ImmutableArray<Node> doSlicing(Node seedNode, Location seedLocation,
                     if (oldAliases != null) {
                         try {
                             // Update relevant locations if required
-                            if (activeStatement instanceof CopyAssignment) {
-                                SourceElement originalTarget =
-                                    ((CopyAssignment) activeStatement).getArguments().get(0);
+                            if (activeStatement instanceof Assignment a) {
+                                SourceElement originalTarget = a.getArguments().get(0);
                                 ReferencePrefix relevantTarget = toReferencePrefix(originalTarget);
                                 Location normalizedPrefix =
                                     normalizeAlias(services, relevantTarget, info);

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/ThinBackwardSlicer.java

@@ -9,8 +9,8 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.SourceElement;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.expression.Expression;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
 import de.uka.ilkd.key.java.ast.reference.ReferencePrefix;
 import de.uka.ilkd.key.java.ast.statement.MethodBodyStatement;
 import de.uka.ilkd.key.logic.JTerm;
@@ -38,7 +38,7 @@ protected boolean accept(Node node, Node previousChild, Services services,
             throws ProofInputException {
         try {
             boolean accept = false;
-            if (activeStatement instanceof CopyAssignment copyAssignment) {
+            if (activeStatement instanceof Assignment copyAssignment) {
                 ImmutableArray<Expression> arguments = copyAssignment.getArguments();
                 if (arguments.size() >= 1) {
                     SourceElement originalTarget = arguments.get(0);

key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java

@@ -794,7 +794,7 @@ public JavaBlock readBlock(String block, JPContext context,
         }
         var f = JavaBlock
                 .createJavaBlock((StatementBlock) getConverter(allowSchemaJava).process(sb));
-        JavaLogger.print(block, f);
+        // JavaLogger.print(block, f);
         return f;
     }