WIP: fixing issue #719

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

@@ -261,23 +261,25 @@ case class PIfStmt(ifs: Vector[PIfClause], els: Option[PBlock]) extends PActualS
 
 case class PIfClause(pre: Option[PSimpleStmt], condition: PExpression, body: PBlock) extends PNode
 
-case class PExprSwitchStmt(pre: Option[PSimpleStmt], exp: PExpression, cases: Vector[PExprSwitchCase], dflt: Vector[PBlock]) extends PActualStatement with PScope with PGhostifiableStatement
+sealed trait PBreakableStmt extends PActualStatement
+
+case class PExprSwitchStmt(pre: Option[PSimpleStmt], exp: PExpression, cases: Vector[PExprSwitchCase], dflt: Vector[PBlock]) extends PBreakableStmt with PScope with PGhostifiableStatement
 
 sealed trait PExprSwitchClause extends PNode
 
 case class PExprSwitchDflt(body: PBlock) extends PExprSwitchClause
 
 case class PExprSwitchCase(left: Vector[PExpression], body: PBlock) extends PExprSwitchClause
 
-case class PTypeSwitchStmt(pre: Option[PSimpleStmt], exp: PExpression, binder: Option[PIdnDef], cases: Vector[PTypeSwitchCase], dflt: Vector[PBlock]) extends PActualStatement with PScope with PGhostifiableStatement
+case class PTypeSwitchStmt(pre: Option[PSimpleStmt], exp: PExpression, binder: Option[PIdnDef], cases: Vector[PTypeSwitchCase], dflt: Vector[PBlock]) extends PBreakableStmt with PScope with PGhostifiableStatement
 
 sealed trait PTypeSwitchClause extends PNode
 
 case class PTypeSwitchDflt(body: PBlock) extends PTypeSwitchClause
 
 case class PTypeSwitchCase(left: Vector[PExpressionOrType], body: PBlock) extends PTypeSwitchClause
 
-sealed trait PGeneralForStmt extends PActualStatement
+sealed trait PGeneralForStmt extends PBreakableStmt
 
 case class PForStmt(pre: Option[PSimpleStmt], cond: PExpression, post: Option[PSimpleStmt], spec: PLoopSpec, body: PBlock) extends PGeneralForStmt with PScope with PGhostifiableStatement
 
@@ -290,7 +292,7 @@ case class PGoStmt(exp: PExpression) extends PActualStatement
 sealed trait PDeferrable extends PNode
 case class PDeferStmt(exp: PDeferrable) extends PActualStatement with PGhostifiableStatement
 
-case class PSelectStmt(send: Vector[PSelectSend], rec: Vector[PSelectRecv], aRec: Vector[PSelectAssRecv], sRec: Vector[PSelectShortRecv], dflt: Vector[PSelectDflt]) extends PActualStatement with PScope
+case class PSelectStmt(send: Vector[PSelectSend], rec: Vector[PSelectRecv], aRec: Vector[PSelectAssRecv], sRec: Vector[PSelectShortRecv], dflt: Vector[PSelectDflt]) extends PBreakableStmt with PScope
 
 sealed trait PSelectClause extends PNode
 

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

