From 29e25ab6e3f46edb2cbe38109666eb6100ffac06 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Wed, 19 Jul 2023 15:26:03 +0200 Subject: [PATCH] Improve duplicate identifier error --- src/main/scala/viper/silver/parser/Resolver.scala | 9 +++++---- src/test/resources/adt/declarations_2.vpr | 4 ++-- src/test/resources/adt/declarations_5.vpr | 2 +- .../resources/all/basic/let_consistency_resolver.vpr | 3 ++- src/test/resources/all/issues/silver/0027.vpr | 8 ++++---- src/test/resources/all/issues/silver/0048.vpr | 4 ++-- src/test/resources/all/issues/silver/0050.vpr | 9 +++++---- src/test/resources/all/issues/silver/0473.vpr | 2 +- .../wands/regression/consistency_let_resolver.vpr | 3 ++- 9 files changed, 24 insertions(+), 20 deletions(-) diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala index f74b66d1b..f243a5677 100644 --- 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 index 19502fbd2..144b4bae2 100644 --- 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 index df0eb8eab..058b15e3e 100644 --- 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 index 7d4249c60..842062e5e 100644 --- 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 index 153dba0ce..4bf9d35de 100644 --- 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 index a7e0775c6..51ea6152d 100644 --- 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() {} \ No newline at end of file diff --git a/src/test/resources/all/issues/silver/0050.vpr b/src/test/resources/all/issues/silver/0050.vpr index 1188fc04d..5adffea15 100644 --- 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 index c5263a12b..fb0f658af 100644 --- 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 index 7d4249c60..842062e5e 100644 --- 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