-
Notifications
You must be signed in to change notification settings - Fork 13
Open
Description
In the following code, it doesn't seem correct that the first Loan struct computed includes the line START/6 - it seems that that value of list is dead by that point, and the lifetime of the borrow on x shouldn't extend beyond the penultimate statement.
struct List<+> {
value: 0,
}
let x: List<()>;
let y: List<()>;
let list: &'list mut List<()>;
let v: &'v mut ();
block START {
x = use();
y = use();
list = &'b1 mut x;
v = &'b2 mut (*list).value;
list = &'b3 mut y;
use(v);
use(list);
}
// Loan {
// point: START/2,
// path: Var(Variable { name: "x" }),
// kind: Mut,
// region: {START/3, START/4, START/5, START/6} }
// Loan {
// point: START/3,
// path: Extension(Extension(Var(Variable { name: "list" }), FieldName { name: "*" }), FieldName { name: "value" }),
// kind: Mut,
// region: {START/4, START/5} }
// Loan {
// point: START/4,
// path: Var(Variable { name: "y" }),
// kind: Mut,
// region: {START/5, START/6} }
// assert 'list == {START/3, START/4, START/5, START/6};
// assert 'v == {START/4, START/5};
// assert 'b1 == {START/3, START/4, START/5, START/6};
// assert 'b2 == {START/4, START/5};
// assert 'b3 == {START/5, START/6};
Metadata
Metadata
Assignees
Labels
No labels