Skip to content

Proper encoding of uninhabited types (WIP)#107

Merged
Aurel300 merged 4 commits into
Aurel300:rewrite-2023from
zgrannan:zgrannan/uninhabited
Oct 3, 2025
Merged

Proper encoding of uninhabited types (WIP)#107
Aurel300 merged 4 commits into
Aurel300:rewrite-2023from
zgrannan:zgrannan/uninhabited

Conversation

@zgrannan
Copy link
Copy Markdown

@zgrannan zgrannan commented Oct 3, 2025

Still need to clean this up a bit but it appears to work.

This builds on top of #106 which should be merged first

139 failed; 142 passed (+10 compared to #106)

Comment thread prusti-encoder/src/encoders/ty/data.rs Outdated
let fields = self.fields.iter().zip(other.fields.iter());
StructData {
data: (&self.data, &other.data),
inhabited: self.inhabited || other.inhabited,
Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think zip should always combine two different representations of the same type (@JonasAlaif correct me if I'm wrong), so this should rather be an assertion that the two values are equal, like the one for the number of fields at the beginning of this function.

@Aurel300 Aurel300 force-pushed the zgrannan/uninhabited branch from b8f087c to c875dfb Compare October 3, 2025 09:05
Comment thread prusti-encoder/src/encoders/ty/rust_ty.rs Outdated
@Aurel300 Aurel300 marked this pull request as ready for review October 3, 2025 09:48
@Aurel300 Aurel300 merged commit 80cf1e6 into Aurel300:rewrite-2023 Oct 3, 2025
5 of 6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants