(AdtPlugin) fixes and regression tests for #581

src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala

@@ -119,6 +119,21 @@ class AdtPlugin(reporter: viper.silver.reporter.Reporter,
         PFieldAssign(PFieldAccess(transformStrategy(fieldAcc.rcv), fieldAcc.idnuse)(fieldAcc.pos), transformStrategy(rhs))(pfa.pos)
       case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorArgsNames.exists(_.name == idnuse.name) => PDestructorCall(idnuse.name, rcv)(pfa.pos)
       case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorNames.exists("is" + _.name == idnuse.name) => PDiscriminatorCall(PIdnUse(idnuse.name.substring(2))(idnuse.pos), rcv)(pfa.pos)
+      case pr@PResultLit() => {
+        // The transformations applied to the return type of the parent `PFunction` are not known to the `PResultLit`.
+        // This is hack to make the return type known despite that, see https://github.com/viperproject/silver/issues/581.
+        var par: PNode = pr.parent.get
+        while (!par.isInstanceOf[PFunction]) {
+          if (par == null) sys.error("cannot use 'result' outside of function")
+          val nextpar = par.parent.get
+          if (nextpar.isInstanceOf[PFunction]) {
+            val func = nextpar.asInstanceOf[PFunction]
+            par.parent = Some(func.copy(typ = transformStrategy(func.typ))(func.pos))
+          }
+          par = par.parent.get
+        }
+        pr
+      }
     }).recurseFunc({
       // Stop the recursion if a destructor call or discriminator call is parsed as left-hand side of a field assignment
       case PFieldAssign(fieldAcc, _) if declaredConstructorArgsNames.exists(_.name == fieldAcc.idnuse.name) ||

src/test/resources/adt/issue-581.vpr

@@ -0,0 +1,31 @@
+adt Test {
+    A()
+    B(b: Int)
+}
+
+function foo(): Test
+    ensures result.isA
+{
+    A()
+}
+
+function bar(): Test
+    ensures result.isB
+    ensures result.b == 42
+    ensures inv(result)
+{
+    B(42)
+}
+
+function inv(t: Test): Bool {
+    t.isB && t.b > 10
+}
+
+// FIXME: this triggers an error: [typechecker.error] expected identifier, but got PAdtConstructor(PIdnDef(A),List())
+// FIXME: due to `PBinExp` losing its information about `parent`, see https://github.com/viperproject/silver/issues/581
+// function baz(): Test
+//     ensures A() == result
+//     ensures result == A()
+// {
+//     A
+// }