Return variable required for method calls

https://github.com/gradual-verification/gvc0/blob/master/src/test/resources/bugs/translate2.c0 is failing with a Could not translate term into Viper expression! Exiting safely. My explanation for why this is failing is not 100% confirmed, because in the backend a .vpr program containing a method call statement that is not assigned to a return value fails the Viper/Silver type checker. In this program, initialize(box); on line 23 is being called and its return value is not returned to anything. When I wrote in a temporary variable to bypass the type checker in Viper, the vpr version of the program that I ran in the backend verified successfully. So, I can’t really properly confirm what is failing in the backend, since it is now succeeding. My intuition is that on line 24 a run-time check is produced for acc(box->content->value) when the result of initialize(box) is != 0. In this case, there is a run-time check being produced that has a branch condition attached to it that is dependent on the missing return variable of initialize. So, the backend (through the c0 frontend) cannot resolve the translation of \result != 0, since \result is not assigned to anything in the callee context. Same issue for https://github.com/gradual-verification/gvc0/blob/master/src/test/resources/bugs/translate3.c0.

@conradz Since Viper cannot accept method calls that are not assigned to anything when they have a return value, the frontend needs to avoid sending such programs to Viper.

@conradz and @hemantgouni It would be nice to warn about this in some way in the pipeline. Right now the error is not descriptive enough for the problem. I am not sure what the best solution is. I feel like warning about this in the backend is the right solution for future frontends, but might be a little tricky to do and is probably something to do as a future enhancement.

gradual-verification / gvc0

Return variable required for method calls #14