Cross method join is not supported

[viper-admin]

Created by @vakaras on 2015-07-03 16:42

Initial version of Chalice2Silver used eval expression to establish relation between context in which the method was forked and in which it is joined. Now, the eval is deprecated, and it seems to be impossible to write such precondition that it is possible to join token passed as argument:

#!Chalice

  method client(tk : token<Main.work>)
    requires acc(tk.joinable) && tk.joinable
  {
    join tk; // Fails with inhale.failed:insufficient.permission
  }

A larger example can be found in the test suite: oldC2SCases/crossMethodToken.chalice.