maybe bogus: cannot access any field of a datatype where one or more fields are private

[jonhnet]

I can't figure out what the visibility complaint here means.

+ /home/jonh/verus/source/target-verus/release/verus --time src/bundle.rs
error: in pub open spec function, cannot access any field of a datatype where one or more fields are private
   --> src/marshalling/SeqMarshalling_v.rs:358:11
    |
358 | ...   ((self.total_size - Self::spec_size_of_length_field()) / (self.config.spec_uni...
    |         ^^^^^^^^^^^^^^^

2024-01-08-16-29-29.zip

I am presently working around this by closing all the spec fns it's complaining about, but that may make verification an undue burden.

Note the enclosed code requires the trait-default branch of Verus.

[jonhnet]

This was user error. I had the struct pub, but forgot that (unlike traits and enums) I had an obligation to also put pub adjectives on the fields of the struct. Thank you.

However, it might be helpful to enhance this error message to identify one or more non-pub fields. Something like "struct Foo has non-pub fields x, y, z, ...". In the fullness of time, perhaps a Rust-like suggestion inserting 'pub' into the field declaration.

[utaal-b]

Moved to #387 (comment)