Disallow asserting expressions in axioms (#858)

Author: marcoeilers

src/main/scala/viper/silver/ast/Program.scala

@@ -568,6 +568,7 @@ sealed trait DomainAxiom extends DomainMember {
     (if(!Consistency.noResult(exp)) Seq(ConsistencyError("Axioms can never contain result variables.", exp.pos)) else Seq()) ++
     (if(!Consistency.noOld(exp)) Seq(ConsistencyError("Axioms can never contain old expressions.", exp.pos)) else Seq()) ++
     (if(!Consistency.noLocationAccesses(exp)) Seq(ConsistencyError("Axioms can never contain location accesses.", exp.pos)) else Seq()) ++
+    (if(!Consistency.noAsserting(exp)) Seq(ConsistencyError("Axioms can never contain asserting expressions.", exp.pos)) else Seq()) ++
     (if(!(exp isSubtype Bool)) Seq(ConsistencyError("Axioms must be of Bool type", exp.pos)) else Seq()) ++
     Consistency.checkPure(exp)
 

src/main/scala/viper/silver/ast/utility/Consistency.scala

@@ -90,6 +90,9 @@ object Consistency {
   /** Returns true if the given node contains no location accesses. */
   def noLocationAccesses(n: Node) = !n.existsDefined { case _: LocationAccess => }
 
+  /** Returns true if the given node contains no asserting expressions. */
+  def noAsserting(n: Node) = !n.existsDefined { case _: Asserting => }
+
   /** Returns true if the given node contains no accessibility predicates (unfolding predicates is
     * allowed) and no magic wands (applying wands is allowed).
     */

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

@@ -0,0 +1,15 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+domain foo  {
+  function bar(): Bool
+
+  axiom {
+    //:: ExpectedOutput(consistency.error)
+    asserting (true) in true
+  }
+}
+
+function baz(): Int
+  requires bar()