From b684ebc167a2724f834796d5ea73c6d9d6449421 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Wed, 3 Jul 2024 16:34:45 +0200
Subject: [PATCH] Add purity checks to the ternary expression (#778)

* fix issue

* fix a few tests
---
 .../typing/ghost/GhostExprTyping.scala           |  4 +++-
 .../resources/regressions/issues/000777-1.gobra  | 12 ++++++++++++
 .../resources/regressions/issues/000777-2.gobra  | 16 ++++++++++++++++
 3 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 src/test/resources/regressions/issues/000777-1.gobra
 create mode 100644 src/test/resources/regressions/issues/000777-2.gobra

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala
index 2fcba6af7..2f2a04d60 100644
--- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala
+++ b/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
diff --git a/src/test/resources/regressions/issues/000777-1.gobra b/src/test/resources/regressions/issues/000777-1.gobra
new file mode 100644
index 000000000..29e2921ac
--- /dev/null
+++ b/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)
+}
\ No newline at end of file
diff --git a/src/test/resources/regressions/issues/000777-2.gobra b/src/test/resources/regressions/issues/000777-2.gobra
new file mode 100644
index 000000000..6dc507300
--- /dev/null
+++ b/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)
+}
\ No newline at end of file