Implements PR suggestions by Joao

src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala

@@ -144,9 +144,10 @@ trait NameResolution {
       case _ => violation("PIdnUnk always has a parent")
     }
 
-  // technically, `isGhostDef` should consider for implementation proofs whether the method getting implemented is ghost
-  // however, since implementation proofs are syntactically restricted, we assume for now that definitions in all
-  // implementation proofs are non-ghost.
+  // technically, `isGhostDef` should consider for implementation proofs whether the method getting implemented is ghost or not.
+  // however, we treat all implementation proofs as non-ghost and ignore whether an implementation proof is related to a
+  // ghost or actual method because the implementation proof is syntactically restricted and can only call the implemented
+  // method and/or fold and unfold the interface's predicate.
   private[resolution] lazy val isGhostDef: PNode => Boolean = n => isEnclosingGhost(n)
 
   private[resolution] def serialize(id: PIdnNode): String = id.name

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostWellDef.scala

@@ -144,7 +144,7 @@ trait GhostWellDef { this: TypeInfoImpl =>
       if (isEnclosingGhost(e)) {
         Violation.violation(exprType(e).isInstanceOf[GhostPointerT], s"Cannot allocate non-ghost memory in ghost code.")
       } else {
-        Violation.violation(exprType(e).isInstanceOf[ActualPointerT], s"All memory allocated within actual code must be located on the actual heap")
+        Violation.violation(exprType(e).isInstanceOf[ActualPointerT], s"Cannot allocate ghost memory in non-ghost code.")
       }
       noMessages
 

src/test/resources/regressions/features/interfaces/ghostnessOfImplementation-fail1.gobra

@@ -0,0 +1,65 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// this test makes sure that a method's implementation has the same ghostness as specified in the interface
+
+package pkg
+
+type itfWithActualMethod interface {
+    decreases
+    actualMethod() int
+}
+
+type itfWithActualPureMethod interface {
+    decreases
+    pure actualPureMethod() int
+}
+
+type itfWithGhostMethod interface {
+    ghost
+    decreases
+    ghostMethod() int
+}
+
+type itfWithGhostPureMethod interface {
+    ghost
+    decreases
+    pure ghostPureMethod() int
+}
+
+type someImplementation struct {
+    value int
+}
+
+// checks that `someImplementation` is indeed considered an implementation of each interface, i.e., that the ghost
+// attribute in the interface and implementation is correctly handled.
+//:: ExpectedOutput(type_error)
+*someImplementation implements itfWithActualMethod
+//:: ExpectedOutput(type_error)
+*someImplementation implements itfWithActualPureMethod
+//:: ExpectedOutput(type_error)
+*someImplementation implements itfWithGhostMethod
+//:: ExpectedOutput(type_error)
+*someImplementation implements itfWithGhostPureMethod
+
+ghost
+decreases
+func (impl *someImplementation) actualMethod() int {
+    return 42
+}
+
+ghost
+decreases
+pure func (impl *someImplementation) actualPureMethod() int {
+    return 42
+}
+
+decreases
+func (impl *someImplementation) ghostMethod() int {
+    return 42
+}
+
+decreases
+pure func (impl *someImplementation) ghostPureMethod() int {
+    return 42
+}

src/test/resources/regressions/issues/000037.gobra → src/test/resources/regressions/issues/000037-1.gobra

@@ -8,12 +8,17 @@ type Rectangle struct {
 }
 
 ghost
+decreases
 pure func GetHeight(r Rectangle) (res int) {
     return r.Height
 }
 
 func main() {
+    someActualVariable := 42
     r := Rectangle{Width: 2, Height: 5}
     h := GetHeight(r)
     assert h == GetHeight(r) && h == 5
-}
+    // h is implicitly a ghost variable. Thus, the following assignment (to a non-ghost variable) should fail:
+    //:: ExpectedOutput(type_error)
+    someActualVariable = h
+}

src/test/resources/regressions/issues/000037-2.gobra

@@ -0,0 +1,29 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+ghost
+decreases x
+pure func more(x int) int {
+  return x <= 0 ? 1 : more(x - 2) + 3
+}
+
+ghost /* lemma */
+decreases x
+ensures x < more(x)
+func increasing(x int)
+
+// returning b (a ghost variable) is not allowed as this is an actual function
+//:: ExpectedOutput(type_error)
+func exampleLemmaUse(a int) int {
+  increasing(a)
+  b := more(a)
+  c := more(b)
+  if a < 1000 {
+    increasing(more(a))
+    assert 2 <= c - a
+  }
+  assert 2 <= c - a || 200 <= a
+  return b
+}