Changes needed to translate both contracts and method bodies. The Statement and Expression traversers need to have a mode that controls two things:

1. Parameters occurring in contracts are translated as the corresponding in-parameter of the corresponding procedure. Parameters occurring in method bodies are translated as the corresponding out-parameter of the corresponding procedure.

2. Method calls in method bodies are translated as call commands. Method calls in contracts are translated as function calls.

0 files changed, 0 insertions, 0 deletions