Fix more position issues

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

@@ -148,7 +148,7 @@ public Position getEndPosition() {
      *
      * @return the relative position of the primary token.
      */
-    public Position getRelativePosition() {
+    public recoder.java.SourceElement.Position getRelativePosition() {
         return posInfo.getRelativePosition();
     }
 

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

@@ -21,6 +21,6 @@ public interface Label extends TerminalProgramElement {
 
     Position getEndPosition();
 
-    Position getRelativePosition();
+    recoder.java.SourceElement.Position getRelativePosition();
 
 }

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

@@ -69,15 +69,6 @@ public static Position fromToken(Token token) {
         return newOneZeroBased(token.getLine(), token.getCharPositionInLine());
     }
 
-    /**
-     * Creates a new location from a token.
-     *
-     * @param token the token
-     */
-    public static Position fromToken(org.antlr.runtime.Token token) {
-        return newOneZeroBased(token.getLine(), token.getCharPositionInLine());
-    }
-
     /**
      * Creates a new location from a token.
      *
@@ -88,7 +79,11 @@ public static Position fromToken(de.uka.ilkd.key.parser.proofjava.Token token) {
     }
 
     public static Position fromPosition(SourceElement.Position pos) {
-        return newOneZeroBased(pos.getLine(), pos.getColumn());
+        if (pos == SourceElement.Position.UNDEFINED) {
+            return UNDEFINED;
+        } else {
+            return new Position(pos.getLine(), pos.getColumn() + 1);
+        }
     }
 
     /**
@@ -173,7 +168,7 @@ public boolean isNegative() {
      */
     public String toString() {
         if (this != UNDEFINED) {
-            return String.valueOf(line) + '/' + (column - 1);
+            return String.valueOf(line) + '/' + column;
         } else {
             return "??/??";
         }

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

@@ -1,5 +1,7 @@
 package de.uka.ilkd.key.java;
 
+import recoder.java.SourceElement;
+
 import java.net.URI;
 import java.nio.file.Paths;
 
@@ -18,7 +20,7 @@ public class PositionInfo {
     /**
      * TODO: What is the purpose of this? To which position is this one relative?
      */
-    private final Position relPos;
+    private final SourceElement.Position relPos;
 
     /** The start position. */
     private final Position startPos;
@@ -39,7 +41,7 @@ public class PositionInfo {
     private URI parentClassURI;
 
     private PositionInfo() {
-        this.relPos = Position.UNDEFINED;
+        this.relPos = SourceElement.Position.UNDEFINED;
         this.startPos = Position.UNDEFINED;
         this.endPos = Position.UNDEFINED;
         fileURI = UNKNOWN_URI;
@@ -52,7 +54,7 @@ private PositionInfo() {
      * @param startPos the start position
      * @param endPos the end position
      */
-    public PositionInfo(Position relPos, Position startPos, Position endPos) {
+    public PositionInfo(SourceElement.Position relPos, Position startPos, Position endPos) {
         this.relPos = relPos;
         this.startPos = startPos;
         this.endPos = endPos;
@@ -67,7 +69,8 @@ public PositionInfo(Position relPos, Position startPos, Position endPos) {
      * @param endPos the end position
      * @param fileURI the resource the PositionInfo refers to
      */
-    public PositionInfo(Position relPos, Position startPos, Position endPos, URI fileURI) {
+    public PositionInfo(SourceElement.Position relPos, Position startPos, Position endPos,
+            URI fileURI) {
         this.relPos = relPos;
         this.startPos = startPos;
         this.endPos = endPos;
@@ -127,7 +130,7 @@ public URI getURI() {
         return fileURI;
     }
 
-    public Position getRelativePosition() {
+    public SourceElement.Position getRelativePosition() {
         return relPos;
     }
 
@@ -141,7 +144,7 @@ public Position getEndPosition() {
 
     /**
      * Creates a new PositionInfo from joining the intervals of the given PositionInfos. The file
-     * informations have to match, otherwise null is returned.
+     * information have to match, otherwise null is returned.
      *
      * @param p1 the first PositionInfo
      * @param p2 the second PositionInfo
@@ -180,7 +183,7 @@ public static PositionInfo join(PositionInfo p1, PositionInfo p2) {
             end = p2.endPos;
         }
         // TODO: join relative position as well
-        return new PositionInfo(Position.UNDEFINED, start, end, p1.getURI());
+        return new PositionInfo(SourceElement.Position.UNDEFINED, start, end, p1.getURI());
     }
 
     /**

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

@@ -385,14 +385,13 @@ private ExtList collectChildrenAndComments(recoder.java.ProgramElement pe) {
      * @return the newly created PositionInfo
      */
     private PositionInfo positionInfo(recoder.java.SourceElement se) {
-        Position relPos = Position.fromPosition(se.getRelativePosition());
-        Position startPos = Position.fromPosition(se.getStartPosition());
-        Position endPos = Position.fromPosition(se.getEndPosition());
+        var relPos = se.getRelativePosition();
+        var startPos = Position.fromPosition(se.getStartPosition());
+        var endPos = Position.fromPosition(se.getEndPosition());
         if ((!inLoopInit))
             return new PositionInfo(relPos, startPos, endPos, currentClassURI);
         else
             return new PositionInfo(relPos, startPos, endPos);
-
     }
 
     /**

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

@@ -66,7 +66,7 @@ public interface SourceElement extends SVSubstitute {
      *
      * @return the relative position of the primary token.
      */
-    Position getRelativePosition();
+    recoder.java.SourceElement.Position getRelativePosition();
 
     /** complete position information */
     PositionInfo getPositionInfo();

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java

@@ -334,7 +334,8 @@ private void transformMethodDecl(TextualJMLMethodDecl decl, Comment[] originalCo
         assert originalComments.length > 0;
 
         // prepend Java modifiers
-        PositionedString declWithMods = new PositionedString(decl.getParsableDeclaration());
+        PositionedString declWithMods = new PositionedString(decl.getParsableDeclaration(),
+            decl.getSourceFileName(), decl.getApproxPosition());
 
         // only handle model methods
         if (!decl.getMods().contains(JMLModifier.MODEL)) {
@@ -350,7 +351,9 @@ private void transformMethodDecl(TextualJMLMethodDecl decl, Comment[] originalCo
         MethodDeclaration methodDecl;
         try {
             methodDecl = services.getProgramFactory().parseMethodDeclaration(declWithMods.text);
-            updatePositionInformation(methodDecl, declWithMods.pos);
+            if (declWithMods.pos != de.uka.ilkd.key.java.Position.UNDEFINED) {
+                updatePositionInformation(methodDecl, declWithMods.pos);
+            }
             attach(methodDecl, astParent, 0); // about the 0 see the comment in
             // transformFieldDecl() above
         } catch (Throwable e) {

key.core/src/main/java/de/uka/ilkd/key/logic/ProgramElementName.java

@@ -149,8 +149,8 @@ public Position getEndPosition() {
      *
      * @return the relative position of the primary token.
      */
-    public Position getRelativePosition() {
-        return Position.UNDEFINED;
+    public recoder.java.SourceElement.Position getRelativePosition() {
+        return recoder.java.SourceElement.Position.UNDEFINED;
     }
 
 

key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java

@@ -190,7 +190,7 @@ public Position getEndPosition() {
      * @return the relative position of the primary token.
      */
     @Override
-    public Position getRelativePosition() {
+    public recoder.java.SourceElement.Position getRelativePosition() {
         return pi.getRelativePosition();
     }
 

key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java

@@ -112,8 +112,8 @@ public Position getEndPosition() {
     }
 
     @Override
-    public Position getRelativePosition() {
-        return Position.UNDEFINED;
+    public recoder.java.SourceElement.Position getRelativePosition() {
+        return recoder.java.SourceElement.Position.UNDEFINED;
     }
 
     @Override

key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java

@@ -184,8 +184,8 @@ public Position getEndPosition() {
 
 
     @Override
-    public Position getRelativePosition() {
-        return Position.UNDEFINED;
+    public recoder.java.SourceElement.Position getRelativePosition() {
+        return recoder.java.SourceElement.Position.UNDEFINED;
     }
 
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java

@@ -402,9 +402,7 @@ public void close() {
      */
     protected List<PositionedString> getPositionedStrings(List<BuildingIssue> issues) {
         return issues.stream().map(w -> new PositionedString(w.getMessage(),
-            file != null ? file.getExternalForm() : "<unknown file>",
-            // TODO one or zero based?
-            new Position(w.getLineNumber(), w.getPosInLine())))
+            file != null ? file.getExternalForm() : "<unknown file>", w.getPosition()))
                 .collect(Collectors.<PositionedString>toList());
     }
 

key.core/src/main/java/de/uka/ilkd/key/speclang/PositionedString.java

@@ -50,10 +50,6 @@ public PositionedString(@Nonnull String text, @Nullable String fileName,
         this.pos = pos;
     }
 
-    public PositionedString(@Nonnull String text, Token t) {
-        this(text, t.getInputStream().getSourceName(), Position.fromToken(t));
-    }
-
     public PositionedString(@Nonnull String text, String fileName) {
         this(text, fileName, null);
     }

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java

@@ -85,7 +85,7 @@ private String concatenate(Comment[] comments) {
         StringBuilder sb = new StringBuilder(comments[0].getText());
 
         for (int i = 1; i < comments.length; i++) {
-            Position relativePos = comments[i].getRelativePosition();
+            var relativePos = comments[i].getRelativePosition();
             for (int j = 0; j < relativePos.getLine(); j++) {
                 sb.append("\n");
             }

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLClassInv.java

@@ -23,6 +23,7 @@ public TextualJMLClassInv(ImmutableList<JMLModifier> mods,
             JmlParser.Class_invariantContext ctx) {
         super(mods, null);
         inv = ctx;
+        setPosition(ctx);
     }
 
     public ParserRuleContext getInv() {

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLDepends.java

@@ -21,6 +21,7 @@ public final class TextualJMLDepends extends TextualJMLConstruct {
     public TextualJMLDepends(ImmutableList<JMLModifier> mods, Name[] heaps,
             @Nonnull LabeledParserRuleContext depends) {
         super(mods);
+        setPosition(depends);
         for (Name hName : HeapLDT.VALID_HEAP_NAMES) {
             this.depends.put(hName, ImmutableSLList.nil());
         }

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLoopSpec.java

@@ -42,8 +42,12 @@ public TextualJMLLoopSpec addClause(ClauseHd clause, LabeledParserRuleContext ct
 
     public TextualJMLLoopSpec addClause(ClauseHd clause, @Nullable Name heapName,
             LabeledParserRuleContext ctx) {
-        if (heapName == null)
+        if (heapName == null) {
             heapName = HeapLDT.BASE_HEAP_NAME;
+        }
+        if (clauses.isEmpty()) {
+            setPosition(ctx);
+        }
         clauses.add(new Entry(clause, ctx, heapName));
         return this;
     }

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java

@@ -20,6 +20,7 @@ public TextualJMLMethodDecl(ImmutableList<JMLModifier> mods,
             JmlParser.Method_declarationContext methodDefinition) {
         super(mods);
         this.methodDefinition = methodDefinition;
+        setPosition(methodDefinition);
     }
 
     public String getParsableDeclaration() {

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java

@@ -107,6 +107,9 @@ public TextualJMLSpecCase(ImmutableList<JMLModifier> mods, @Nonnull Behavior beh
     }
 
     public TextualJMLSpecCase addClause(Clause clause, LabeledParserRuleContext ctx) {
+        if (clauses.isEmpty()) {
+            setPosition(ctx);
+        }
         clauses.add(new Entry(clause, ctx));
         return this;
     }

key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLExceptionFactory.java

@@ -203,10 +203,6 @@ public SLTranslationException createWarningException(String message) {
             createAbsolutePosition(this.line, this.column));
     }
 
-    public SLTranslationException createWarningException(String message, Token t) {
-        return new SLWarningException(new PositionedString(message, t));
-    }
-
     /**
      * Create a message from a {@link RecognitionException}. This needs to be done manually because
      * antlr exceptions are not designed to provide error messages, see:

key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java

@@ -38,8 +38,7 @@ public BuildingException(@Nullable Token t, String message, Throwable e) {
 
     private static String getPosition(Token t) {
         if (t != null) {
-            return t.getTokenSource().getSourceName() + ":" + t.getLine() + ":"
-                + t.getCharPositionInLine() + 1;
+            return t.getTokenSource().getSourceName() + ":" + Position.fromToken(t);
         } else
             return "";
     }