Dominik Stolz

Add nightly feature

1

This PR adds a `nightly` feature which uses the recently added `PidFd` type from the standard library.

Mismatched types error in ghost macro

1

The following code produces a mismatched types error: ```rust fn foo() { let mut c: Ghost = ghost! { 0 }; c = ghost! { *c + 1 }; //...

The description of `crate-item-ok-goal` for function declarations specifies that > For a fn declaration declared in the crate C, like the following: > > fn foo u32 where T: Ord...

This issue tracks the remaining work for type invariants: - [ ] #843 - [x] Float quantifiers for invariants: #846 - [ ] Always include user invariant: The user invariant...

Generate type invariants for arrays, closures, and the never type

5

We only handle array types with non-generic lengths. The invariant modules generated for closures still have issues with clones.

When moving a single field of an aggregate value, we still consider the local initialized. As a consequence, we sometimes resolve locals that are only partially initialized. Combined with type...

Properly support open type invariants

2

The `#[open_inv]` attribute can be applied to functions, function arguments, and fields to declare them as having an open type invariant. Concretely: - on functions: completely ignore type invariants in...

Consider lifetime outlives relation when resolving multiple borrows

2

When multiple locals must be resolved at the same program point, we currently use their index as a heuristic for the correct order of resolution. A more correct solution would...

While debugging an issue with zips containing symlinks I noticed a couple of things: - The behavior of `mz_zip_writer_add_file` and `mz_zip_writer_add_path` is inconsistent. The latter skips symlinks if `store_links` and...