drop unnecessary param in IsValidResultOfDecoding

viperproject · Jan 9, 2025 · b37959e · b37959e
1 parent 84ea83b
commit b37959e
Show file tree

Hide file tree

Showing 7 changed files with 8 additions and 8 deletions.
diff --git a/pkg/slayers/path/empty/empty_spec.gobra b/pkg/slayers/path/empty/empty_spec.gobra
@@ -37,7 +37,7 @@ func (e Path) DowngradePerm(buf []byte) {
 ghost
 pure
 decreases
-func (p Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+func (p Path) IsValidResultOfDecoding(b []byte) bool {
 	return true
 }
 

diff --git a/pkg/slayers/path/epic/epic_spec.gobra b/pkg/slayers/path/epic/epic_spec.gobra
@@ -102,7 +102,7 @@ pure func (p *Path) GetUnderlyingScionPathBuf(buf []byte) []byte {
 ghost
 pure
 decreases
-func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+func (p *Path) IsValidResultOfDecoding(b []byte) (res bool) {
 	return true
 }
 

diff --git a/pkg/slayers/path/onehop/onehop_spec.gobra b/pkg/slayers/path/onehop/onehop_spec.gobra
@@ -54,7 +54,7 @@ pure func (o *Path) InferSizeUb(ghost ub []byte) (b bool) {
 ghost
 pure
 decreases
-func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+func (p *Path) IsValidResultOfDecoding(b []byte) (res bool) {
 	return true
 }
 

diff --git a/pkg/slayers/path/path.go b/pkg/slayers/path/path.go
@@ -83,17 +83,17 @@ type Path interface {
 	//@ requires  NonInitMem()
 	//@ preserves acc(sl.Bytes(b, 0, len(b)), R42)
 	//@ ensures   err == nil ==> Mem(b)
+	//@ ensures   err == nil ==> IsValidResultOfDecoding(b)
 	//@ ensures   err != nil ==> err.ErrorMem()
 	//@ ensures   err != nil ==> NonInitMem()
-	//@ ensures   err == nil ==> IsValidResultOfDecoding(b, err)
 	//@ decreases
 	DecodeFromBytes(b []byte) (err error)
 	//@ ghost
 	//@ pure
 	//@ requires Mem(b)
 	//@ requires acc(sl.Bytes(b, 0, len(b)), R42)
 	//@ decreases
-	//@ IsValidResultOfDecoding(b []byte, err error) (res bool)
+	//@ IsValidResultOfDecoding(b []byte) bool
 	// Reverse reverses a path such that it can be used in the reversed direction.
 	// XXX(shitz): This method should possibly be moved to a higher-level path manipulation package.
 	//@ requires  Mem(ub)

diff --git a/pkg/slayers/path/path_spec.gobra b/pkg/slayers/path/path_spec.gobra
@@ -40,7 +40,7 @@ func (p *rawPath) DowngradePerm(ghost buf []byte) {
 ghost
 pure
 decreases
-func (p *rawPath) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+func (p *rawPath) IsValidResultOfDecoding(b []byte) bool {
 	return true
 }
 

diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra
@@ -25,7 +25,7 @@ import (
 ghost
 pure
 decreases
-func (p *Decoded) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+func (p *Decoded) IsValidResultOfDecoding(b []byte) (res bool) {
 	return true
 }
 

diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra
@@ -46,7 +46,7 @@ pure
 requires  acc(s.Mem(buf), _)
 requires  acc(sl.Bytes(buf, 0, len(buf)), R42)
 decreases
-func (s *Raw) IsValidResultOfDecoding(buf []byte, err error) (res bool) {
+func (s *Raw) IsValidResultOfDecoding(buf []byte) (res bool) {
 	return let base := s.GetBase(buf) in
 		base.EqAbsHeader(buf) &&
 		base.WeaklyValid()