From f5ca8115d40fdc898dcb3bc60b17097c1becf2a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 11 Jan 2024 22:20:33 +0100 Subject: [PATCH] fix tests --- src/main/resources/stubs/net/ip.gobra | 1 + src/main/resources/stubs/net/net.gobra | 3 +++ src/main/resources/stubs/strings/strings.gobra | 3 +++ src/main/resources/stubs/sync/mutex.gobra | 1 + src/main/resources/stubs/sync/waitgroup.gobra | 1 + src/test/scala/viper/gobra/GobraPackageTests.scala | 2 +- .../scala/viper/gobra/erasing/GhostErasureUnitTests.scala | 2 +- .../scala/viper/gobra/reporting/StatsCollectorTests.scala | 4 ++-- 8 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/main/resources/stubs/net/ip.gobra b/src/main/resources/stubs/net/ip.gobra index f6a3ee897..0c177d6bc 100644 --- a/src/main/resources/stubs/net/ip.gobra +++ b/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. diff --git a/src/main/resources/stubs/net/net.gobra b/src/main/resources/stubs/net/net.gobra index d1d1ff11e..0319d37dd 100644 --- a/src/main/resources/stubs/net/net.gobra +++ b/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 diff --git a/src/main/resources/stubs/strings/strings.gobra b/src/main/resources/stubs/strings/strings.gobra index 0307bf577..140ee75d5 100644 --- a/src/main/resources/stubs/strings/strings.gobra +++ b/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,6 +178,7 @@ 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) } @@ -184,6 +186,7 @@ func HasPrefix(s, prefix string) (ret bool) { // 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 } diff --git a/src/main/resources/stubs/sync/mutex.gobra b/src/main/resources/stubs/sync/mutex.gobra index 9f400718c..94f4a2d2f 100644 --- a/src/main/resources/stubs/sync/mutex.gobra +++ b/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 diff --git a/src/main/resources/stubs/sync/waitgroup.gobra b/src/main/resources/stubs/sync/waitgroup.gobra index 2de127d4d..3531a90bc 100644 --- a/src/main/resources/stubs/sync/waitgroup.gobra +++ b/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 diff --git a/src/test/scala/viper/gobra/GobraPackageTests.scala b/src/test/scala/viper/gobra/GobraPackageTests.scala index 4fb362995..f889fe9de 100644 --- a/src/test/scala/viper/gobra/GobraPackageTests.scala +++ b/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 diff --git a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala index dd203575a..d71f9f84a 100644 --- a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala +++ b/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") diff --git a/src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala b/src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala index 25980a22a..421d30da1 100644 --- a/src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala +++ b/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) }