Federico Poli

Program: ``` predicate R(a: Int) define Q(a) ( forall x: Ref :: false ==> R(a) ) method lemma(a: Int) returns (x: Ref) requires forall b: Bool :: Q(a) { assume...

Is it possible to apply a perm expression on a parameter of a macro? The following doesn't parse: ``` define check(expr) { assert perm(expr) < write } ``` Error message:...

The following program, generated by a fuzzer starting from Silver's test suite, makes Silicon crash. There are some weird characters in it, like "\ufffd\ufffd\ufffd". Error: ``` Silicon 1.1-SNAPSHOT Verification aborted...

The following program fails to verify in Silicon and Carbon, but by uncommenting the first assert statement everything goes through. The incompleteness is essentially by design, as explained by @mschwerhoff...

Unexpected `.postcard_creator_wrapper_sent` folder

1

Hi :wave: I noticed that the `postcards-folder` script always creates a `.postcard_creator_wrapper_sent` folder, which I guess is only used for debugging. I think the issue is in `create_text_cover`, where the...

An example to be fixed in the the ongoing Prusti rewrite: ```rust use prusti_contracts::*; #[requires(*x == a && a != b)] //#[after_expiry(*x == before_expiry(*result))] // Does not verify, but it...

Making co-existing jni-sys wrappers as safe as possible

5

While building [duchess](https://github.com/duchess-rs/duchess) we found a data race in the OpenJDK implementation of `JNI_GetCreatedJavaVMs`. When called concurrently with `JNI_CreateJavaVM`, `JNI_GetCreatedJavaVMs` might return pointers to partially-initialized JVMs ([OpenJDK bug](https://bugs.java.com/bugdatabase/view_bug?bug_id=JDK-8308341)), which then...

`len()` implementation without overflow errors

1

Viktor Kuncak (@vkuncak) suggested the following trick to implement a `len()` method that verifies with overflow checks enabled. They used it in [Stainless](https://github.com/epfl-lara/stainless): ```rust impl Link { #[pure] #[ensures(result usize...

Package flag required even when providing a manifest path

1

Hi! When running `cargo-modules orphan --manifest-path=path/to/package/Cargo.toml` in a workspace, the output is the following: ``` Error: Multiple packages present in workspace, please explicitly select one via --package flag. Packages present...