pr 378

Author: jcp19

pkg/addr/host.go

@@ -15,9 +15,6 @@
 
 // +gobra
 
-// @ initEnsures ErrBadHostAddrType.ErrorMem()
-// @ initEnsures ErrMalformedHostAddrType.ErrorMem()
-// @ initEnsures ErrUnsupportedSVCAddress.ErrorMem()
 package addr
 
 import (

pkg/addr/isdas.go

@@ -127,7 +127,7 @@ func asParseBGP(s string) (retAs AS, retErr error) {
 	// @ strconv.Exp2to10(30)
 	// @ strconv.Exp2to10(20)
 	// @ strconv.Exp2to10(10)
-	// @ assert _as < strconv.Exp(2, BGPASBits)
+	// @ assert _as < uint64(strconv.Exp(2, BGPASBits))
 	return AS(_as), nil
 }
 

verification/dependencies/net/ip.gobra

@@ -85,7 +85,7 @@ func (ip IP) To4(ghost wildcard bool) (res IP) {
 }
 
 pure
-preserves forall i int :: { &s[i] } 0 <= i && i < len(s) ==> acc(&s[i], R55)
+requires forall i int :: { &s[i] } 0 <= i && i < len(s) ==> acc(&s[i], R55)
 decreases
 func isZeros(s []byte) bool
 

verification/dependencies/strconv/atoi.gobra

@@ -37,7 +37,7 @@ func Exp2to10(exp int) {
 // ParseUint is like ParseInt but for unsigned numbers.
 requires base == 0 || (2 <= base && base <= 36)
 requires bitSize > 0 && bitSize <= 64
-ensures retErr == nil ==> (ret >= 0 && ret < Exp(2, bitSize))
+ensures retErr == nil ==> (ret >= 0 && ret < uint64(Exp(2, bitSize)))
 ensures retErr != nil ==> retErr.ErrorMem()
 decreases _
 func ParseUint(s string, base int, bitSize int) (ret uint64, retErr error)