From 0d5fc69f2921269b7946a6bd5b9d7eb256ab1693 Mon Sep 17 00:00:00 2001
From: dnezam <55559979+dnezam@users.noreply.github.com>
Date: Thu, 8 Feb 2024 12:41:22 +0100
Subject: [PATCH] Remove comment + test for revealing closure

---
 .../scala/viper/gobra/frontend/Desugar.scala  |  2 --
 .../opaque/reveal-closure-fail1.gobra         | 20 -------------------
 2 files changed, 22 deletions(-)
 delete mode 100644 src/test/resources/regressions/features/opaque/reveal-closure-fail1.gobra

diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala
index de34b6338..10973fdca 100644
--- a/src/main/scala/viper/gobra/frontend/Desugar.scala
+++ b/src/main/scala/viper/gobra/frontend/Desugar.scala
@@ -3239,8 +3239,6 @@ object Desugar extends LazyLogging {
           val isOpaque = m.spec.isOpaque
 
           val mem = if (m.spec.isPure) {
-            // Not sure whether passing opaque here instead of raising a violation if opaque
-            // is true is correct, since this doesn't seem to be a normal method/function call.
             in.PureMethod(recv, proxy, args, returns, pres, posts, terminationMeasures, None, isOpaque)(src)
           } else {
             in.Method(recv, proxy, args, returns, pres, posts, terminationMeasures, None)(src)
diff --git a/src/test/resources/regressions/features/opaque/reveal-closure-fail1.gobra b/src/test/resources/regressions/features/opaque/reveal-closure-fail1.gobra
deleted file mode 100644
index 496fa2ca3..000000000
--- a/src/test/resources/regressions/features/opaque/reveal-closure-fail1.gobra
+++ /dev/null
@@ -1,20 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-package pkg
-
-func main() {
-	x@ := 0
-	c := preserves acc(&x)
-		 ensures x == old(x) + n && m == x
-		 func f(n int) (m int) {
-			x += n;
-			return x
-		 }
-
-	// QUES: Not sure how to test that we cannot reveal closure calls; the following
-	// doesn't parse
-	r := reveal (c(10) as f)
-	assert x == 10 && r == 10
-
-}