uclid-org/uclid

instance procedure calls use modified values

adwait opened this issue · 1 comments

Procedure proc1 modifies x and proc2 uses x.
The following results in proc2 using the value of x from the previous step (as expected).

module m {
  ...
  next {
    call () = proc1();
    call () = proc2();
  }
  ...
}

The following results in proc2 using the new value of x.

module main {
  instance m1 : m ();
  ...
  next {
    call () = m1.proc1();
    call () = m1.proc2();
  }
  ...
}

See file test/test-instance-procedure-calls-1.ucl.

Fixed by this: #238