Search results

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

Status: Open.

#199 In coord-e/thrust;

· coord-e opened on Jul 31, 2026

Panic: refine_local_defs calls optimized_mir on non-fn-like defs before the is_fn_like guard, so any program with a const/static item (or an array-repeat [v; N]) aborts before verification

bugSomething isn't workingSomething isn't working

Status: Open.

#198 In coord-e/thrust;

· coord-e opened on Jul 30, 2026

Unsound: calling a non-capturing closure with an argument, inside a function that has parameters, leaves the outer parameter's precondition predicate unconstrained — panicking programs verify as safe

Status: Open.

#197 In coord-e/thrust;

· coord-e opened on Jul 29, 2026

Unsound: a #[param(name: { v | φ })] precondition combined with #[ensures(..)] is dropped at call sites too, so a #[thrust::trusted] function with a violated precondition verifies panicking programs as safe

Status: Open.

#196 In coord-e/thrust;

· coord-e opened on Jul 28, 2026

Ordering comparisons (<, >) on tuple/aggregate values emit ill-typed SMT (< Tuple Tuple) via the generic PartialOrd::lt/gt extern specs, so safe programs comparing tuples are falsely rejected

Status: Open.

#195 In coord-e/thrust;

· coord-e opened on Jul 27, 2026

Incompleteness: a refinement on a generic type argument in #[param] position is dropped for multi-variant enums, so the payload refinement is never assumed in the callee

bugSomething isn't workingSomething isn't working

Status: Open.

#193 In coord-e/thrust;

· coord-e opened on Jul 26, 2026

Incompleteness: an existentially-quantified precondition (requires(exists ..)) emits a quantifier into the Horn clause body, so the default z3 solver returns unknown — Result::unwrap/unwrap_err are unverifiable

Status: Open.

#192 In coord-e/thrust;

· coord-e opened on Jul 25, 2026

Incompleteness: a #[param(name: { v | φ })] precondition is silently dropped when the function also has an #[ensures(..)], so trivially-correct functions are rejected

Status: Open.

#191 In coord-e/thrust;

· coord-e opened on Jul 24, 2026

Unsound: a generic trait impl method's body is never checked against the trait method's spec, so callers assume an unverified ensures and panicking programs verify as safe

Status: Open.

#190 In coord-e/thrust;

· coord-e opened on Jul 23, 2026

Incompleteness: overriding a defaulted trait method reuses the trait method's inference template, so the default body's return value pollutes the override's inferred spec — safe programs are wrongly rejected

Status: Open.

#187 In coord-e/thrust;

· coord-e opened on Jul 22, 2026

Incompleteness: an explicit invariant! havocs live locals it doesn't mention, even when the loop never modifies them, wrongly rejecting safe programs

Status: Open.

#186 In coord-e/thrust;

· coord-e opened on Jul 21, 2026

Unsound: unsigned integer constants with the high bit set (e.g. u8 = 200) are decoded as negative in const_value_ty, so always-panicking programs verify as safe

bugSomething isn't workingSomething isn't working

Status: Open.

#180 In coord-e/thrust;

· coord-e opened on Jul 18, 2026