Method Wellformedness

[viper-admin]

Created by @arquintl on 2020-06-19 07:38 Last updated on 2020-06-19 07:44

Check that methods do not have the same name as fields

This is invalid:

type Rectangle struct {
    Width, Height int
}

ghost
requires acc(r.Width)
ensures acc(r.Width)
pure func (r *Rectangle) Width() (res int) {
    return r.Width
}

‌

[viper-admin]

@arquintl on 2020-06-19 07:44:

• edited the description

[viper-admin]

@arquintl on 2020-06-19 07:44:

• edited the description

[Felalolf]

it detects that something is incorrect, but the error messages are not good.