Pointerbender
Pointerbender
I created PR #582 for a quick fix for some corner cases, however, this is not a sufficient fix yet. For example, this program still crashes: ``` adt Test {...
I have some extra information to share that was accumulated during a [Zulip](https://prusti.zulipchat.com/#narrow/stream/236614-general/topic/Building.20custom.20viperserver.20.2B.20silver) discussion with Alex Summers: Ideally, when the transformer here: https://github.com/viperproject/silver/blob/5503e4a736a2b9b455ed279a66c34c1597907c77/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala#L110-L129 reaches the `PFunction` case, it should replace...
This hack seems to work for most corner cases: https://github.com/viperproject/silver/blob/2fe26fb919ab67442bf102e54751df38c327541f/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala#L122-L136 However, this does not solve the corner case from [this comment](https://github.com/viperproject/silver/issues/581#issuecomment-1139643448), still. I'm hoping that there is a better solution...
> > These names might much more strongly want access to the wrapped type to be explicit (but still safe) rather than through Deref, though, as they're much more "active"...
Do the effects of `MaybeDangling` also recurse into the pointee and/or pointee's fields? E.g. will `MaybeDangling` also strip the `&mut T` from its memory-dependent validity obligations, or would that require...
> `core::mem::size_of` > trait to allow users to specify what this method will return for their type That's exciting stuff! Would this also be possible for `core::mem::align_of`, by any chance?...
Once this PR has laid the ground-work for adding specs to the Rust standard library, how hard/easy would it be for an advanced end-user to contribute standard library specs for...
> We might work on this in the future but I would like to see a good use case first. Maybe you have one? Thanks for the explanation! Originally I...
p.s. a slight variation of the program and MIR is: ```rust use prusti_contracts::*; pub struct Foo { fn drop(&mut self) {} } pub struct Bar; impl Bar { #[trusted] pub...
I just converted this PR to draft. Although the work-around in this PR works, I suspect a better solution will come out of #581. It seems to be related to...