backup

viperproject · Dec 18, 2024 · 4a7b5b9 · 4a7b5b9
1 parent ff165ba
commit 4a7b5b9
Show file tree

Hide file tree

Showing 6 changed files with 41 additions and 15 deletions.
diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala
@@ -896,7 +896,7 @@ case class PFunctionSpec(
                           isPure: Boolean = false,
                           isTrusted: Boolean = false,
                           isOpaque: Boolean = false,
-                          mayBeUsedInInit: Boolean,
+                          mayBeUsedInInit: Boolean = false,
                       ) extends PSpecification
 
 case class PBackendAnnotation(key: String, values: Vector[String]) extends PGhostMisc

diff --git a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala
@@ -321,13 +321,14 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
 
     def stubProgram(inArgs: Vector[(PParameter, Boolean)], body : PStatement) : PProgram = PProgram(
       PPackageClause(PPkgDef("pkg")),
-      Vector(),
-      Vector(),
+      Vector.empty,
+      Vector.empty,
+      Vector.empty,
       Vector(PFunctionDecl(
         PIdnDef("foo"),
         inArgs.map(_._1),
         PResult(Vector()),
-        PFunctionSpec(Vector(), Vector(), Vector(), Vector.empty, Vector.empty),
+        PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty),
         Some(PBodyParameterInfo(inArgs.collect{ case (n: PNamedParameter, true) => PIdnUse(n.id.name) }), PBlock(Vector(body)))
       ))
     )
@@ -361,7 +362,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 {

diff --git a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
@@ -120,13 +120,13 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside {
 
   test("Parser: spec only function") {
     frontend.parseFunctionDecl("func foo() { b.bar() }", specOnly = true) should matchPattern {
-      case PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None) =>
+      case PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false, false), None) =>
     }
   }
 
   test("Parser: spec only function with nested blocks") {
     frontend.parseFunctionDecl("func foo() { if(true) { b.bar() } else { foo() } }", specOnly = true) should matchPattern {
-      case PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None) =>
+      case PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false, false), None) =>
     }
   }
 
@@ -159,7 +159,7 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside {
     val modes: Set[Boolean] = Set(false, true)
     modes.foreach(specOnly => {
       frontend.parseFunctionDecl("func bar()", specOnly) should matchPattern {
-        case PFunctionDecl(PIdnDef("bar"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None) =>
+        case PFunctionDecl(PIdnDef("bar"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false, false), None) =>
       }
     })
   }
@@ -2642,20 +2642,42 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside {
   }
 
   test("Parser: should be able to parse normal termination measure") {
-    frontend.parseFunctionDecl("decreases n; func factorial (n int) int") should matchPattern {
-      case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), None)), Vector(), false, false, false), None) =>
-    }
+    val expected = PFunctionDecl(
+      PIdnDef("factorial"),
+      Vector(PNamedParameter(PIdnDef("n"), PIntType())),
+      PResult(Vector(PUnnamedParameter(PIntType()))),
+      PFunctionSpec(
+        Vector.empty,
+        Vector.empty,
+        Vector.empty,
+        Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), None)),
+        Vector.empty,
+      ),
+      None
+    )
+    frontend.parseFunctionDecl("decreases n; func factorial (n int) int") should equal (expected)
   }
 
   test("Parser: should be able to parse underscore termination measure") {
-    frontend.parseFunctionDecl("decreases _; func factorial (n int) int") should matchPattern {
-      case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PWildcardMeasure(None)), Vector(), false, false, false), None) =>
-    }
+    val expected = PFunctionDecl(
+      PIdnDef("factorial"),
+      Vector(PNamedParameter(PIdnDef("n"), PIntType())),
+      PResult(Vector(PUnnamedParameter(PIntType()))),
+      PFunctionSpec(
+        Vector.empty,
+        Vector.empty,
+        Vector.empty,
+        Vector(PWildcardMeasure(None)),
+        Vector.empty,
+      ),
+      None
+    )
+    frontend.parseFunctionDecl("decreases _; func factorial (n int) int") should equal (expected)
   }
 
   test("Parser: should be able to parse conditional termination measure" ) {
     frontend.parseFunctionDecl("decreases n if n>1; decreases _ if n<2; func factorial (n int) int") should matchPattern {
-      case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), Some(PGreater(PNamedOperand(PIdnUse("n")), PIntLit(one, Decimal)))), PWildcardMeasure(Some(PLess(PNamedOperand(PIdnUse("n")), PIntLit(two, Decimal))))), Vector(), false, false, false), None) if one == 1 && two == 2 =>
+      case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), Some(PGreater(PNamedOperand(PIdnUse("n")), PIntLit(one, Decimal)))), PWildcardMeasure(Some(PLess(PNamedOperand(PIdnUse("n")), PIntLit(two, Decimal))))), Vector(), false, false, false, false), None) if one == 1 && two == 2 =>
     }
   }
 

diff --git a/src/test/scala/viper/gobra/typing/ExprTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/ExprTypingUnitTests.scala
@@ -3366,6 +3366,7 @@ class ExprTypingUnitTests extends AnyFunSuite with Matchers with Inside {
       PPackageClause(PPkgDef("pkg")),
       Vector(),
       Vector(),
+      Vector(),
       Vector(PMethodDecl(
         PIdnDef("foo"),
         PUnnamedReceiver(PMethodReceiveName(PNamedOperand(PIdnUse("self")))),

diff --git a/src/test/scala/viper/gobra/typing/StmtTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/StmtTypingUnitTests.scala
@@ -62,6 +62,7 @@ class StmtTypingUnitTests extends AnyFunSuite with Matchers with Inside {
         PPackageClause(PPkgDef("pkg")),
         Vector(),
         Vector(),
+        Vector(),
         Vector(PFunctionDecl(
           PIdnDef("foo"),
           inArgs.map(_._1),

diff --git a/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala
@@ -358,6 +358,7 @@ class TypeTypingUnitTests extends AnyFunSuite with Matchers with Inside {
       PPackageClause(PPkgDef("pkg")),
       Vector(),
       Vector(),
+      Vector(),
       Vector(PMethodDecl(
         PIdnDef("foo"),
         PUnnamedReceiver(PMethodReceiveName(PNamedOperand(PIdnUse("self")))),