Merge pull request #1297 from utwente-fmt/issue-924

Fixed issue #924: context_everywhere was not propagated correctly in run methods.

src/col/vct/col/origin/Blame.scala

@@ -359,6 +359,16 @@ case class ContextEverywhereFailedInPost(
   override def inlineDescWithSource(node: String, failure: String): String =
     s"Context of `$node` may not hold in the postcondition, since $failure."
 }
+case class ContextEverywhereFailedInRunPost(
+    failure: ContractFailure,
+    node: RunMethod[_],
+) extends ContractedFailure with WithContractFailure {
+  override def baseCode: String = "contextRunPostFailed"
+  override def descInContext: String =
+    "Context may not hold in postcondition, since"
+  override def inlineDescWithSource(node: String, failure: String): String =
+    s"Context of `$node` may not hold in the postcondition, since $failure."
+}
 case class AutoValueLeakCheckFailed(
     failure: ContractFailure,
     node: ContractApplicable[_],

src/rewrite/vct/rewrite/PropagateContextEverywhere.scala

@@ -24,6 +24,12 @@ case object PropagateContextEverywhere extends RewriterBuilder {
     override def blame(error: PostconditionFailed): Unit =
       app.blame.blame(ContextEverywhereFailedInPost(error.failure, app))
   }
+
+  case class ContextEverywhereRunPostconditionFailed(app: RunMethod[_])
+    extends Blame[PostconditionFailed] {
+    override def blame(error: PostconditionFailed): Unit =
+      app.blame.blame(ContextEverywhereFailedInRunPost(error.failure, app))
+  }
 }
 
 case class PropagateContextEverywhere[Pre <: Generation]()
@@ -60,6 +66,19 @@ case class PropagateContextEverywhere[Pre <: Generation]()
             }
           },
         ))
+      case runMethod: RunMethod[Pre] =>
+        allScopes.anyDeclare(allScopes.anySucceedOnly(
+          runMethod,
+          invariants.having(
+            invariants.top ++ unfoldStar(runMethod.contract.contextEverywhere)
+          ) {
+                runMethod.rewrite(blame =
+                  PostBlameSplit
+                    .left(ContextEverywhereRunPostconditionFailed(runMethod), runMethod.blame)
+                )
+          },
+        ))
+
       case other => rewriteDefault(other)
     }
 

test/main/vct/test/integration/examples/ForkJoinSpec.scala

@@ -9,4 +9,27 @@ class ForkJoinSpec extends VercorsSpec {
   vercors should verify using anyBackend example "concepts/forkjoin/fibonacci.pvl"
   vercors should verify using anyBackend examples("concepts/forkjoin/OwickiGries.pvl", "concepts/forkjoin/Worker.pvl")
   vercors should error withCode "runnableMethodMissing" example "concepts/forkjoin/TestFork.pvl"
+  vercors should verify using anyBackend in "The context_everywhere of a run method" pvl
+    """
+    pure int f();
+
+    class C {
+      context_everywhere f() == 3;
+      run {
+        assert f() == 3;
+      }
+    }
+
+    requires f() == 3;
+    void main() {
+        C c = new C();
+        fork c;
+        join c;
+    }
+    """
+
+
+
+
+
 }