Merge pull request #802 from viperproject/meilers_dont_count_requires_as_pre

Allow domain axioms to use functions that have decreases clauses

Author: marcoeilers

src/main/scala/viper/silver/parser/Resolver.scala

@@ -7,6 +7,7 @@
 package viper.silver.parser
 
 import viper.silver.FastMessaging
+import viper.silver.parser.PKw.Requires
 
 import scala.collection.mutable
 
@@ -685,8 +686,13 @@ case class TypeChecker(names: NameAnalyser) {
                           check(fd.typ)
                           fd.formalArgs foreach (a => check(a.typ))
                         }
-                        if (pfa.isDescendant[PAxiom] && pfn.pres.length != 0)
+                        if (pfa.isDescendant[PAxiom] && pfn.pres.toSeq.exists(pre => pre.k.rs == Requires)) {
+                          // A domain axiom, which must always be well-defined, is calling a function that has at least
+                          // one real precondition (i.e., not just a requires clause or something similar that's
+                          // temporarily represented as a precondition), which means that the call may not always be
+                          // well-defined. This is not allowed.
                           issueError(func, s"Cannot use function ${func.name}, which has preconditions, inside axiom")
+                        }
 
                       case pdf: PDomainFunction =>
                         val domain = pdf.domain

src/test/resources/all/issues/silicon/0847.vpr

@@ -0,0 +1,68 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+function f1(i: Int): Int
+    decreases i
+    requires i > -2
+{
+    i > 0 ? 1 + f1(i - 1) : 0
+}
+
+function f2(i: Int): Int
+    decreases i
+{
+    i > 0 ? 1 + f2(i - 1) : 0
+}
+
+function f3(i: Int): Int
+    decreases i
+    ensures result >= 0
+{
+    i > 0 ? 1 + f3(i - 1) : 0
+}
+
+function f4(i: Int): Int
+    ensures result >= 0
+    decreases _
+{
+    i > 0 ? 1 + f4(i - 1) : 0
+}
+
+function f5(i: Int): Int
+    requires i > -2
+    decreases i
+    ensures result >= 0
+{
+    i > 0 ? 1 + f5(i - 1) : 0
+}
+
+domain t {
+    function fAlias1(Int): Int
+    function fAlias2(Int): Int
+    function fAlias3(Int): Int
+    function fAlias4(Int): Int
+    function fAlias5(Int): Int
+
+    axiom {
+        //:: ExpectedOutput(typechecker.error)
+        forall i: Int :: f1(i) == fAlias1(i)
+    }
+
+    axiom {
+        forall i: Int :: f2(i) == fAlias2(i)
+    }
+
+    axiom {
+        forall i: Int :: f3(i) == fAlias3(i)
+    }
+
+    axiom {
+        forall i: Int :: f4(i) == fAlias4(i)
+    }
+
+    axiom {
+        //:: ExpectedOutput(typechecker.error)
+        forall i: Int :: f5(i) == fAlias5(i)
+    }
+}