Add purity checks to the ternary expression (#778)

* fix issue

* fix a few tests

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala

@@ -44,7 +44,9 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
         // check that `cond` is of type bool
         assignableTo.errors(exprType(cond), BooleanT)(expr) ++
         // check that `thn` and `els` have a common type
-        mergeableTypes.errors(exprType(thn), exprType(els))(expr)
+        mergeableTypes.errors(exprType(thn), exprType(els))(expr) ++
+        // check that all subexpressions are pure.
+        isPureExpr(cond) ++ isWeaklyPureExpr(thn) ++ isWeaklyPureExpr(els)
 
     case n@PForall(vars, triggers, body) =>
       // check whether all triggers are valid and consistent

src/test/resources/regressions/issues/000777-1.gobra

@@ -0,0 +1,12 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000777
+
+ghost
+requires i >= 0
+decreases i
+func h(i int) (res int) {
+    //:: ExpectedOutput(type_error)
+    return i == 0 ? 0 : h(i - 1)
+}

src/test/resources/regressions/issues/000777-2.gobra

@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000777
+
+ghost
+requires i > 0
+decreases i
+pure func h(i int) (res int)
+
+ghost
+requires 0 <= i
+decreases
+func test(i int) {
+    x := i == 0 ? 0 : h(i)
+}