Clean up the Java AST: Avoid sub-classes in favor of Enum

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/impl/InformationFlowContractImpl.java

@@ -11,7 +11,7 @@
 import de.uka.ilkd.key.informationflow.po.InfFlowContractPO;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.ModifierKind;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.op.IObserverFunction;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
@@ -431,7 +431,7 @@ public String getPODisplayName() {
 
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public ModifierKind getVisibility() {
         assert false; // this is currently not applicable for contracts
         return null;
     }

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

@@ -9,7 +9,7 @@
 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.expression.BinaryAssignment;
 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;
@@ -22,6 +22,8 @@
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.Pair;
 
+import static de.uka.ilkd.key.java.ast.expression.BinaryAssignment.BinaryAssignmentKind.COPY;
+
 public class BasicLoopExecutionSnippet extends ReplaceAndRegisterMethod implements FactoryMethod {
 
     @Override
@@ -101,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 BinaryAssignment(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,10 @@
 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.BinaryAssignment;
 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;
@@ -123,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 BinaryAssignment(selfVar, n);
             sb = new StatementBlock(ca);
         } else {
             final MethodBodyStatement call =
@@ -136,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 BinaryAssignment(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 BinaryAssignment(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.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java

@@ -190,7 +190,8 @@ private MethodSpec newRef(final TypeName sort) {
     /**
      * Takes a string representing a type e.g. "java.lang.Object[]" and returns a new name without
      * "." and "[]", e.g. "java_lang_Object_ARRAY_". It is used to create correct setter and getter
-     * method names. This method is also used in Assignment.toString(boolean rfl) to generate the
+     * method names. This method is also used in BinaryAssignment.toString(boolean rfl) to generate
+     * the
      * correct method names.
      */
     public static String cleanTypeName(TypeName s) {

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenFacade.java

@@ -6,6 +6,7 @@
 import java.io.IOException;
 import java.util.Collection;
 import java.util.List;
+import java.util.NoSuchElementException;
 import java.util.concurrent.Callable;
 
 import de.uka.ilkd.key.control.KeYEnvironment;
@@ -66,7 +67,7 @@ public void launcherStopped(SolverLauncher launcher,
 
                     tg.generateJUnitTestSuite(finishedSolvers);
                     reporter.writeln("Compile the generated files using a Java compiler.");
-                } catch (IOException e) {
+                } catch (NoSuchElementException | IOException e) {
                     reporter.reportException(e);
                 }
             }

key.core.wd/src/main/java/de/uka/ilkd/key/wd/BlockWellDefinedness.java

@@ -7,7 +7,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.ModifierKind;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
@@ -109,7 +109,7 @@ public String getTypeName() {
     }
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public ModifierKind getVisibility() {
         return block.getVisibility();
     }
 

key.core.wd/src/main/java/de/uka/ilkd/key/wd/ClassWellDefinedness.java

@@ -7,7 +7,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.ModifierKind;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
@@ -155,7 +155,7 @@ public String getTypeName() {
     }
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public ModifierKind getVisibility() {
         return inv.getVisibility();
     }
 

key.core.wd/src/main/java/de/uka/ilkd/key/wd/LoopWellDefinedness.java

@@ -7,7 +7,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.ModifierKind;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
@@ -99,7 +99,7 @@ public String getTypeName() {
     }
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public ModifierKind getVisibility() {
         return inv.getVisibility();
     }
 

key.core.wd/src/main/java/de/uka/ilkd/key/wd/MethodWellDefinedness.java

@@ -9,7 +9,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.ModifierKind;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
@@ -467,7 +467,7 @@ public String getTypeName() {
     }
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public ModifierKind getVisibility() {
         return contract.getVisibility();
     }
 

key.core.wd/src/main/java/de/uka/ilkd/key/wd/SpecificationRepositoryWD.java

@@ -10,7 +10,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.ModifierKind;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.op.IObserverFunction;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
@@ -363,7 +363,7 @@ public void addClassInvariant(ClassInvariant inv) {
         }
 
         // inherit non-private, non-static invariants
-        if (!inv.isStatic() && VisibilityModifier.allowsInheritance(inv.getVisibility())) {
+        if (!inv.isStatic() && ModifierKind.allowsInheritance(inv.getVisibility())) {
             final ImmutableList<KeYJavaType> subs = services.getJavaInfo().getAllSubtypes(kjt);
             for (KeYJavaType sub : subs) {
                 ClassInvariant subInv = inv.setKJT(sub);

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

@@ -0,0 +1,21 @@
+/* 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;
+
+import de.uka.ilkd.key.java.ast.expression.Assignment;
+import de.uka.ilkd.key.java.ast.expression.BinaryAssignment;
+
+import org.key_project.logic.SyntaxElement;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (13.08.26)
+ */
+public class JavaAstUtils {
+    public static boolean isCopyAssignment(SyntaxElement a) {
+        return a instanceof Assignment b
+                && b.getKind() == BinaryAssignment.BinaryAssignmentKind.COPY;
+    }
+}

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

@@ -9,7 +9,6 @@
 import de.uka.ilkd.key.java.ast.ProgramElement;
 import de.uka.ilkd.key.java.ast.abstraction.*;
 import de.uka.ilkd.key.java.ast.declaration.*;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
 import de.uka.ilkd.key.java.ast.reference.TypeRef;
@@ -35,6 +34,8 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import static de.uka.ilkd.key.java.ast.declaration.ModifierKind.*;
+
 /**
  * an instance serves as representation of a Java model underlying a DL formula. This class provides
  * calls to access the elements of the Java model using the KeY data structures only. Implementation
@@ -481,14 +482,19 @@ public static boolean isVisibleTo(SpecificationElement ax, KeYJavaType visibleTo
         // TODO: package information not yet available
         // BUGFIX: package-private is understood as private (see bug #1268)
         final boolean visibleToPackage = false;
-        final VisibilityModifier visibility = ax.getVisibility();
-        if (VisibilityModifier.isPublic(visibility)) {
+        final ModifierKind visibility = ax.getVisibility();
+        // package private is modelled as null
+        assert visibility == null || visibility.isVisibility();
+
+        if (PUBLIC == visibility) {
             return true;
         }
-        if (VisibilityModifier.allowsInheritance(visibility)) {
+
+        if (ModifierKind.allowsInheritance(visibility)) {
             return visibleTo.getSort().extendsTrans(kjt.getSort()) || visibleToPackage;
         }
-        if (VisibilityModifier.isPackageVisible(visibility)) {
+
+        if (visibility == null || visibility == JML_PACKAGE) {
             return visibleToPackage;
         } else {
             return kjt.equals(visibleTo);

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

@@ -913,7 +913,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;
     }
 
@@ -1005,7 +1005,7 @@ public JavaParserFactory getProgramFactory() {
     }
 
     @NonNull
-    private JavaSymbolSolver getSymbolResolver() {
+    public JavaSymbolSolver getSymbolResolver() {
         return programFactory.getSymbolSolver();
     }