cleanup

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

@@ -53,8 +53,7 @@ case class PPackage(
 
 case class PProgram(
                      packageClause: PPackageClause,
-                     // TODO: doc
-                     staticInvs: Vector[PPkgInvariant],
+                     pkgInvariants: Vector[PPkgInvariant],
                      imports: Vector[PImport],
                      friends: Vector[PFriendPkgDecl],
                      declarations: Vector[PMember]
@@ -63,8 +62,7 @@ case class PProgram(
 
 case class PPreamble(
                       packageClause: PPackageClause,
-                      // TODO: doc
-                      staticInvs: Vector[PPkgInvariant],
+                      pkgInvariants: Vector[PPkgInvariant],
                       imports: Vector[PImport],
                       friends: Vector[PFriendPkgDecl],
                       positions: PositionManager,

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

@@ -63,25 +63,25 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   // program
 
   def showProgram(p: PProgram): Doc = p match {
-    case PProgram(packageClause, /*progPosts,*/ staticInvs, imports, friends, declarations) =>
-      showPreamble(packageClause, /*progPosts,*/ staticInvs, imports, friends) <>
+    case PProgram(packageClause, pkgInvs, imports, friends, declarations) =>
+      showPreamble(packageClause, pkgInvs, imports, friends) <>
         ssep(declarations map showMember, line <> line) <> line
   }
 
   // preamble
 
   def showPreamble(p: PPreamble): Doc = p match {
-    case PPreamble(packageClause, staticInvs, imports, friends, _) =>
-      showPreamble(packageClause, staticInvs, imports, friends)
+    case PPreamble(packageClause, pkgInvs, imports, friends, _) =>
+      showPreamble(packageClause, pkgInvs, imports, friends)
   }
 
   private def showPreamble(
                             packageClause: PPackageClause,
-                            staticInvs: Vector[PPkgInvariant],
+                            pkgInvs: Vector[PPkgInvariant],
                             imports: Vector[PImport],
                             friends: Vector[PFriendPkgDecl]
                           ): Doc =
-    vcat(staticInvs.map(showPkgInvariant)) <>
+    vcat(pkgInvs.map(showPkgInvariant)) <>
       showPackageClause(packageClause) <> line <> line <>
       ssep(friends map showFriend, line) <> line <>
       ssep(imports map showImport, line) <> line

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

@@ -65,7 +65,7 @@ object Desugar extends LazyLogging {
         val pkg = i.getTypeInfo.tree.originalRoot
         importsCollector.registerCurrentPackage(pkg)
         val nonDupInvs = pkg.programs
-          .flatMap(_.staticInvs)
+          .flatMap(_.pkgInvariants)
           .filter(!_.duplicable)
           .map(_.inv)
           .map(mainDesugarer.specificationD(mainDesugarer.FunctionContext.empty(), i.getTypeInfo)(_))
@@ -3476,7 +3476,7 @@ object Desugar extends LazyLogging {
 
       // Check that all duplicable static invariants are actually duplicable.
       mainPkg.programs
-        .flatMap(_.staticInvs)
+        .flatMap(_.pkgInvariants)
         .filter(_.duplicable)
         .map(_.inv)
         .map(genCheckAssertionIsDup)
@@ -3572,7 +3572,7 @@ object Desugar extends LazyLogging {
 
       // collect package invariants
       val partitionFunc = (inv: PPkgInvariant) => if (inv.duplicable) Left(inv.inv) else Right(inv.inv)
-      val (dups, nonDups) = pkg.programs.flatMap(_.staticInvs).partitionMap(partitionFunc)
+      val (dups, nonDups) = pkg.programs.flatMap(_.pkgInvariants).partitionMap(partitionFunc)
       val goA = specificationD(FunctionContext.empty(), info)(_)
       val dDups = dups.map(goA)
       val dNonDups = nonDups.map(goA)
@@ -3678,7 +3678,7 @@ object Desugar extends LazyLogging {
       val progPres: Vector[in.Assertion] = p.imports.flatMap(_.importPres).map(specificationD(FunctionContext.empty(), info)(_))
       // val progPosts: Vector[in.Assertion] = p.initPosts.map(specificationD(FunctionContext.empty(), info)(_))
       val progPosts: Vector[in.Assertion] = Vector.empty // p.initPosts.map(specificationD(FunctionContext.empty(), info)(_))
-      val pkgInvariants: Vector[in.Assertion] = p.staticInvs.map{i => specificationD(FunctionContext.empty(), info)(i.inv)}
+      val pkgInvariants: Vector[in.Assertion] = p.pkgInvariants.map{ i => specificationD(FunctionContext.empty(), info)(i.inv)}
       val resourcesForFriends: Vector[in.Assertion] = p.friends.map{i => specificationD(FunctionContext.empty(), info)(i.assertion)}
       val pkgInvariantsImportedPackages: Vector[in.Assertion] =
         initSpecs match {

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

@@ -430,7 +430,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     val spec = if (ctx.specification() != null)
       visitSpecification(ctx.specification())
     else
-      PFunctionSpec(Vector.empty,Vector.empty,Vector.empty, Vector.empty, Vector.empty, mayBeUsedInInit = false).at(ctx) // TODO: drop
+      PFunctionSpec(Vector.empty,Vector.empty,Vector.empty, Vector.empty, Vector.empty).at(ctx)
     // The name of each explicitly specified method must be unique and not blank.
     val id = idnDef.get(ctx.IDENTIFIER())
     val args = visitNode[Vector[Vector[PParameter]]](ctx.parameters())
@@ -2265,15 +2265,15 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     if (initPosts.nonEmpty) {
       violation(s"initEnsures clauses are no longer supported after Gobra PR #797.")
     }
-    val staticInvs: Vector[PPkgInvariant] = visitListNode[PPkgInvariant](ctx.pkgInvariant())
+    val pkgInvs: Vector[PPkgInvariant] = visitListNode[PPkgInvariant](ctx.pkgInvariant())
     val importDecls = ctx.importDecl().asScala.toVector.flatMap(visitImportDecl)
     val friendPkgs: Vector[PFriendPkgDecl] = visitListNode[PFriendPkgDecl](ctx.friendPkgDecl())
 
     // Don't parse functions/methods if the identifier is blank
     val members = visitListNode[PMember](ctx.specMember())
     val ghostMembers = ctx.ghostMember().asScala.flatMap(visitNode[Vector[PGhostMember]])
     val decls = ctx.declaration().asScala.toVector.flatMap(visitDeclaration(_).asInstanceOf[Vector[PDeclaration]])
-    PProgram(packageClause, /* initPosts, */ staticInvs, importDecls, friendPkgs, members ++ decls ++ ghostMembers).at(ctx)
+    PProgram(packageClause, pkgInvs, importDecls, friendPkgs, members ++ decls ++ ghostMembers).at(ctx)
   }
 
   override def visitPreamble(ctx: GobraParser.PreambleContext): PPreamble = {
@@ -2282,10 +2282,10 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     if (initPosts.nonEmpty) {
       violation(s"initEnsures clauses are no longer supported after Gobra PR #797.")
     }
-    val staticInvs: Vector[PPkgInvariant] = visitListNode[PPkgInvariant](ctx.pkgInvariant())
+    val pkgInvs: Vector[PPkgInvariant] = visitListNode[PPkgInvariant](ctx.pkgInvariant())
     val importDecls = ctx.importDecl().asScala.toVector.flatMap(visitImportDecl)
     val friendPkgs: Vector[PFriendPkgDecl] = visitListNode[PFriendPkgDecl](ctx.friendPkgDecl())
-    PPreamble(packageClause, staticInvs, importDecls, friendPkgs, pom).at(ctx)
+    PPreamble(packageClause, pkgInvs, importDecls, friendPkgs, pom).at(ctx)
   }
 
   /**

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

@@ -461,7 +461,7 @@ object Parser extends LazyLogging {
         // note that the resolveImports strategy could be embedded in e.g. a logfail strategy to report a
         // failed strategy application
         val updatedImports = rewrite(topdown(attempt(resolveImports)))(prog.imports)
-        PProgram(prog.packageClause, prog.staticInvs, updatedImports, prog.friends, prog.declarations).at(prog)
+        PProgram(prog.packageClause, prog.pkgInvariants, updatedImports, prog.friends, prog.declarations).at(prog)
       })
       // create a new package node with the updated programs
       val updatedPkg = PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info).at(pkg)
@@ -493,7 +493,7 @@ object Parser extends LazyLogging {
           case n@PTupleTerminationMeasure(_, cond) => PWildcardMeasure(cond).at(n)
           case t => t
         }
-        PFunctionSpec(spec.pres, spec.preserves, spec.posts, replacedMeasures, spec.backendAnnotations, spec.isPure, spec.isTrusted, mayBeUsedInInit = spec.mayBeUsedInInit) // TODO: drop
+        PFunctionSpec(spec.pres, spec.preserves, spec.posts, replacedMeasures, spec.backendAnnotations, spec.isPure, spec.isTrusted, mayBeUsedInInit = spec.mayBeUsedInInit)
       }
 
       val replaceTerminationMeasuresForFunctionsAndMethods: Strategy =
@@ -509,7 +509,7 @@ object Parser extends LazyLogging {
         // apply the replaceTerminationMeasuresForFunctionsAndMethods to declarations until the strategy has succeeded
         // (i.e. has reached PMember nodes) and stop then
         val updatedDecls = rewrite(alltd(replaceTerminationMeasuresForFunctionsAndMethods))(prog.declarations)
-        PProgram(prog.packageClause, prog.staticInvs, prog.imports, prog.friends, updatedDecls).at(prog)
+        PProgram(prog.packageClause, prog.pkgInvariants, prog.imports, prog.friends, updatedDecls).at(prog)
       })
       // create a new package node with the updated programs
       Right(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info).at(pkg))

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala

@@ -44,13 +44,16 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
     needsMeasureError
   }
 
+  private def pureFunctionsDoNotNeedMayInitMsg = "Pure functions and methods cannot open package invariants," +
+    "and thus, they must not be annotated with 'mayInit'."
+
   private[typing] def wellDefIfPureMethod(member: PMethodDecl): Messages = {
     if (member.spec.isPure) {
       isSingleResultArg(member) ++
         isSinglePureReturnExpr(member) ++
         isPurePostcondition(member.spec) ++
         nonVariadicArguments(member.args) ++
-        error(member, "Pure functions cannot be annotated with 'mayInit'.", member.spec.mayBeUsedInInit)
+        error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit)
     } else noMessages
   }
 
@@ -66,7 +69,7 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
         isSinglePureReturnExpr(member) ++
         isPurePostcondition(member.spec) ++
         nonVariadicArguments(member.args) ++
-        error(member, "Pure functions do not need to be annotated with 'mayInit'.", member.spec.mayBeUsedInInit)
+        error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit)
     } else noMessages
   }
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala

@@ -24,7 +24,6 @@ trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl =>
     case PFold(acc) => wellDefFoldable(acc)
     case PUnfold(acc) => wellDefFoldable(acc)
     case POpenDupPkgInv() =>
-      // TODO: do the same for opening non-dup invs
       tryEnclosingFunctionOrMethod(stmt) match {
         case Some(m) =>
           val occursInInitMember = m match {