Pointerbender
Pointerbender
I see! This even happens despite the fact that `do_something` is not marked as `#[pure]`. Thinking deeper about it, I believe part of the reason must be because `do_something` gets...
It just got weirder, in some cases I need to make Prusti explicitly retain the `$discriminant_axiom` and `$discriminant_range` domain axioms for enums, even if `is_unfoldable` is `true`! Unfortunately, this is...
> We have faced similar issues with @vl0w for deeply nested generics + iterators. Have you also seen problems related to nesting pure functions too deep so that the snap...
> This bug should be fixed once we fully migrate to manual axiomatization of functions. Ah, thanks! Is this also part of the refactoring or is this a separate feature?
I managed to make a reduced example for 2 out of the 3 bugs mentioned in this issue: [issue-1044-1.rs.txt](https://github.com/viperproject/prusti-dev/files/8889224/issue-1044-1.rs.txt) It is still larger than the usual examples, but at least...
The same also happens for enums that have struct variants: ```rust #[derive(PartialEq)] pub enum Binop { Add { left: u32, right: u32 }, Sub { left: u32, right: u32 },...
> Speaking of #749, has there been any progress on the issue of shared reference tuples? I keep running into this issue when working with option/result/enum types. You mention that...
It seems that the expression replacement in `fn inline_spec_item` fails here: https://github.com/viperproject/prusti-dev/blob/7a5c782d52c92a7e7ce208786efad64fb2cb7836/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs#L100-L102 Here it tries to replace the expression for `_4`: ``` Field( FieldExpr { base: Local( Local { variable:...
Looks like the extra code from #980 doesn't fix it, but this custom fix does seem to work: https://github.com/viperproject/prusti-dev/compare/master...Pointerbender:issue-1006?expand=1#diff-2bae12bf0e8545aac8fbb34fd81324fbf8bf69d6178b4084a790ab14ad106bdb The only problem with it is that it triggers a panic...
([#729](https://github.com/viperproject/prusti-dev/issues/729#issuecomment-1103777134) is another known issue for which I have the new encoder temporarily disabled on my local build, btw)