AbstractVerificationError structural equality does not take position into account

[viper-admin]

Created by @vakaras on 2015-07-31 14:30

When Silver AST was designed, a design decision was made that node position is not taken into account when comparing two nodes. However, this causes a problem that two verification errors at different locations can also be considered equal if they refer to identical AST nodes.

This problem is illustrated with the following Scala test:

#!scala

/*
 * This Source Code Form is subject to the terms of the Mozilla Public
 * License, v. 2.0. If a copy of the MPL was not distributed with this
 * file, You can obtain one at http://mozilla.org/MPL/2.0/.
 */

package viper.silver

import org.scalatest.FunSuite
import viper.silver.ast.{Exp, LineColumnPosition, IntLit, LtCmp}
import org.scalatest.matchers.ShouldMatchers
import viper.silver.verifier.errors.ContractNotWellformed
import viper.silver.verifier.reasons.AssertionFalse

class AstNodeEqualityTest extends FunSuite with ShouldMatchers {

  test("line numbers") {

    val position1 = LineColumnPosition(1, 1)
    val offendingNode1: Exp = LtCmp(
      IntLit(1)(position1),
      IntLit(2)(position1)
    )(position1)

    val reason1 = AssertionFalse(offendingNode1)
    val error1 = ContractNotWellformed(offendingNode1, reason1)

    val position2 = LineColumnPosition(4, 1)
    val offendingNode2: Exp = LtCmp(
      IntLit(1)(position2),
      IntLit(2)(position2)
    )(position2)

    val reason2 = AssertionFalse(offendingNode2)
    val error2 = ContractNotWellformed(offendingNode2, reason2)

    assert(error1 != error2)

  }

}

SBT output:

#!console

> test-only viper.silver.AstNodeEqualityTest
[info] Compiling 1 Scala source to /home/developer/source/silver/target/scala-2.10/test-classes...
[info] AstNodeEqualityTest:
[info] - line numbers *** FAILED ***
[info]   org.scalatest.exceptions.TestFailedException was thrown. (AstNodeEqualityTest.scala:38)
[error] Failed: : Total 1, Failed 1, Errors 0, Passed 0, Skipped 0
[error] Failed tests:
[error]         viper.silver.AstNodeEqualityTest
[error] (test:test-only) sbt.TestsFailedException: Tests unsuccessful
[error] Total time: 3 s, completed Jul 31, 2015 2:19:24 PM