Remove comment + test for revealing closure

viperproject · Feb 8, 2024 · 0d5fc69 · 0d5fc69
1 parent bcd8ef6
commit 0d5fc69
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 22 deletions.
diff --git 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