fixes and regression tests for viperproject#581

Pointerbender · May 27, 2022 · 87f22d1 · 87f22d1
1 parent 5503e4a
commit 87f22d1
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 2 deletions.
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
@@ -463,7 +463,6 @@ case class PDestructorCall(name: String, rcv: PExp)
   override def args: Seq[PExp] = Seq(rcv)
 
   override def translateExp(t: Translator): Exp = {
-    val actualRcv = t.exp(rcv)
     val so: Option[Map[TypeVar, Type]] = adtSubstitution match {
       case Some(ps) => Some(ps.m.map(kv => TypeVar(kv._1) -> t.ttyp(kv._2)))
       case None => None
@@ -472,6 +471,10 @@ case class PDestructorCall(name: String, rcv: PExp)
       case Some(s) =>
         val adt = t.getMembers()(this.adt.idndef.name).asInstanceOf[Adt]
         assert(s.keys.toSet == adt.typVars.toSet)
+        val actualRcv = rcv match {
+          case pr@PResultLit() => Result(AdtType(adt, s))(t.liftPos(pr))
+          case _ => t.exp(rcv)
+        }
         AdtDestructorApp(adt, name, actualRcv, s)(t.liftPos(this))
       case _ => sys.error("type unification error - should report and not crash")
     }
@@ -496,7 +499,6 @@ case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)
   override def args: Seq[PExp] = Seq(rcv)
 
   override def translateExp(t: Translator): Exp = {
-    val actualRcv = t.exp(rcv)
     val so: Option[Map[TypeVar, Type]] = adtSubstitution match {
       case Some(ps) => Some(ps.m.map(kv => TypeVar(kv._1) -> t.ttyp(kv._2)))
       case None => None
@@ -505,6 +507,10 @@ case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)
       case Some(s) =>
         val adt = t.getMembers()(this.adt.idndef.name).asInstanceOf[Adt]
         assert(s.keys.toSet == adt.typVars.toSet)
+        val actualRcv = rcv match {
+          case pr@PResultLit() => Result(AdtType(adt, s))(t.liftPos(pr))
+          case _ => t.exp(rcv)
+        }
         AdtDiscriminatorApp(adt, name.name, actualRcv, s)(t.liftPos(this))
       case _ => sys.error("type unification error - should report and not crash")
     }

diff --git a/src/test/resources/adt/issue-581.vpr b/src/test/resources/adt/issue-581.vpr
@@ -0,0 +1,17 @@
+adt Test {
+    A()
+    B(b: Int)
+}
+
+function foo(): Test
+    ensures result.isA
+{
+    A()
+}
+
+function bar(): Test
+    ensures result.isB
+    ensures result.b == 42
+{
+    B(42)
+}