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