Vytautas Astrauskas

> Is this something that Prusti should generate automatically in the Viper program when `check_overflows = true`, or should this information be encoded differently somehow? Yes, it should. After my...

My refactorings are still in progress.

> Also, would it be easy to add support for `get(&0)`? Currently the `&0` is `[Prusti: unsupported feature] unsupported constant type Ref('_#6r, usize, Not)` In a pure context, you may...

Reference-typed fields are not yet supported (`get` returns `Option`).

The problem is that the bit operation is applied in a specification to a value returned by a function. Here is the minimal example: ```rust // compile-flags: -Pencode_bitvectors=true use prusti_contracts::*;...

> I think the `fix_quantifiers` and/or the `optimize_folding` passes might be altering the user-specified quantifiers in a way that makes it hard for Viper to infer the correct triggers Just...

> In that case I think the best way forward to fix this performance issue is to add triggers to the test case once #812 is resolved and @vakaras' refactorings...

Thank you for investigating this! I suspect that the second option would be quite easy to implement and hopefully does not introduce too serious performance problems. So, I personally would...

Thanks for referencing the tools! I would like to clarify their aims and capabilities: > Prusti for proving properties such as absence of overflows on unmodified Rust code Prusti ([project...

@DevQps Thank you for compiling this list. I think it is a really nice starting point from which at some point we could try to build a “security cookbook”.