From 374c94b19c2e6a92e11a24803f0d4180cf29218a Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Thu, 17 Oct 2024 11:32:48 +0200
Subject: [PATCH] Error on resource value used as return type.

Related: #1267.
---
 .../vct/rewrite/EncodeResourceValues.scala       | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/rewrite/vct/rewrite/EncodeResourceValues.scala b/src/rewrite/vct/rewrite/EncodeResourceValues.scala
index 8b4054518..91f54c1e8 100644
--- a/src/rewrite/vct/rewrite/EncodeResourceValues.scala
+++ b/src/rewrite/vct/rewrite/EncodeResourceValues.scala
@@ -12,6 +12,7 @@ import vct.col.util.DeclarationBox
 import vct.result.VerificationError.{SystemError, UserError}
 import vct.rewrite.EncodeResourceValues.{
   GenericsNotSupported,
+  ResourceValueReturnType,
   UnknownResourceValue,
   UnsupportedResourceValue,
   WrongResourcePattern,
@@ -45,6 +46,14 @@ case object EncodeResourceValues extends RewriterBuilder {
     override def text: String =
       node.o.messageInContext("Wrong resource pattern encoding")
   }
+
+  case class ResourceValueReturnType(m: AbstractMethod[_]) extends UserError {
+    override def text: String =
+      m.o.messageInContext(
+        "Resource values as method return types currently not supported because of https://github.com/utwente-fmt/vercors/issues/1267"
+      )
+    override def code: String = "resourceValueReturnType"
+  }
 }
 
 case class EncodeResourceValues[Pre <: Generation]()
@@ -458,4 +467,11 @@ case class EncodeResourceValues[Pre <: Generation]()
       case TResourceVal() => TAxiomatic(valAdt.top.ref, Nil)
       case other => rewriteDefault(other)
     }
+
+  override def dispatch(decl: Declaration[Pre]): Unit =
+    decl match {
+      case m: AbstractMethod[Pre] if m.returnType == TResourceVal[Pre]() =>
+        throw new ResourceValueReturnType(m)
+      case _ => super.dispatch(decl)
+    }
 }