Issues

Panic: a null-sorted value (`fn(..)` pointer, `&str`) stored in an aggregate that also has a non-singleton field is filtered out of `Env::dependencies`, aborting with `unbound var` or `no entry found for key`

bug

#217

· coord-e opened

on Aug 14, 2026

Unsound: a user `Drop` impl is never checked at the drop site — `TerminatorKind::Drop` only resolves prophecies, so a destructor that panics verifies as `safe`

bug

#215

· coord-e opened

on Aug 13, 2026

Unsound: `==` on `&mut` references compares the prophecy too, so the comparison's result depends on writes made after it — panicking programs verify as `safe`

bug

#210

· coord-e opened

on Aug 10, 2026

Unsound: a two-phase borrow (`v.push(v.len())`) havocs the receiver before the arguments are evaluated, so reads in the argument see the prophecy — panicking programs verify as `safe`

#209

· coord-e opened

on Aug 9, 2026

Unsound: moving a `&mut`-capturing closure out of any aggregate (incl. `enum`/`Option`), with no higher-order call, drops its prophecy and verifies panicking programs as `safe` (generalizes #177)

bug

#207

· coord-e opened

on Aug 8, 2026

Ill-typed SMT: a closure that mutates a captured variable, passed to a generic HOF spec'd with `pre!`/`post!`, has its pre/postcondition predicate declared at the FnMut receiver sort `Mut<env>` but applied at the bare `env` sort, so verification aborts with a solver sort mismatch

bug

#206

· coord-e opened

on Aug 7, 2026

Incompleteness: an explicit `invariant!` on a loop that writes through a `&mut` drops the reference's prophecy link, so the referent is havoc'd after the borrow ends — safe programs wrongly rejected (no workaround; the inference path handles it)

#205

· coord-e opened

on Aug 6, 2026

Unsound: `Vec` equality (`==`) is modeled as structural equality of the whole `(array, length)` representation, so vectors equal in Rust but differing in stale slots past `length` (after `pop`/`truncate`) compare unequal — dead-branch panics verify as `safe`

bug

#203

· coord-e opened

on Aug 5, 2026

Incompleteness: a `&mut` stored in a `Vec` (Seq/array-backed container) never has its prophecy resolved at drop, so safe programs are wrongly rejected as `Unsat`

#202

· coord-e opened

on Aug 3, 2026

Incompleteness: a `fn(..)` pointer value called outside the basic block that created it loses the callee's refinement spec (result is havoc'd), so valid programs verify as `Unsat`

#201

· coord-e opened

on Aug 2, 2026

Unsound: an uncalled generic function (a type param appears in its signature) has its body skipped entirely, so a `#[thrust::callable]` entry point whose body always panics — or whose body violates its own `ensures` — verifies as `safe`

#200

· coord-e opened

on Aug 1, 2026

`thrust-rustc` compiles at rustc's default edition (2015), not 2021 like its `ui_test` suite: annotation diagnostics are masked as `E0433: missing crate 'core'`, and edition-sensitive programs behave differently

#199

· coord-e opened

on Jul 31, 2026

Navigation Menu

All issues

Panic: a null-sorted value (`fn(..)` pointer, `&str`) stored in an aggregate that also has a non-singleton field is filtered out of `Env::dependencies`, aborting with `unbound var` or `no entry found for key`

Unsound: a user `Drop` impl is never checked at the drop site — `TerminatorKind::Drop` only resolves prophecies, so a destructor that panics verifies as `safe`

Unsound: `==` on `&mut` references compares the prophecy too, so the comparison's result depends on writes made after it — panicking programs verify as `safe`

Unsound: a two-phase borrow (`v.push(v.len())`) havocs the receiver before the arguments are evaluated, so reads in the argument see the prophecy — panicking programs verify as `safe`

Unsound: moving a `&mut`-capturing closure out of any aggregate (incl. `enum`/`Option`), with no higher-order call, drops its prophecy and verifies panicking programs as `safe` (generalizes #177)

Ill-typed SMT: a closure that mutates a captured variable, passed to a generic HOF spec'd with `pre!`/`post!`, has its pre/postcondition predicate declared at the FnMut receiver sort `Mut<env>` but applied at the bare `env` sort, so verification aborts with a solver sort mismatch

Incompleteness: an explicit `invariant!` on a loop that writes through a `&mut` drops the reference's prophecy link, so the referent is havoc'd after the borrow ends — safe programs wrongly rejected (no workaround; the inference path handles it)

Unsound: `Vec` equality (`==`) is modeled as structural equality of the whole `(array, length)` representation, so vectors equal in Rust but differing in stale slots past `length` (after `pop`/`truncate`) compare unequal — dead-branch panics verify as `safe`

Incompleteness: a `&mut` stored in a `Vec` (Seq/array-backed container) never has its prophecy resolved at drop, so safe programs are wrongly rejected as `Unsat`

Incompleteness: a `fn(..)` pointer value called outside the basic block that created it loses the callee's refinement spec (result is havoc'd), so valid programs verify as `Unsat`

Unsound: an uncalled generic function (a type param appears in its signature) has its body skipped entirely, so a `#[thrust::callable]` entry point whose body always panics — or whose body violates its own `ensures` — verifies as `safe`

`thrust-rustc` compiles at rustc's default edition (2015), not 2021 like its `ui_test` suite: annotation diagnostics are masked as `E0433: missing crate 'core'`, and edition-sensitive programs behave differently

Search results