Pointerbender
Pointerbender
A small addendum, it seems this is because the assertions do not (always?) seem to trigger the quantifier. The quantifier being (at the Viper level): ``` inhale (let _LET_0 ==...
Are there any plans to support `unsafe {}` and raw pointers in Prusti in the (far) future? I could think of one hypothetical scenario that may not play nice with...
> There have been [attempts](https://eprints.illc.uva.nl/id/eprint/1790/2/MoL-2021-04.text.pdf) to unify RustBelt and Stacked Borrows, but it seems that they raised more questions than answered. Thanks for the link to that thesis! I think...
> For your example, permissions, unfortunately, will not help because the permission to access `*value` and `*ptr` belongs to the activation record (stack frame) and, therefore, you can access them...
Hmm, I tried to see if I could illustrate this with a Viper example, but so far I came up empty handed and now have more questions than before, haha....
> Could you check whether setting [USE_MORE_COMPLETE_EXHALE](https://viperproject.github.io/prusti-dev/dev-guide/config/flags.html#use_more_complete_exhale) setting to false fixes the issue? Indeed it does!
Are there any known down-sides to setting [USE_MORE_COMPLETE_EXHALE](https://viperproject.github.io/prusti-dev/dev-guide/config/flags.html#use_more_complete_exhale) to false with Prusti? This work-around seems to work when it is `true` instead and wondering which work-around to choose :smile: ```rust...
I've got another example that fails in all cases: * `use_more_complete_exhale = false` * `use_more_complete_exhale = true` * both with Prusti and Viper IDE ([Viper file](https://github.com/viperproject/prusti-dev/files/8575498/lib.rs_prusti_example.A.test-2.vpr.txt)) ```rust use prusti_contracts::*; fn...
@alexanderjsummers per the Zulip chat, here are the two generated Viper files :) one with all the `self.bar(a);` statements uncommented and the other with just 2 `self.bar(a);` statements. [lib.rs_prusti_example::B::foo all...
Thanks for the feedback and good luck with the exams! > By the way, putting #[pure] on Cell methods is unsound because pure functions assume that data referenced via shared...