Skip to content

Commit 4b5f2f2

Browse files
authored
Do not add extra newline at end of file (#877)
1 parent 836ccf1 commit 4b5f2f2

File tree

3 files changed

+17
-3
lines changed

3 files changed

+17
-3
lines changed

src/main/scala/viper/silver/ast/Position.scala

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -108,8 +108,10 @@ class IdentifierPosition(val file: Path, val start: HasLineColumn, val end: Opti
108108

109109
class LineCol(fp: FastParser) {
110110
def getPos(index: Int): (Int, Int) = {
111-
// val Array(line, col) = ctx.input.prettyIndex(index).split(":").map(_.toInt)
112111
val line_offset = fp._line_offset
112+
if (line_offset.isEmpty) {
113+
return (1, 1);
114+
}
113115
val result = java.util.Arrays.binarySearch(line_offset, index)
114116
if (result >= 0) {
115117
// Exact match

src/main/scala/viper/silver/parser/FastParser.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -990,7 +990,7 @@ class FastParser {
990990
// Add an empty line at the end to make `computeFrom(s.length)` return
991991
// `(lines.length, 1)`, as the old implementation of `computeFrom` used to do.
992992
val lines = s.linesWithSeparators
993-
_line_offset = (lines.map(_.length) ++ Seq(0)).toArray
993+
_line_offset = lines.map(_.length).toArray
994994
var offset = 0
995995
for (i <- _line_offset.indices) {
996996
val line_length = _line_offset(i)

src/test/scala/AstPositionsTests.scala

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ class AstPositionsTests extends AnyFunSuite {
6363
|method bar(r: Ref)
6464
| requires 0 > r . foo
6565
|// Comment
66-
|""".stripMargin
66+
|function end(): Ref""".stripMargin
6767

6868
val res: Program = generateViperAst(code).get
6969
// Check position of field
@@ -188,5 +188,17 @@ class AstPositionsTests extends AnyFunSuite {
188188
case _ =>
189189
fail("methods must have start and end positions set")
190190
}
191+
// Check position of function
192+
assert(res.functions.length === 1)
193+
val fn: Function = res.functions(0)
194+
fn.pos match {
195+
case spos: AbstractSourcePosition =>
196+
assert(spos.start.line === 15 && spos.end.get.line === 15)
197+
// Here it is unclear if we want to include the `function ` part in the pos
198+
assert(spos.start.column === 1 || spos.start.column === 10)
199+
assert(spos.end.get.column === 20)
200+
case _ =>
201+
fail("functions must have start and end positions set")
202+
}
191203
}
192204
}

0 commit comments

Comments
 (0)