fix tests

src/main/resources/stubs/net/ip.gobra

@@ -144,6 +144,7 @@ func (ip IP) To4() (res IP) {
 
 pure
 preserves forall i int :: 0 <= i && i < len(s) ==> acc(&s[i], 1/100000)
+decreases _
 func isZeros(s []byte) bool
 
 // To16 converts the IP address ip to a 16-byte representation.

src/main/resources/stubs/net/net.gobra

@@ -171,6 +171,7 @@ pred (op *OpError) Mem() {
 }
 
 requires acc(e.Mem(), _)
+decreases
 pure func (e *OpError) Unwrap() error { return unfolding acc(e.Mem(), _) in e.Err }
 
 requires acc(e.Mem())
@@ -271,8 +272,10 @@ type UnknownNetworkError string
 
 func (e UnknownNetworkError) Error() string   // { return "unknown network " + string(e) }
 ensures !res
+decreases
 pure func (e UnknownNetworkError) Timeout() (res bool)   { return false }
 ensures !res
+decreases
 pure func (e UnknownNetworkError) Temporary() (res bool) { return false }
 
 type InvalidAddrError string

src/main/resources/stubs/strings/strings.gobra

@@ -151,6 +151,7 @@ ensures len(elems) == 0 ==> res == ""
 ensures len(elems) == 1 ==> res == elems[0]
 // (joao) Leads to precondition of call might not hold (permission to elems[i] might not suffice)
 // ensures len(elems) > 1 ==> res == elems[0] + sep + Join(elems[1:], sep)
+decreases _
 pure func Join(elems []string, sep string) (res string) /*{
 	switch len(elems) {
 	case 0:
@@ -177,13 +178,15 @@ pure func Join(elems []string, sep string) (res string) /*{
 // HasPrefix tests whether the string s begins with prefix.
 pure
 ensures ret == (len(s) >= len(prefix) && s[0:len(prefix)] == prefix)
+decreases _
 func HasPrefix(s, prefix string) (ret bool) {
 	return len(s) >= len(prefix) && (s[0:len(prefix)] == prefix)
 }
 
 // HasSuffix tests whether the string s ends with suffix.
 pure
 ensures ret == (len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix)
+decreases _
 func HasSuffix(s, suffix string) (ret bool) {
 	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
 }

src/main/resources/stubs/sync/mutex.gobra

@@ -14,6 +14,7 @@ pred (m *Mutex) UnlockP()
 
 ghost
 requires acc(m.LockP(), _)
+decreases _
 pure func (m *Mutex) LockInv() pred()
 
 ghost

src/main/resources/stubs/sync/waitgroup.gobra

@@ -17,6 +17,7 @@ pred (wg *WaitGroup) Token(t pred())
 
 ghost
 requires acc(g.WaitGroupP(), _)
+decreases _
 pure func (g *WaitGroup) WaitMode() bool
 
 ghost

src/test/scala/viper/gobra/GobraPackageTests.scala

@@ -65,7 +65,7 @@ class GobraPackageTests extends GobraTests {
             "-I", currentDir.toFile.getPath,
             // termination checks in functions are currently disabled in the tests. This can be enabled in the future,
             // but requires some work to add termination measures all over the test suite.
-            disableCheckTerminationPureFns = true,
+            "--disableTermCheckPureFns",
           ))
         } yield config
 

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

@@ -341,7 +341,7 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
         new PackageInfo("pkg", "pkg", false)
       )
       val tree = new Info.GoTree(pkg)
-      val config = Config()
+      val config = Config(disableCheckTerminationPureFns = true)
       val info = new TypeInfoImpl(tree, Map.empty)(config)
       info.errors match {
         case Vector(msgs) => fail(s"Type-checking failed: $msgs")

src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala

@@ -32,12 +32,12 @@ class StatsCollectorTests extends AnyFunSuite with BeforeAndAfterAll {
   }
 
   test("Integration without chopper") {
-    val config = createConfig(Array("--recursive", "--projectRoot", statsCollectorTestDir, "-I", statsCollectorTestDir))
+    val config = createConfig(Array("--recursive", "--projectRoot", statsCollectorTestDir, "-I", statsCollectorTestDir, "--disableTermCheckPureFns"))
     runIntegration(config)
   }
 
   test("Integration with chopper") {
-    val config = createConfig(Array("--recursive", "--projectRoot", statsCollectorTestDir, "-I", statsCollectorTestDir, "--chop", "10"))
+    val config = createConfig(Array("--recursive", "--projectRoot", statsCollectorTestDir, "-I", statsCollectorTestDir, "--chop", "10", "--disableTermCheckPureFns"))
     runPackagesSeparately(config)
     runIntegration(config)
   }