Incorrect desugaring of ternary operator with impure operands

[jcp19]

Reported by Conradin Laux.

In the file below, function h2 verifies just fine, but function h does not, even though it computes the same value as h2 using a ternary expression.

ghost
requires i >= 0
decreases i
func h(i int) (res int) {
    return i == 0 ? 0 : h(i - 1)
}

ghost
requires i >= 0
decreases i
func h2(i int) (res int) {
    if i == 0 {
        return 0
    } else {
        return h2(i - 1)
    }
}

Looking at the viper encoding, we find that the ternary expression in function h is encoded as

      var N2: Int
      // first, h is called
      N2 := h_41fccf1_F(i_V0_CN0 - 1)
      // only then do we desugar the ternary expression
      res_V0_CN1 := (i_V0_CN0 == 0 ? 0 : N2)

Clearly, this is wrong. I think that the most appropriate solution here is to always require that a ternary expression is pure. As such, the example above would be rejected because we would call a non-pure function in a ternary operation. This does not limit expressiveness, because we could always use a ghost if instead.

[ArquintL]

Alternatively, we could encode an impure ternary operator as an if statement. While convenient to overcome Go‘s shortage of a ternary operator, this encoding might be more surprising than just rejecting such ternary operators

[jcp19]

Alternatively, we could encode an impure ternary operator as an if statement. While convenient to overcome Go‘s shortage of a ternary operator, this encoding might be more surprising than just rejecting such ternary operators

Yeah, I think that would be too surprising, and I don't see a good reason for doing that transformation because a ghost if is always acceptable in the contexts where a non-pure conditional expression was accepted before this PR.