Conditionals in expressions (not formulas) should be translated to if statements in Gradual Viper

[jennalwise]

Conditionals in expressions are not supported in Gradual Viper programs, rather conditionals in formulas are supported and if statements are also supported. So, to support conditionals in expressions GVC0 needs to translate them into if statements in Gradual Viper. I believe GVC0 does a similar type of translation for method calls and allocs in expressions, so that code would be a great start to look at for this.

This issue was discovered from the following example and error:

// C0 program
// A utility function to get maximum of two integers
int max(int a, int b)
{
    return (a > b)? a : b;
}

// Gradual Viper program
method max(a: Int, b: Int) returns ($result: Int)
{
   $result := (a > b ? a : b)
}

So what is happening is (a > b ? a : b) is being used in a return statement, which is translated into result := (a > b ? a : b) in Gradual Viper, and so (a > b ? a : b) is considered an expression. However, we do not support conditionals in expressions, because they may appear in specifications which already have their own case for conditionals that handles them appropriately. Therefore, the following error is produced by Gradual Viper: [error] An internal error occurred. (a > b ? a : b) occurred unexpectedly. (<no position>)