tiny changes

pkg/addr/fmt.go

@@ -27,6 +27,7 @@ import (
 // ParseFormattedIA parses an IA that was formatted with the FormatIA function.
 // The same options must be provided to successfully parse.
 // @ trusted
+// @ requires false
 func ParseFormattedIA(ia string, opts ...FormatOption) (IA, error) {
 	parts := strings.Split(ia, "-")
 	if len(parts) != 2 {
@@ -46,6 +47,7 @@ func ParseFormattedIA(ia string, opts ...FormatOption) (IA, error) {
 // ParseFormattedISD parses an ISD number that was formatted with the FormatISD
 // function. The same options must be provided to successfully parse.
 // @ trusted
+// @ requires false
 func ParseFormattedISD(isd string, opts ...FormatOption) (ISD, error) {
 	o := applyFormatOptions(opts)
 	if o.defaultPrefix {
@@ -75,6 +77,7 @@ func ParseFormattedAS(as_ string, opts ...FormatOption) (AS, error) {
 
 // FormatIA formats the ISD-AS.
 // @ trusted
+// @ requires false
 func FormatIA(ia IA, opts ...FormatOption) string {
 	o := applyFormatOptions(opts)
 	as_ := fmtAS(ia.AS(), o.separator)
@@ -86,6 +89,7 @@ func FormatIA(ia IA, opts ...FormatOption) string {
 
 // FormatISD formats the ISD number.
 // @ trusted
+// @ requires false
 func FormatISD(isd ISD, opts ...FormatOption) string {
 	o := applyFormatOptions(opts)
 	if o.defaultPrefix {
@@ -96,6 +100,7 @@ func FormatISD(isd ISD, opts ...FormatOption) string {
 
 // FormatAS formats the AS number.
 // @ trusted
+// @ requires false
 func FormatAS(as_ AS, opts ...FormatOption) string {
 	o := applyFormatOptions(opts)
 	s := fmtAS(as_, o.separator)
@@ -150,6 +155,7 @@ type formatOptions struct {
 }
 
 // @ trusted
+// @ requires false
 func applyFormatOptions(opts []FormatOption) formatOptions {
 	o := formatOptions{
 		defaultPrefix: false,
@@ -164,6 +170,7 @@ func applyFormatOptions(opts []FormatOption) formatOptions {
 // WithDefaultPrefix enables the default prefix which depends on the type. For
 // the AS number, the prefix is 'AS'. For the ISD number, the prefix is 'ISD'.
 // @ trusted
+// @ requires false
 func WithDefaultPrefix() FormatOption {
 	return func(o *formatOptions) {
 		o.defaultPrefix = true
@@ -173,6 +180,7 @@ func WithDefaultPrefix() FormatOption {
 // WithSeparator sets the separator to use for formatting AS numbers. In case of
 // the empty string, the ':' is used.
 // @ trusted
+// @ requires false
 func WithSeparator(separator string) FormatOption {
 	return func(o *formatOptions) {
 		o.separator = separator
@@ -181,6 +189,7 @@ func WithSeparator(separator string) FormatOption {
 
 // WithFileSeparator returns an option that sets the separator to underscore.
 // @ trusted
+// @ requires false
 func WithFileSeparator() FormatOption {
 	return WithSeparator("_")
 }

verification/dependencies/strings/builder.gobra

@@ -34,10 +34,6 @@ ensures   err == nil
 decreases _
 func (b *Builder) WriteString(s string) (n int, err error)
 
-requires b.Mem()
-decreases _
-func (b *Builder) String() string
-
 ghost
 requires acc(b)
 requires *b === Builder{}