Skip to content

Implement Enums#17

Closed
tillarnold wants to merge 19 commits into
Aurel300:rewrite-2023from
tillarnold:enum
Closed

Implement Enums#17
tillarnold wants to merge 19 commits into
Aurel300:rewrite-2023from
tillarnold:enum

Conversation

@tillarnold
Copy link
Copy Markdown

@tillarnold tillarnold commented Nov 6, 2023

Replaced by #24


Builds on top of #16. To see what changed since #16 see https://github.com/tillarnold/prusti-dev/compare/rustfmt..tillarnold:prusti-dev:enum

This adds support for enums to new prusti, pure (snapshots) as well as impure (predicates).
I refactored mk_structlike to extract the different parts into functions that i can then reuse for mk_enum.

TODO:

  • test pure (currently not possible due to goto issue)
  • creating instances of enums in pure functions

@JonasAlaif
Copy link
Copy Markdown
Collaborator

This can't be used as is, please replay the changes without the cargo fmt once you have time :)

@tillarnold
Copy link
Copy Markdown
Author

@JonasAlaif with all the other changes that happened to the type encoder I'm not able to just replay the changes on the main branch. I will recreate this manually on top of the current branch without the fmt run but it'll take a bit more effort than just a rebase.

@tillarnold tillarnold closed this Nov 15, 2023
@tillarnold tillarnold mentioned this pull request Nov 15, 2023
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