Vytautas Astrauskas

Continue refactoring.

4

Continue refactoring.

Continue refactoring

Try disabling more complete exhale and see what happens.

7

At least on some examples, it seems that the more complete exhale does not have anymore its great effect on performance. Since it has incompletenesses, try disabling it.

It seems that the compiler runs coherence checks (such as trait orphan check) in `after_expansion` implementation which, we do not do. We should fix this. Creusot code that does this:...

Internal error when expiring multiple shared borrows at the same time

1

The following example: ```rust use prusti_contracts::*; pub struct Tree { right: Option, } fn sub_tree_sub_size_computed_helper( node: &Tree, subSize1: &u32, ) { match &node.right { None => {} Some(r) => {...

Slice and array indexing should be supported in triggers

4

Currently, using `s[i]` in a trigger where `s` is an array or a slice causes Prusti to crash.

Docs on available tools and when to use them

10

It seems that most issues on this repository are about improving tooling. However, I think that it is also important to teach the community how to use these tools efficiently....

Some initial thoughts on what a verifier needs from the compiler.

Please summarize your changes, why they are needed and how you tested them.

Try disabling function unfolding triggers.

2

Enable `--disableFunctionUnfoldTrigger`.