Forbid ADT discriminators in triggers and adapt test

Author: marcoeilers

Diff for: src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala

@@ -314,9 +314,11 @@ case class AdtDiscriminatorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, T
     }
   }
 
-  override def extensionIsValidTrigger(): Boolean = !rcv.existsDefined(Expressions.isForbiddenInTrigger)
+  // Since a discriminator desugars to ADT_tag(rcv) == name_tag, which contains an equality,
+  // it cannot be used anywhere inside a trigger.
+  override def extensionIsValidTrigger(): Boolean = false
 
-  override def extensionIsForbiddenInTrigger(): Boolean = false
+  override def extensionIsForbiddenInTrigger(): Boolean = true
 }
 
 object AdtDiscriminatorApp {

Diff for: src/test/resources/all/issues/silver/0849.vpr

@@ -46,14 +46,9 @@ method testDestr2(s: Set[Term], c: Term) {
 
 method testDiscr(s: Set[Term], c: Term) {
   assume c in s
-  assume forall i: Term :: {i.isConst} i in s ==> foo(i)
+  // i.isConst must not be picked as a trigger, otherwise the backends may crash
+  assume forall i: Term :: i.isConst ==> foo(i)
   var t: Bool := c.isConst
   assert foo(c)
 }
 
-method testDiscr2(s: Set[Term], c: Term) {
-  assume c in s
-  assume forall i: Term :: {i.isConst} i in s ==> foo(i)
-  //:: ExpectedOutput(assert.failed:assertion.false)
-  assert foo(c)
-}

Diff for: src/test/resources/all/issues/silver/0849_2.vpr

@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+adt Term {
+  Const(n: Int)
+}
+
+domain theory {
+  function foo(t: Term): Bool
+
+  axiom ax1 { forall n: Int ::
+    {Const(n)}      // Type checker error
+    {foo(Const(n))} // OK
+    foo(Const(n))
+  }
+}
+
+
+method testDiscr(s: Set[Term], c: Term) {
+  assume c in s
+  //:: ExpectedOutput(typechecker.error)
+  assume forall i: Term :: {i.isConst} i in s ==> foo(i)
+  assert foo(c)
+}