fixed intendation, added comment, removed todo

viperproject · Oct 2, 2023 · dcc383d · dcc383d
1 parent 0c28aee
commit dcc383d
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 4 deletions.
diff --git a/build.sbt b/build.sbt
@@ -34,7 +34,7 @@ lazy val gobra = (project in file("."))
     libraryDependencies += "org.apache.commons" % "commons-lang3" % "3.9", // for SystemUtils
     libraryDependencies += "org.apache.commons" % "commons-text" % "1.9", // for escaping strings in parser preprocessor
     libraryDependencies += "commons-codec" % "commons-codec" % "1.15", // for obtaining the hex encoding of a string
-    libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.12.0",
+    libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.13.0",
     libraryDependencies += "org.scalaz" %% "scalaz-core" % "7.3.7", // used for EitherT
 
     scalacOptions ++= Seq(

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala
@@ -30,7 +30,7 @@ trait GhostIdTyping { this: TypeInfoImpl =>
     })
     case c: AdtDestructor => wellDefAndType(c.decl.typ)
     case _: AdtDiscriminator => LocalMessages(noMessages)
-    case _: MatchVariable => LocalMessages(noMessages) // TODO
+    case _: MatchVariable => LocalMessages(noMessages)
     case _: BuiltInFPredicate | _: BuiltInMPredicate => LocalMessages(noMessages)
   }
 

diff --git a/src/test/resources/regressions/issues/000589.gobra b/src/test/resources/regressions/issues/000589.gobra
@@ -17,7 +17,7 @@ decreases l
 func length(l list) int {
 	match l {
 		case Empty{}:
-		    //:: ExpectedOutput(assert_error:assertion_error)
+			//:: ExpectedOutput(assert_error:assertion_error)
 			assert false // <--- assert false here should be reachable
 			return 0
 		default:

diff --git a/src/test/resources/regressions/issues/000655.gobra b/src/test/resources/regressions/issues/000655.gobra
@@ -23,6 +23,8 @@ func foo2() {
 }
 
 /*
+// should work in the future:
+
 ghost
 pure func foo3(x pkg.Tree) bool {
   return match x {
@@ -32,5 +34,4 @@ pure func foo3(x pkg.Tree) bool {
     case _: false
   }
 }
-
 */