move validMetaLenInPath() to test file

mlimbeck · Nov 22, 2023 · a68a3e7 · a68a3e7
1 parent c292a84
commit a68a3e7
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 7 deletions.
diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra
@@ -45,13 +45,6 @@ pred (b *Base) Mem() {
 	(0 < b.NumINF ==> 0 < b.NumHops)
 }
 
-ghost 
-ensures res
-decreases
-pure func validMetaLenInPath() (res bool) {
-	return MetaLen == path.MetaLen
-}
-
 ghost
 decreases
 pure func (b Base) ValidCurrInfSpec() bool {

diff --git a/pkg/slayers/path/scion/base_spec_test.gobra b/pkg/slayers/path/scion/base_spec_test.gobra
@@ -16,7 +16,18 @@
 
 package scion
 
+import (
+	"github.com/scionproto/scion/pkg/slayers/path"
+)
+
 func canAllocateBase() {
 	b := &Base{}
 	fold b.Mem()
+}
+
+ghost 
+ensures res
+decreases
+pure func validMetaLenInPath() (res bool) {
+	return MetaLen == path.MetaLen
 }