-
Notifications
You must be signed in to change notification settings - Fork 1
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Incompleteness: a refinement declared on any parameter but the last (
#[param]/#[sig]) is never assumed in the body, so no multi-argument function can be given a refinement-typed signaturebugSomething isn't workingSomething isn't workingStatus: Open.#261 In coord-e/thrust;Incompleteness: the hard-coded
fp.spacer.global=truez3 option makes any nested loop whose inner body has a merging conditional unverifiable — an 11-clause system that z3 solves in 0.5s without it runs >5min with itbugSomething isn't workingSomething isn't workingStatus: Open.#260 In coord-e/thrust;Unsound: a crate with no
main(any--crate-type lib/rlib/…) gets no entry-point anchor, so every inferred precondition is discharged asfalseand the whole crate —pubAPI functions that always panic included — verifies assafebugSomething isn't workingSomething isn't workingStatus: Open.#259 In coord-e/thrust;No method of a trait
implcan be specified:requires/ensures/param/ret/sigemit theirformula_fncompanions as items of theimpl, so every trait-impl method dies withE0407— and the only alternative (spec on the trait) forces one spec on all implsbugSomething isn't workingSomething isn't workingStatus: Open.#258 In coord-e/thrust;A loop bound that MIR folds into a debug-info constant cannot be named in
invariant!:let n = 10; while i < nfatally errors with "not a live variable", and under shadowing the name silently binds to the wrong variablebugSomething isn't workingSomething isn't workingStatus: Open.#257 In coord-e/thrust;- Status: Open.#255 In coord-e/thrust;
Panic (
deref unbound var/borrowing unbound var):THRUST_ENUM_EXPANSION_DEPTH_LIMITtruncates every binding form, not just enum unfolding, so a&muttwoenumlayers deep (Result<Option<&mut T>, E>) gets no flow binding and any use of it aborts the compilerbugSomething isn't workingSomething isn't workingStatus: Open.#253 In coord-e/thrust;Unsound: the drop-flag edge of a conditionally-moved value still gets a liveness-derived implicit drop, so the consumed path's
&mutprophecy is re-resolved and that path vanishes —if flag { f(); }over anFnOnceverifies panicking programs assafebugSomething isn't workingSomething isn't workingStatus: Open.#250 In coord-e/thrust;Stack overflow (non-termination) in
TypeBuilder::build: a struct is always expanded structurally with no cycle cut, so any struct that reaches itself (struct Node { next: Option<Box<Node>> },struct Tree { kids: Vec<Tree> }) aborts the compilerbugSomething isn't workingSomething isn't workingStatus: Open.#249 In coord-e/thrust;Unsound: at
-C opt-level >= 1a compound assignment through a&mutthat sits behind a projection is reborrowed twice, the two prophecy resolutions contradict the write, and the function verifies vacuously — evenassert!(false)issafebugSomething isn't workingSomething isn't workingStatus: Open.#248 In coord-e/thrust;Unsound: at
-C opt-level >= 1GVN rewrites theBoxderef temp fromderef_copytocopy, sounelaborate_derefsmisses it and every write through a nestedBoxlands on a copy — panicking programs verify assafebugSomething isn't workingSomething isn't workingStatus: Open.#244 In coord-e/thrust;Incompleteness: calling the same un-annotated
&mut-taking helper twice from a function that itself takes&mutmakes the inferred-spec CHC system recursive over aMut<T>datatype argument — trivially-safe programs die onTimeoutbugSomething isn't workingSomething isn't workingStatus: Open.#243 In coord-e/thrust;