Aurea comments

Results 157 comments of


                                            Aurea

Remove `extern crate prusti_contracts` from Prusti

Thanks, this was also bugging me.

Support for library contracts

@Pointerbender This discussion is starting to overlap quite a bit with @juliand665's thesis. (Also for that reason @jjurm the solution in this PR does not yet have to be perfect.)...

Support for library contracts

Generally looks good! I wish it wasn't a PR that combined so many changes: - support cross-crate specs; - refactor build process for loading `prusti-contracts` and core/std specs; - refactor...

Consistency error with chained pure fns and tuples

Is this check causing the interpreter to skip the assignment? https://github.com/viperproject/prusti-dev/blob/7977d30a028edfe0e300bb2931992d4029385b41/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs#L851

Add Caching Documentation

@JonasAlaif Is this blocked on the PR https://github.com/viperproject/prusti-assistant/pull/134? What is the status there?

Try disabling more complete exhale and see what happens.

@vakaras Since you are merging this, are you 100% sure the performance is overall better? Did @zgrannan get to test this?

Memory crash during Prusti encoding step

Also, just in case you are not familiar with this: [`git bisect`](https://git-scm.com/docs/git-bisect) might make your search through the commits much faster.

No panic detected on unwrap with None type

Thanks for the report! This is because Prusti does not know anything about `Option::unwrap` (and it is just a method like any other), so it has no reason to report...

No panic detected on unwrap with None type

Exporting specifications across crate boundaries is also something we are actively working on.

Prusti does not understand the question mark operator

Thanks for the suggestion! The reason this doesn't work right now is that the ? operator is desugared by the Rust compiler to a method call and by default that...