Improve duplicate identifier error

viperproject · Jul 19, 2023 · 29e25ab · 29e25ab
1 parent c2c1b11
commit 29e25ab
Show file tree

Hide file tree

Showing 9 changed files with 24 additions and 20 deletions.
diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -876,20 +876,21 @@ case class NameAnalyser() {
           namesInScope ++= getCurrentMap.map(_._1)
         n match {
           case d: PDeclaration =>
-            getMap(d).get(d.idndef.name) match {
+            val map = getMap(d)
+            map.get(d.idndef.name) match {
               case Some(m: PMember) if d eq m =>
               // We re-encountered a member we already looked at in the previous run.
               // This is expected, nothing to do.
               case Some(e: PDeclaration) =>
-                messages ++= FastMessaging.message(e.idndef, "Duplicate identifier `" + e.idndef.name + "' at " + e.idndef.pos._1 + " and at " + d.idndef.pos._1)
+                messages ++= FastMessaging.message(d.idndef, "Duplicate identifier `" + e.idndef.name + "' at " + e.idndef.pos._1 + " and at " + d.idndef.pos._1)
               case None =>
                 globalDeclarationMap.get(d.idndef.name) match {
                   case Some(e: PDeclaration) =>
                     if (!(d.parent.isDefined && d.parent.get.isInstanceOf[PDomainFunction]))
-                      messages ++= FastMessaging.message(e, "Identifier shadowing `" + e.idndef.name + "' at " + e.idndef.pos._1 + " and at " + d.idndef.pos._1)
+                      messages ++= FastMessaging.message(d.idndef, "Identifier shadowing `" + e.idndef.name + "' at " + e.idndef.pos._1 + " and at " + d.idndef.pos._1)
                   case None =>
-                    getMap(d).put(d.idndef.name, d)
                 }
+                map.put(d.idndef.name, d)
             }
           case i@PIdnUse(name) =>
             // look up in both maps (if we are not in a method currently, we look in the same map twice, but that is ok)

diff --git a/src/test/resources/adt/declarations_2.vpr b/src/test/resources/adt/declarations_2.vpr
@@ -1,14 +1,14 @@
 adt SimpleList {
     SimpleNil()
-    //:: ExpectedOutput(typechecker.error)
     SimpleCons(value: Int, tail: SimpleList)
+    //:: ExpectedOutput(typechecker.error)
     SimpleCons(value: Int, tail: SimpleList)
 }
 
 adt List[T] {
     Nil()
-    //:: ExpectedOutput(typechecker.error)
     Cons(value: T, tail: List[T])
+    //:: ExpectedOutput(typechecker.error)
     Cons(value: T, tail: List[T])
 }
 

diff --git a/src/test/resources/adt/declarations_5.vpr b/src/test/resources/adt/declarations_5.vpr
@@ -1,9 +1,9 @@
 adt List[T] {
     Nil()
+    //:: ExpectedOutput(typechecker.error)
     Cons(value: T, tail: List[T])
 }
 
-//:: ExpectedOutput(typechecker.error)
 field value: Int
 
 
diff --git a/src/test/resources/all/basic/let_consistency_resolver.vpr b/src/test/resources/all/basic/let_consistency_resolver.vpr
@@ -12,11 +12,12 @@ method test02() {
   assert (let y == (0) in true) && y == 0
 }
 
-//:: ExpectedOutput(typechecker.error)
 method test03(y: Int) {
+  //:: ExpectedOutput(typechecker.error)
   assert let y == (0) in true
 }
 
+//:: ExpectedOutput(typechecker.error)
 method test03() {
   //:: ExpectedOutput(typechecker.error)
   assert let y == (0) in let y == (true) in true

diff --git a/src/test/resources/all/issues/silver/0027.vpr b/src/test/resources/all/issues/silver/0027.vpr
@@ -1,9 +1,9 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-//:: ExpectedOutput(typechecker.error)
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 
+//:: ExpectedOutput(typechecker.error)
 function f(): Bool { true }
 
 method m(x: Ref)

diff --git a/src/test/resources/all/issues/silver/0048.vpr b/src/test/resources/all/issues/silver/0048.vpr
@@ -1,6 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-  //:: ExpectedOutput(typechecker.error)
-method Bug() {}
+method Bug() {}
+//:: ExpectedOutput(typechecker.error)
 method Bug() {}
diff --git a/src/test/resources/all/issues/silver/0050.vpr b/src/test/resources/all/issues/silver/0050.vpr
@@ -1,14 +1,15 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
-//:: ExpectedOutput(typechecker.error)
 field x: Int
 
+//:: ExpectedOutput(typechecker.error)
 method test1(x: Ref)
   requires acc(x.x) // error: expected field
 {}
 
+//:: ExpectedOutput(typechecker.error)
 method test2(x: Ref)
   requires acc(x.f) // no error
 {}
diff --git a/src/test/resources/all/issues/silver/0473.vpr b/src/test/resources/all/issues/silver/0473.vpr
@@ -16,6 +16,6 @@ domain Test[T] {
 }
 
 domain DuplicateTest[T] {
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   function add_wrong(left: T, left: T): T
 }
diff --git a/src/test/resources/wands/regression/consistency_let_resolver.vpr b/src/test/resources/wands/regression/consistency_let_resolver.vpr
@@ -12,11 +12,12 @@ method test02() {
   assert (let y == (0) in true) && y == 0
 }
 
-//:: ExpectedOutput(typechecker.error)
 method test03(y: Int) {
+  //:: ExpectedOutput(typechecker.error)
   assert let y == (0) in true
 }
 
+//:: ExpectedOutput(typechecker.error)
 method test03() {
   //:: ExpectedOutput(typechecker.error)
   assert let y == (0) in let y == (true) in true