Range

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -797,7 +797,7 @@ sealed trait PMisc extends PNode
 
 sealed trait PActualMisc extends PMisc
 
-case class PRange(exp: PExpression, enumerated: PIdnUnk) extends PActualMisc
+case class PRange(exp: PExpression, enumerated: PUnkLikeId) extends PActualMisc
 
 sealed trait PParameter extends PMisc {
   def typ: PType

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -1823,7 +1823,10 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     } else if (has(ctx.rangeClause())) {
       // for <assignees (:= | =)>? range <expr>
       val expr = visitNode[PExpression](ctx.rangeClause().expression()).at(ctx.rangeClause())
-      val enumerated = idnUnk.get(ctx.rangeClause().IDENTIFIER()).at(ctx.rangeClause.IDENTIFIER())
+      val enumerated = if (ctx.rangeClause().IDENTIFIER().getSymbol().getText() != "_")
+        idnUnk.get(ctx.rangeClause().IDENTIFIER()).at(ctx.rangeClause.IDENTIFIER())
+      else
+        PWildcard().at(ctx.rangeClause().IDENTIFIER())
       val range = PRange(expr, enumerated).at(ctx.rangeClause())
       if (has(ctx.rangeClause().DECLARE_ASSIGN())) {
         // :=

src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala

@@ -277,18 +277,11 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
   def getBlankAssigneeTypeRange(n: PNode, left: Vector[PNode], range: PRange): Type = {
     require(n.isInstanceOf[PIdnNode] || n.isInstanceOf[PBlankIdentifier])
     val pos = left indexWhere (n eq _)
-    if (pos >= 0) {
-      underlyingType(exprType(range.exp)) match {
-        case ChannelT(elem, ChannelModus.Recv | ChannelModus.Bi) => elem
-        case _ => miscType(range).asInstanceOf[InternalSingleMulti].mul.ts(pos)
-      }
-    } else if (n eq range.enumerated) {
-      underlyingType(exprType(range.exp)) match {
-        case _: SliceT | _: ArrayT => IntT(config.typeBounds.Int)
-        case MapT(key, _) => SetT(key)
-        case t => violation(s"type $t is not supported for range")
-      }
-    } else violation("did not find expression corresponding to " + n)
+    violation(pos >= 0, "did not find expression corresponding to " + n)
+    underlyingType(exprType(range.exp)) match {
+      case ChannelT(elem, ChannelModus.Recv | ChannelModus.Bi) => elem
+      case _ => miscType(range).asInstanceOf[InternalSingleMulti].mul.ts(pos)
+    }
   }
 
   def getWildcardType(w: PWildcard): Type = {
@@ -298,6 +291,13 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
         case PVarDecl(typ, right, left, _) => typ.map(symbType).getOrElse(getBlankAssigneeType(w, left, right))
         case PConstSpec(typ, right, left) => typ.map(symbType).getOrElse(getBlankAssigneeType(w, left, right))
         case PShortForRange(range, shorts, _, _, _) => getBlankAssigneeTypeRange(w, shorts, range)
+        case PRange(exp, enumerated) => if (w eq enumerated)
+          underlyingType(exprType(exp)) match {
+            case _: SliceT | _: ArrayT => IntT(config.typeBounds.Int)
+            case MapT(key, _) => SetT(key)
+            case t => violation(s"type $t is not supported for range")
+          }
+          else violation("did not find expression corresponding to " + w)
         case _ => ???
       }
       case _ => ???

src/test/scala/viper/gobra/parsing/GoParserUnitTests.scala

@@ -31,19 +31,19 @@ class GoParserUnitTests extends AnyFunSuite with Matchers with Inside {
     "package p; func f(x ...int,) {};",
     "package p; type T []int; var a []bool; func f() { if a[T{42}[0]] {} };",
     "package p; type T []int; func g(int) bool { return true }; func f() { if g(T{42}[0]) {} };",
-    "package p; type T []int; func f() { for _ = range []int{T{42}[0]} {} };",
+    "package p; type T []int; func f() { for _ = range []int{T{42}[0]} with _ {} };",
     "package p; var a = T{{1, 2}, {3, 4}}",
     "package p; func f() { select { case <- c: case c <- d: case c <- <- d: case <-c <- d: } };",
     "package p; func f() { select { case x := (<-c): } };",
     "package p; func f() { if ; true {} };",
     "package p; func f() { switch ; {} };",
-    "package p; func f() { for _ = range \"foo\" + \"bar\" {} };",
+    "package p; func f() { for _ = range \"foo\" + \"bar\" with _ {} };",
     "package p; func f() { var s []int; g(s[:], s[i:], s[:j], s[i:j], s[i:j:k], s[:j:k]) };",
     "package p; var ( _ = (struct {*T}).m; _ = (interface {T}).m )",
     "package p; func ((T),) m() {}",
     "package p; func ((*T),) m() {}",
     "package p; func (*(T),) m() {}",
-    "package p; func _(x []int) { for range x {} }",
+    "package p; func _(x []int) { for range x with _ {} }",
     "package p; func _() { if [T{}.n]int{} {} }",
     "package p; func _() { map[int]int{}[0]++; map[int]int{}[0] += 1 }",
     "package p; func _(x interface{f()}) { interface{f()}(x).f() }",
@@ -76,7 +76,8 @@ class GoParserUnitTests extends AnyFunSuite with Matchers with Inside {
     "package p; func f() { if f(); /* ERROR \"missing condition\" */ {} };",
     "package p; func f() { if _ = range /* ERROR \"expected operand\" */ x; true {} };",
     "package p; func f() { switch _ /* ERROR \"expected switch expression\" */ = range x; true {} };",
-    "package p; func f() { for _ = range x ; /* ERROR \"expected '{'\" */ ; {} };",
+    "package p; func f() { for _ = range x {}; /* ERROR \"expected 'with'\" */ ; {} };",
+    "package p; func f() { for _ = range x with _ ; /* ERROR \"expected '{'\" */ ; {} };",
     "package p; func f() { for ; ; _ = range /* ERROR \"expected operand\" */ x {} };",
     "package p; func f() { for ; _ /* ERROR \"expected boolean or range expression\" */ = range x ; {} };",
     "package p; func f() { switch t = /* ERROR \"expected ':=', found '='\" */ t.(type) {} };",