@@ -4928,11 +4928,11 @@ object Desugar extends LazyLogging {
     def continueLabel(loop: PGeneralForStmt, info: TypeInfo) : String = relativeId(loop, info) + CONTINUE_LABEL_SUFFIX
 
     /** returns the relativeId with the BREAK_LABEL_SUFFIX appended */
-    def breakLabel(loop: PGeneralForStmt, info: TypeInfo) : String = relativeId(loop, info) + BREAK_LABEL_SUFFIX
+    def breakLabel(loop: PBreakableStmt, info: TypeInfo) : String = relativeId(loop, info) + BREAK_LABEL_SUFFIX
 
     /**
       * Finds the enclosing loop which the continue statement refers to and fetches its
-      * continue label.
+      * continue label. Note that `continue` always refers to the inner-most for loop.
       */
     def fetchContinueLabel(n: PContinue, info: TypeInfo) : String = {
       n.label match {
@@ -4947,15 +4947,15 @@ object Desugar extends LazyLogging {
 
     /**
       * Finds the enclosing loop which the break statement refers to and fetches its
-      * break label.
+      * break label. Note that `break` refers to the inner-most for loop, switch or select statement.
       */
     def fetchBreakLabel(n: PBreak, info: TypeInfo) : String = {
       n.label match {
         case None =>
-          val Some(loop) = info.enclosingLoopNode(n)
+          val Some(loop) = info.enclosingBreakableNode(n)
           breakLabel(loop, info)
         case Some(label) =>
-          val Some(loop) = info.enclosingLabeledLoopNode(label, n)
+          val Some(loop) = info.enclosingBreakableNode(label, n)
           breakLabel(loop, info)
       }
     }

src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala

@@ -6,7 +6,7 @@
 
 package viper.gobra.frontend.info
 
-import viper.gobra.ast.frontend.{PCodeRoot, PEmbeddedDecl, PExpression, PFieldDecl, PFunctionDecl, PFunctionOrMethodDecl, PGeneralForStmt, PIdnNode, PIdnUse, PKeyedElement, PLabelUse, PMPredicateDecl, PMPredicateSig, PMember, PMethodDecl, PMethodSig, PMisc, PNode, PParameter, PPkgDef, PScope, PType}
+import viper.gobra.ast.frontend.{PActualStatement, PBreakableStmt, PCodeRoot, PEmbeddedDecl, PExpression, PFieldDecl, PFunctionDecl, PFunctionOrMethodDecl, PGeneralForStmt, PIdnNode, PIdnUse, PKeyedElement, PLabelUse, PMPredicateDecl, PMPredicateSig, PMember, PMethodDecl, PMethodSig, PMisc, PNode, PParameter, PPkgDef, PScope, PType}
 import viper.gobra.frontend.PackageInfo
 import viper.gobra.frontend.PackageResolver.AbstractImport
 import viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInMemberTag
@@ -119,6 +119,12 @@ trait ExternalTypeInfo {
   /** if it exists, it returns the for loop node that contains 'n' */
   def enclosingLoopNode(n: PNode) : Option[PGeneralForStmt]
 
+  /** if it exists, it returns the for loop, switch or select node that contains 'n' with label 'label' */
+  def enclosingBreakableNode(label: PLabelUse, n: PNode): Option[PBreakableStmt]
+
+  /** if it exists, it returns the for loop, switch or select node that contains 'n' */
+  def enclosingBreakableNode(n: PNode): Option[PBreakableStmt]
+
   /** returns the enclosing invariant of 'n' */
   def enclosingInvariantNode(n: PExpression) : PExpression
 

src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala

@@ -95,6 +95,10 @@ class TypeInfoImpl(final val tree: Info.GoTree, final val dependentTypeInfo: Map
 
   override def enclosingLoopNode(n: PNode) : Option[PGeneralForStmt] = enclosingLoopUntilOutline(n).toOption
 
+  override def enclosingBreakableNode(label: PLabelUse, n: PNode): Option[PBreakableStmt] = enclosingLabeledBreakable(label, n).toOption
+
+  override def enclosingBreakableNode(n: PNode): Option[PBreakableStmt] = enclosingBreakableUntilOutline(n).toOption
+
   override def enclosingInvariantNode(n: PExpression) : PExpression = enclosingInvariant(n)
 
   override def samePkgDepsOfGlobalVar(n: SymbolTable.GlobalVariable): Vector[SymbolTable.GlobalVariable] =

src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala

@@ -50,6 +50,25 @@ trait Enclosing { this: TypeInfoImpl =>
     }
   }
 
+  lazy val enclosingBreakableUntilOutline: PNode => Either[Option[PNode], PBreakableStmt] = {
+    down[Either[Option[PNode], PBreakableStmt]](Left(None)) {
+      case x: POutline => Left(Some(x))
+      case x: PBreakableStmt => Right(x)
+    }
+  }
+
+  // Returns the enclosing breakable statement that has a specific label
+  def enclosingLabeledBreakable(label: PLabelUse, node: PNode): Either[Option[PNode], PBreakableStmt] = {
+    enclosingBreakableUntilOutline(node) match {
+      case Right(breakable) => breakable match {
+        case tree.parent(l: PLabeledStmt) if l.label.name == label.name => Right(breakable)
+        case tree.parent(p) => enclosingLabeledBreakable(label, p)
+        case _ => Left(None)
+      }
+      case r => r
+    }
+  }
+
   def enclosingInvariant(n: PExpression) : PExpression = {
     n match {
       case tree.parent(p) if enclosingExpr(p).isDefined => enclosingExpr(p).get

src/test/resources/regressions/issues/000719.gobra

@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000719
+
+decreases
+func foo() {
+    //:: ExpectedOutput(loop_termination_error)
+    decreases
+    for i := 0; ; i++ {
+        switch i {
+            default:
+                break
+        }
+    }
+}