utwente-fmt/vercors

ConstantifyFinalFields is a bit dubious

Opened this issue · 0 comments

pieter-bos commented
  • in pvl we should check that final fields are all assigned exactly once in each constructor
  • ConstantifyFinalFields allows heap-independent function invocations, but such invocations might succeed in the local context of a constructor, and fail in the "axiomatized" context.