cleanup tests

viperproject · Jan 29, 2025 · eddaf6a · eddaf6a
1 parent e92f444
commit eddaf6a
Show file tree

Hide file tree

Showing 10 changed files with 26 additions and 125 deletions.
diff --git a/src/test/resources/regressions/features/globals/scion-like01.go b/src/test/resources/regressions/features/globals/scion-like01.go
diff --git a/src/test/resources/regressions/features/globals/scion-like02.go b/src/test/resources/regressions/features/globals/scion-like02.go
diff --git a/src/test/resources/regressions/features/globals/scion-like03.go b/src/test/resources/regressions/features/globals/scion-like03.go
diff --git a/...ckage/pkg_init/monotonicset/bounded.gobra → .../globals/scion/monotonicset/bounded.gobra b/...ckage/pkg_init/monotonicset/bounded.gobra → .../globals/scion/monotonicset/bounded.gobra
diff --git a/...kage/pkg_init/scion/path/onehop/onehop.go → ...tures/globals/scion/path/onehop/onehop.go b/...kage/pkg_init/scion/path/onehop/onehop.go → ...tures/globals/scion/path/onehop/onehop.go
@@ -3,9 +3,9 @@
 
 package onehop
 
-// ##(-I ../../..)
+// ##(-I ../../)
 
-import "scion/path"
+import "path"
 
 const PathType path.Type = 2
 

diff --git a/.../same_package/pkg_init/scion/path/path.go → ...sions/features/globals/scion/path/path.go b/.../same_package/pkg_init/scion/path/path.go → ...sions/features/globals/scion/path/path.go
@@ -3,7 +3,7 @@
 
 package path
 
-// ##(-I ../../)
+// ##(-I ../)
 
 // This approach is sound, assuming that the paths below are unique per a package.
 // This assumption is not problematic, and is similar to the assumption we make for
@@ -14,6 +14,23 @@ package path
 
 // @ import "monotonicset"
 
+/*@
+
+pred PkgInv() {
+	acc(&registeredPaths) &&
+	registeredKeys.Inv()  &&
+	(forall i uint16 :: 0 <= i && i < maxPathType ==>
+		registeredPaths[i].inUse == registeredKeys.FContains(i))
+}
+
+ghost
+decreases
+pure func RegisteredTypes() monotonicset.BoundedMonotonicSet {
+	return registeredKeys
+}
+
+@*/
+
 const maxPathType = 256
 
 var registeredPaths /*@@@*/ [maxPathType]metadata

diff --git a/...package/pkg_init/scion/path/scion/base.go → ...features/globals/scion/path/scion/base.go b/...package/pkg_init/scion/path/scion/base.go → ...features/globals/scion/path/scion/base.go
@@ -3,9 +3,9 @@
 
 package scion
 
-// ##(-I ../../..)
+// ##(-I ../../)
 
-import "scion/path"
+import "path"
 
 const PathType path.Type = 1
 

diff --git a/...rces/same_package/pkg_init/scion/scion.go → ...gressions/features/globals/scion/scion.go b/...rces/same_package/pkg_init/scion/scion.go → ...gressions/features/globals/scion/scion.go
@@ -7,7 +7,7 @@
 
 package scion
 
-// ##(-I ..)
+// ##(-I .)
 
 // Example inspired by how PathTypes are registered in the SCION border router.
 // Based on https://github.com/viperproject/VerifiedSCION/tree/master/pkg/slayers/scion.go
@@ -19,9 +19,9 @@ import (
 	// @ importRequires path.PkgInv()
 	// @ importRequires path.RegisteredTypes().DoesNotContain(1) &&
 	// @ 	path.RegisteredTypes().DoesNotContain(2)
-	// @ "scion/path"
-	"scion/path/onehop"
-	"scion/path/scion"
+	// @ "path"
+	"path/onehop"
+	"path/scion"
 )
 
 // We should introduce preconditions and postconditions to this function to guarantee that

diff --git a/src/test/resources/same_package/pkg_init/scion/path/path_spec.gobra b/src/test/resources/same_package/pkg_init/scion/path/path_spec.gobra
diff --git a/src/test/resources/same_package/pkg_init/scion/scion_spec.gobra b/src/test/resources/same_package/pkg_init/scion/scion_spec.gobra