Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for multiset update in rust #5700

Open
kbuaaaaaa opened this issue Aug 15, 2024 · 1 comment
Open

Support for multiset update in rust #5700

kbuaaaaaa opened this issue Aug 15, 2024 · 1 comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny priority: not yet Will reconsider working on this when we're looking for work

Comments

@kbuaaaaaa
Copy link
Contributor

Dafny version

4.7.0

Code to produce this issue

method Main(){
  var v0 := multiset{1,2,3};
  v0 := v0[3 := 0];
  print v0;
}

Command to run and resulting output

dafny run -t rs main.dfy

Dafny program verifier finished with 1 verified, 0 errors
(0,-1): Error: Microsoft.Dafny.UnsupportedInvalidOperationException: <i>EmitIndexCollectionUpdate for multiset<int></i>

What happened?

No support for updating multiset in Rust.

What type of operating system are you experiencing the problem on?

Linux, Mac

@kbuaaaaaa kbuaaaaaa added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Aug 15, 2024
@kbuaaaaaa kbuaaaaaa changed the title Support for multisite update in rust Support for multiset update in rust Aug 15, 2024
@MikaelMayer MikaelMayer added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny priority: not yet Will reconsider working on this when we're looking for work and removed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label labels Aug 15, 2024
@MikaelMayer
Copy link
Member

The Rust code generator is not officially available yet and under construction.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny priority: not yet Will reconsider working on this when we're looking for work
Projects
None yet
Development

No branches or pull requests

2 participants