-
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
- Status: Open.#269 In coord-e/thrust;
Replacing a
Box/&mut-typed struct or tuple field (c.page = Box::new(..)) is elaborated into a write *through* the old pointer, so the field's type in the env becomes its pointee and every later use of the struct aborts the analyzerbugSomething isn't workingSomething isn't workingStatus: Open.#267 In coord-e/thrust;A locally-declared
struct/enumnever gets aModelinstance, soVec<P>/Box<P>/&[P]/[P; N]/&mut Pabort inTypeBuilder::build—Vec<P>dies insidealloc's private fields (*const u8), and a one-lineimpl Model for P { type Ty = Self; }makes every case verifybugSomething isn't workingSomething isn't workingStatus: Open.#266 In coord-e/thrust;Incompleteness: a
&mutinto anenum/Optionwhose payload is aVec(anySeq-modeled container) defeats the default solver configuration — a five-lineOption<Vec<i64>>program times out, while the same code with the container in a struct field, or moved out by value, verifies in 0.5 sbugSomething isn't workingSomething isn't workingStatus: Open.#263 In coord-e/thrust;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;