add check for ghost pure members too

viperproject · Feb 5, 2025 · ded98e5 · ded98e5
1 parent dc71130
commit ded98e5
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala
@@ -49,7 +49,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
       isSingleResultArg(member) ++
         isSinglePureReturnExpr(member) ++
         isPurePostcondition(member.spec) ++
-        nonVariadicArguments(member.args)
+        nonVariadicArguments(member.args) ++
+        member.spec.posts.flatMap(hasOldExpression)
     } else noMessages
   }