Update pkg/slayers/scion_spec.gobra

viperproject · Jan 7, 2025 · 1226e2b · 1226e2b
1 parent f934d8d
commit 1226e2b
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra
@@ -810,8 +810,5 @@ ensures  b
 decreases
 pure func (s *SCION) ValidSizeOhpUb(ub []byte) (b bool) {
 	return unfolding s.Mem(ub) in
-		// let pathSlice := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
-		// let pathLen := s.Path.LenSpec(pathSlice) in
-		// CmnHdrLen + s.AddrHdrLenSpecInternal() + pathLen <= len(ub)
 		s.ValidSizeOhpUbOpenInv(ub)
 }