Details: Location bb15[12] has not yet been encoded

viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.

http://prusti.org

Other

1.52k stars 103 forks source link

Details: Location bb15[12] has not yet been encoded #1462

Closed smokytheangel0 closed 8 months ago

smokytheangel0 commented 8 months ago

Not entirely sure what this means in relation to what I am doing. I'm not even sure I know what I'm doing right now. Screen Shot 2023-10-16 at 14 11 40

smokytheangel0 commented 8 months ago

I think it has to do with referenced typed fields?

fpoli commented 8 months ago

Thank you for the report. "Internal errors" are in 99% of the cases a bug in the implementation of our tool, as the error message suggests. Could you provide a minimal example to reproduce the bug? Without that, we cannot debug this.

fpoli commented 8 months ago

Feel free to reopen if you have a minimal example.