Federico Poli

Default precondition of external functions

4

We discussed that external functions should have `false` as precondition, instead of `true`. The latter only makes sense if Prusti verifies *all* the dependencies, but this is not what `cargo-prusti`...

Example that fails with more complete exhale

4

The following program: - does not verify in Prusti, - verifies if the parameter `b` is commented out, - alternatively, it verifies if `PRUSTI_USE_MORE_COMPLETE_EXHALE` is **false**. ```rust use prusti_contracts::*; const...

Incorrect loop invariant permissions due to structure initialized before the invariant

6

The following program causes an internal error ("generating fold-unfold Viper statements failed") caused by a limitation in the encoding of initialization of local variables. ```rust fn test() { let mut...

Overflow check not disabled

1

Disabling overflow checks is not enough to verify the following program. ```rust fn test(x: i32) -> i32 { -x // ERROR } ``` ``` [Prusti: verification error] assertion might fail...

Currently the encoding of pure expressions walks the CFG backward, from the return statement(s) to the entry point. The encoder starts with a "return expression" that is `_0`, and at...

Tests crashing due to missing Viper function definitions

1

The tests listed below crash with a Viper exception, probably because a function is called without being defined. Example of exception: ``` Java exception: java.lang.RuntimeException: Function name m_pure_chain_7$$id$opensqu$0$closesqu$__$TY$__Snap$m_pure_chain_7$$A$opensqu$0$closesqu$$_beg_$_end_$Snap$m_pure_chain_7$$A$opensqu$0$closesqu$$_beg_$_end_ not found...

Can the library help somehow in the generation of native proxies of Java objects? At the moment we are using this crate https://github.com/viperproject/jni-gen (undocumented...) Our approach inspects the JVM by...

Interrupting the test suite doesn't kill the server

8

I currently have 2 `prusti-server` and 5 `prusti-server-driver` unused programs running in the background: ``` $ ps ax | grep [p]rusti 5638 pts/18 Sl 0:00 ../target/debug/prusti-server --port=0 5640 pts/18 Sl...

The [`vergen` crate](https://crates.io/crates/vergen) seems a better alternative than manually calling `git` https://github.com/viperproject/prusti-dev/blob/69325d35ec51a45118ec93ed4e46957e1d08f903/prusti/build.rs#L12-L16 https://github.com/viperproject/prusti-dev/blob/69325d35ec51a45118ec93ed4e46957e1d08f903/prusti/build.rs#L21-L25

In our project [viperproject/prusti-dev](https://github.com/viperproject/prusti-dev/tree/42c6ac199946f532d9a34752d22dba4faaa157fc) `cargo outdated` fails with the following error. ``` error: package `/home/fpoli/src/prusti-dev/prusti-contracts/prusti-specs/Cargo.toml` is a member of the wrong workspace expected: /home/fpoli/src/prusti-dev/Cargo.toml actual: /home/fpoli/src/prusti-dev/prusti-contracts/Cargo.toml ``` This error message...