make Modifier to an enum

Author: wadoon

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.Modifier;
 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 Modifier.ModifierKind getVisibility() {
         assert false; // this is currently not applicable for contracts
         return null;
     }

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.Modifier;
 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 Modifier.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.Modifier;
 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 Modifier.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.Modifier;
 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 Modifier.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.Modifier;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
@@ -468,7 +468,7 @@ public String getTypeName() {
     }
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public Modifier.ModifierKind getVisibility() {
         return contract.getVisibility();
     }
 

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

@@ -10,7 +10,6 @@
 
 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.logic.JTerm;
 import de.uka.ilkd.key.logic.op.IObserverFunction;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
@@ -363,7 +362,7 @@ public void addClassInvariant(ClassInvariant inv) {
         }
 
         // inherit non-private, non-static invariants
-        if (!inv.isStatic() && VisibilityModifier.allowsInheritance(inv.getVisibility())) {
+        if (!inv.isStatic() && inv.getVisibility().allowsInheritance()) {
             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/JavaInfo.java

@@ -8,7 +8,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.Modifier.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
@@ -377,14 +378,18 @@ 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 Modifier.ModifierKind visibility = ax.getVisibility();
+        assert visibility != null && visibility.isVisibility();
+
+        if (PUBLIC == visibility) {
             return true;
         }
-        if (VisibilityModifier.allowsInheritance(visibility)) {
+
+        if (visibility.allowsInheritance()) {
             return visibleTo.getSort().extendsTrans(kjt.getSort()) || visibleToPackage;
         }
-        if (VisibilityModifier.isPackageVisible(visibility)) {
+
+        if (visibility == PROTECTED || visibility == JML_PACKAGE) {
             return visibleToPackage;
         } else {
             return kjt.equals(visibleTo);

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

@@ -6,17 +6,17 @@
 import java.util.List;
 
 import de.uka.ilkd.key.java.ast.*;
-import de.uka.ilkd.key.java.ast.declaration.modifier.Static;
 import de.uka.ilkd.key.java.visitor.Visitor;
 
 import org.key_project.util.ExtList;
 
+import static de.uka.ilkd.key.java.ast.declaration.Modifier.createModifierList;
+
 
 public class ClassInitializer extends JavaDeclaration
         implements MemberDeclaration, StatementContainer {
 
 
-
     protected final StatementBlock body;
 
 
@@ -26,8 +26,10 @@ public ClassInitializer() {
     }
 
 
-    public ClassInitializer(Static modifier, StatementBlock body) {
-        super(new Modifier[] { modifier });
+    public ClassInitializer(boolean isStatic, StatementBlock body) {
+        super(
+            isStatic ? createModifierList(Modifier.ModifierKind.STATIC)
+                    : createModifierList());
         this.body = body;
     }
 
@@ -40,8 +42,7 @@ public ClassInitializer(Modifier[] modifier, StatementBlock body, PositionInfo p
     /**
      * Class initializer.
      *
-     * @param children
-     *        list with all children. May include: a StatementBlock (taken as body of the
+     * @param children list with all children. May include: a StatementBlock (taken as body of the
      *        ClassInitialiyer), several Modifier (taken as modifiers of the declaration), a Comment
      */
     public ClassInitializer(ExtList children) {
@@ -50,7 +51,6 @@ public ClassInitializer(ExtList children) {
     }
 
 
-
     public StatementBlock getBody() {
         return body;
     }
@@ -92,11 +92,9 @@ public int getChildCount() {
     /**
      * Returns the child at the specified index in this node's "virtual" child array
      *
-     * @param index
-     *        an index into this node's "virtual" child array
+     * @param index an index into this node's "virtual" child array
      * @return the program element at the given position
-     * @exception ArrayIndexOutOfBoundsException
-     *            if <tt>index</tt> is out of bounds
+     * @throws ArrayIndexOutOfBoundsException if <tt>index</tt> is out of bounds
      */
 
     public ProgramElement getChildAt(int index) {
@@ -116,7 +114,9 @@ public ProgramElement getChildAt(int index) {
         throw new ArrayIndexOutOfBoundsException();
     }
 
-    /** A binary class initializer does not occur. */
+    /**
+     * A binary class initializer does not occur.
+     */
 
     public boolean isBinary() {
         return false;
@@ -171,8 +171,7 @@ public SourceElement getLastElement() {
      * calls the corresponding method of a visitor in order to perform some action/transformation on
      * this element
      *
-     * @param v
-     *        the Visitor
+     * @param v the Visitor
      */
     public void visit(Visitor v) {
         v.performActionOnClassInitializer(this);