Federico Poli comments

Results 208 comments of


                                            Federico Poli

Failing magic wand generation

PR #739 fixes the former program, but not the latter.

The issue is in the separation of duties between the fold-unfold algorithm and the code that handles the expiration of borrows. Currently, the fold-unfold algorithm considers expressions like `f.g` and...

encode_bitvectors not working with generics instantiated to u32

Thank you for the report. From the log it looks like a network transmission error. Could you also include the log of the "Output > Prusti Assistant Server" tab?

encode_bitvectors not working with generics instantiated to u32

Thanks! The second log and the updated example are very helpful. It seems to be a bug that is triggered by using bitwise operations with generic types, even when the...

encode_bitvectors not working with generics instantiated to u32

Note, however, that `#[pure]` on `read(&self) -> T` means that the result cannot change as long as the program holds a shared reference to `Volatile`. This is probably not what...

encode_bitvectors not working with generics instantiated to u32

Then we would need a full example, like a zip of the crate that you are writing.

encode_bitvectors not working with generics instantiated to u32

I think you can attach a zip to this github issue.

encode_bitvectors not working with generics instantiated to u32

Trying your code with the workaround I get a proper error: ``` [Prusti: unsupported feature] bitwise operations on non-boolean types are experimental and disabled by default; use `encode_bitvectors` to enable...

encode_bitvectors not working with generics instantiated to u32

Thanks, with `encode_bitvectors=true` I can reproduce the panic. That flag is quite recent and highly experimental, so if you plan to use it a lot you'll probably find more bugs...

`verify/pass/arrays/{merge,selection_sort}.rs` timeout issue

The same for `pass/arrays/merge.rs` on Mac: Prusti failed to finish within 500 seconds. It finished in 521.787225005s. ([job](https://github.com/viperproject/prusti-dev/runs/4738417450?check_suite_focus=true))