Dafny-to-Rust:

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

class Test {
  var x: int
  constructor() {
    x := 1;
  }
  function Plus(c: int): int reads this {
    x + c
  }
  function Get(): int reads this {
    x
  }
  method Test() {
    print Plus(Plus(Get()));
  }
}

method Main() {
  var c := new Test();
  c.Test();
}

Command to run and resulting output

dafny run -t:rs thefile.dfy

What happened?

There is a Rust compilation error because it complains self cannot be borrowed twice mutably in the same line.

Fixing this seems easy, it's just that we need to borrow self instead of mutably borrow self.
However, that would create a soundness issue we prevented in that Object::from_ref's reference count increment might be dropped in --release if we only borrow, not if we mutably borrow.

What type of operating system are you experiencing the problem on?

Windows