remove one more assumption

jcp19 · jcp19 · commit 07e0993aa521 · 2025-09-28T14:22:21.000+02:00
diff --git a/pkg/slayers/path/scion/base.go b/pkg/slayers/path/scion/base.go
@@ -137,9 +137,7 @@ func (s *Base) DecodeFromBytes(data []byte) (r error) {
 		if s.PathMeta.SegLen[i] > 0 && s.NumINF == 0 {
 			s.NumINF = i + 1
 		}
-		// (VerifiedSCION) Cannot assert bounds of uint:
-		// https://github.com/viperproject/gobra/issues/192
-		//@ assume int(s.PathMeta.SegLen[i]) >= 0
+		//@ assert 0 <= int(s.PathMeta.SegLen[i])
 		s.NumHops += int(s.PathMeta.SegLen[i])
 	}
 	// We must check the validity of NumHops. It is possible to fit more than 64 hops in

Original file line number	Diff line number	Diff line change
`@@ -137,9 +137,7 @@ func (s *Base) DecodeFromBytes(data []byte) (r error) {`
`137`	`137`	`if s.PathMeta.SegLen[i] > 0 && s.NumINF == 0 {`
`138`	`138`	`s.NumINF = i + 1`
`139`	`139`	`}`
`140`		`- // (VerifiedSCION) Cannot assert bounds of uint:`
`141`		`- // https://github.com/viperproject/gobra/issues/192`
`142`		`- //@ assume int(s.PathMeta.SegLen[i]) >= 0`
	`140`	`+ //@ assert 0 <= int(s.PathMeta.SegLen[i])`
`143`	`141`	`s.NumHops += int(s.PathMeta.SegLen[i])`
`144`	`142`	`}`
`145`	`143`	`// We must check the validity of NumHops. It is possible to fit more than 64 hops in`