Remove deprecated initialization postconditions (#971)

* deprecate init posts

* fix unit tests

Author: jcp19

src/main/antlr4/GobraLexer.g4

@@ -92,7 +92,6 @@ OUTLINE     : 'outline';
 DUPLICABLE  : 'dup';
 PKG_INV     : 'pkgInvariant';
 OPEN_DUP_SINV : 'openDupPkgInv' -> mode(NLSEMI);
-INIT_POST   : 'initEnsures';
 IMPORT_PRE  : 'importRequires';
 PROOF       : 'proof';
 GHOST_EQUALS     : '===';

src/main/antlr4/GobraParser.g4

@@ -35,15 +35,13 @@ friendPkgDecl: FRIENDPKG importPath assertion;
 
 // Ghost members
 sourceFile:
-  (pkgInvariant eos)* (initPost eos)* packageClause eos (friendPkgDecl eos)* (importDecl eos)* (
+  (pkgInvariant eos)* packageClause eos (friendPkgDecl eos)* (importDecl eos)* (
     member eos
   )* EOF;
 
 // `preamble` is a second entry point allowing us to parse only the top of a source.
 // That's also why we don not enforce EOF at the end.
-preamble: (pkgInvariant eos)* (initPost eos)* packageClause eos (friendPkgDecl eos)* (importDecl eos)*;
-
-initPost: INIT_POST expression;
+preamble: (pkgInvariant eos)* packageClause eos (friendPkgDecl eos)* (importDecl eos)*;
 
 importPre: IMPORT_PRE expression;
 

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

@@ -54,8 +54,6 @@ case class PPackage(
 case class PProgram(
                      packageClause: PPackageClause,
                      pkgInvariants: Vector[PPkgInvariant],
-                     @deprecated("Init postconditions were deprecated in PR #797 and will soon be completely removed.")
-                     initPosts: Vector[PExpression],
                      imports: Vector[PImport],
                      friends: Vector[PFriendPkgDecl],
                      declarations: Vector[PMember]
@@ -65,8 +63,6 @@ case class PProgram(
 case class PPreamble(
                       packageClause: PPackageClause,
                       pkgInvariants: Vector[PPkgInvariant],
-                      @deprecated("Init postconditions were deprecated in PR #797 and will soon be completely removed.")
-                      initPosts: Vector[PExpression],
                       imports: Vector[PImport],
                       friends: Vector[PFriendPkgDecl],
                       positions: PositionManager,

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

@@ -63,17 +63,15 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   // program
 
   def showProgram(p: PProgram): Doc = p match {
-    // initPosts not shown, they are deprecated and will soon be removed
-    case PProgram(packageClause, pkgInvs, _, imports, friends, declarations) =>
+    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 {
-    // initPosts not shown, they are deprecated and will soon be removed
-    case PPreamble(packageClause, pkgInvs, _, imports, friends, _) =>
+    case PPreamble(packageClause, pkgInvs, imports, friends, _) =>
       showPreamble(packageClause, pkgInvs, imports, friends)
   }
 

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

@@ -2302,30 +2302,21 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     */
   override def visitSourceFile(ctx: GobraParser.SourceFileContext): PProgram = {
     val packageClause: PPackageClause = visitNode(ctx.packageClause())
-    val initPosts: Vector[PExpression] = visitListNode[PExpression](ctx.initPost())
     val pkgInvs: Vector[PPkgInvariant] = visitListNode[PPkgInvariant](ctx.pkgInvariant())
     val importDecls = ctx.importDecl().asScala.toVector.flatMap(visitImportDecl)
     val friendPkgs: Vector[PFriendPkgDecl] = visitListNode[PFriendPkgDecl](ctx.friendPkgDecl())
     val members = ctx.member().asScala.toVector.flatMap(visitMember)
-    PProgram(packageClause, pkgInvs, initPosts, importDecls, friendPkgs, members).at(ctx)
+    PProgram(packageClause, pkgInvs, importDecls, friendPkgs, members).at(ctx)
   }
 
   override def visitPreamble(ctx: GobraParser.PreambleContext): PPreamble = {
     val packageClause: PPackageClause = visitNode(ctx.packageClause())
-    val initPosts: Vector[PExpression] = visitListNode[PExpression](ctx.initPost())
     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, pkgInvs, initPosts, importDecls, friendPkgs, pom).at(ctx)
+    PPreamble(packageClause, pkgInvs, importDecls, friendPkgs, pom).at(ctx)
   }
 
-  /**
-    * Visists an init postcondition
-    * @param ctx the parse tree
-    * @return the positioned PPackageclause
-    */
-  override def visitInitPost(ctx: InitPostContext): PExpression = visitNode[PExpression](ctx.expression())
-
   /**
    * Visits a pkgInvariant
    *

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

@@ -460,7 +460,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.pkgInvariants, prog.initPosts, 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)
@@ -508,7 +508,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.pkgInvariants, prog.initPosts, 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/ProgramTyping.scala

@@ -18,13 +18,10 @@ import viper.gobra.util.{Computation, Violation}
 trait ProgramTyping extends BaseTyping { this: TypeInfoImpl =>
 
   lazy val wellDefProgram: WellDefinedness[PProgram] = createWellDef {
-    case PProgram(_, _, initPosts, _, _, _) if initPosts.nonEmpty =>
-      error(initPosts.head, "'initEnsures' clauses are now deprecated." +
-        " Consider using 'pkgInvariant' clauses instead.")
-    case PProgram(_, _, _, _, friends, _) if !config.enableExperimentalFriendClauses && friends.nonEmpty =>
+    case PProgram(_, _, _, friends, _) if !config.enableExperimentalFriendClauses && friends.nonEmpty =>
       error(friends.head, "Usage of experimental 'friendPkg' clauses is disallowed by default. " +
         "Pass the flag --experimentalFriendClauses to allow it. This feature may change in the future.")
-    case prog@PProgram(_, pkgInvs, _, _, friends, _) =>
+    case prog@PProgram(_, pkgInvs,  _, friends, _) =>
       // Obtains global variable declarations sorted by the order in which they appear in the file
       val sortedByPosDecls: Vector[PVarDecl] = globalVarDeclsSortedByPos(prog)
       // HACK: without this explicit check, Gobra does not find repeated declarations

src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala

@@ -378,7 +378,6 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
       Vector.empty,
       Vector.empty,
       Vector.empty,
-      Vector.empty,
       Vector(PFunctionDecl(
         PIdnDef("foo"),
         inArgs.map(_._1),
@@ -417,7 +416,7 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
       val program = stubProgram(inArgs, stmt)
       val ghostLess = ghostLessProg(program)
       val block = ghostLess match {
-        case PProgram(_, _, _, _, _, Vector(PFunctionDecl(PIdnDef("foo"), _, _, _, Some((_, b))))) => b
+        case PProgram(_, _, _, _, Vector(PFunctionDecl(PIdnDef("foo"), _, _, _, Some((_, b))))) => b
         case p => fail(s"Parsing succeeded but with an unexpected program $p")
       }
       normalize(block.stmts) match {

src/test/scala/viper/gobra/typing/ExprTypingUnitTests.scala

@@ -3367,7 +3367,6 @@ class ExprTypingUnitTests extends AnyFunSuite with Matchers with Inside {
       Vector(),
       Vector(),
       Vector(),
-      Vector(),
       Vector(PMethodDecl(
         PIdnDef("foo"),
         PUnnamedReceiver(PMethodReceiveName(PNamedOperand(PIdnUse("self")))),

src/test/scala/viper/gobra/typing/MemberTypingUnitTests.scala

@@ -85,7 +85,6 @@ class MemberTypingUnitTests extends AnyFunSuite with Matchers with Inside {
         Vector(),
         Vector(),
         Vector(),
-        Vector(),
         members
       )
       (prog, idnUse.map(_ => idnDefX))