541605 - propagate constraints during copying

Status: RESOLVED INCOMPLETE

(Servo Graveyard :: Rust, defect)

Description

[Graydon Hoare :graydon]

Copying from one slot to another should add a copy of every constraint that includes the RHS of the assignment to the copy postcondition (with the RHS renamed, in the constraint, to the new LHS slot).

In other words:

  let int x = 10;
  let int y = 11;
  check lt(x,y);    // postcond = { lt(x,y) }
  let int z = x;    // postcond = { lt(x,y), lt(z,y) }

Unless some horrible complications arise that make this impossible, I believe the current rules permit this propagation to work.

Comment 1

[Graydon Hoare :graydon]

Moved to github issue #35.