Skip to content

Commit

Permalink
Merge pull request viperproject#774 from viperproject/meilers_fix_773
Browse files Browse the repository at this point in the history
Fixing issue viperproject#773
  • Loading branch information
marcoeilers authored Nov 10, 2023
2 parents cabada8 + 9da0777 commit da2f36f
Showing 1 changed file with 14 additions and 8 deletions.
22 changes: 14 additions & 8 deletions src/main/scala/rules/Executor.scala
Original file line number Diff line number Diff line change
Expand Up @@ -253,13 +253,8 @@ object executor extends ExecutionRules {
phase1data = phase1data :+ (s1,
v1.decider.pcs.after(mark),
v1.decider.freshFunctions /* [BRANCH-PARALLELISATION] */)
v1.decider.prover.comment("Loop head block: Check well-definedness of edge conditions")
edgeConditions.foldLeft(Success(): VerificationResult) {
case (result, _) if !result.continueVerification => result
case (intermediateResult, eCond) =>
intermediateResult combine executionFlowController.locally(s1, v1)((s2, v2) => {
eval(s2, eCond, WhileFailed(eCond), v2)((_, _, _) =>
Success())})}})})
Success()
})})
combine executionFlowController.locally(s, v)((s0, v0) => {
v0.decider.prover.comment("Loop head block: Establish invariant")
consumes(s0, invs, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => {
Expand All @@ -276,8 +271,19 @@ object executor extends ExecutionRules {
Success()
else {
execs(s3, stmts, v2)((s4, v3) => {
val edgeCondWelldefinedness = {
v1.decider.prover.comment("Loop head block: Check well-definedness of edge conditions")
edgeConditions.foldLeft(Success(): VerificationResult) {
case (result, _) if !result.continueVerification => result
case (intermediateResult, eCond) =>
intermediateResult combine executionFlowController.locally(s4, v3)((s5, v4) => {
eval(s5, eCond, WhileFailed(eCond), v4)((_, _, _) =>
Success())
})
}
}
v3.decider.prover.comment("Loop head block: Follow loop-internal edges")
follows(s4, sortedEdges, WhileFailed, v3, joinPoint)(Q)})}})}})}))
edgeCondWelldefinedness combine follows(s4, sortedEdges, WhileFailed, v3, joinPoint)(Q)})}})}})}))

case _ =>
/* We've reached a loop head block via an edge other than an in-edge: a normal edge or
Expand Down

0 comments on commit da2f36f

Please sign in to comment.