-
Notifications
You must be signed in to change notification settings - Fork 8
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
feat: add SimpleBlob TestModel for Rust #353
Conversation
4997cbb
to
925daef
Compare
TestModels/SimpleTypes/SimpleBlob/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
Outdated
Show resolved
Hide resolved
fa72165
to
b2aaa32
Compare
TestModels/SimpleTypes/SimpleBlob/runtimes/rust/src/operation/get_blob/_get_blob_input.rs
Outdated
Show resolved
Hide resolved
TestModels/SimpleTypes/SimpleBlob/runtimes/rust/tests/simple_blob_test.rs
Outdated
Show resolved
Hide resolved
TestModels/SimpleTypes/SimpleBlob/runtimes/rust/src/operation/get_blob/_get_blob_input.rs
Show resolved
Hide resolved
dafny_value.value().Extract().to_array(), | ||
)) | ||
Some( | ||
::std::rc::Rc::try_unwrap(dafny_value.value().Extract().to_array()) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks like the right approach AFAICT. I'm not 100% sure it's the best we can do in the limit, but I am sure that it's much easier to optimize this kind of thing once we're actually generating the code, so it should be very quick to fix if we do realize we can do better latter. E.g. we may want to add this conversion to the Dafny Rust runtime.
Please import the generated file and I can help you generate the future files after #368 (need to install Dafny locally, on the branch feat-rust, and then run |
93252f8
to
9f41c1b
Compare
Description of changes:
adds
SimpleBlob
test modelBy submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.