From 11f8701232dc702b6fd173268888d71290e482d7 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Sat, 28 Dec 2024 20:08:25 +0100 Subject: [PATCH] Storing if conditions to temp vars to fix issue #420 --- silver | 2 +- .../viper/carbon/modules/impls/DefaultStmtModule.scala | 7 ++++++- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/silver b/silver index b9f72722..f8b1c822 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit b9f7272234d6c2a2b84e140979d1b282c74ecba1 +Subproject commit f8b1c82279d3f835d78ff78d77b28171c6640486 diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala index 38b0ae28..bd14336d 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala @@ -43,6 +43,7 @@ class DefaultStmtModule(val verifier: Verifier) extends StmtModule with SimpleSt private val lblNamespace = verifier.freshNamespace("stmt.lbl") var lblVarsNamespace = verifier.freshNamespace("var.lbl") + private val tmpVarsNamespace = verifier.freshNamespace("stmt.tmpvar") override def labelNamespace = lblNamespace def name = "Statement module" @@ -209,8 +210,12 @@ class DefaultStmtModule(val verifier: Verifier) extends StmtModule with SimpleSt Nil case i@sil.If(cond, thn, els) => val condTr = if(allStateAssms == TrueLit()) { translateExpInWand(cond) } else { allStateAssms ==> translateExpInWand(cond) } + val condTempVar = LocalVar(Identifier("condition")(tmpVarsNamespace), Bool) checkDefinedness(cond, errors.IfFailed(cond), insidePackageStmt = insidePackageStmt) ++ - If(condTr, + // Assign the condition to a temp var s.t. it's safe to optimize away the following if it's empty without + // losing triggering expressions in the if-condition (see Carbon issue #420). + Assign(condTempVar, condTr) ++ + If(condTempVar, translateStmt(thn, statesStack, allStateAssms, insidePackageStmt), translateStmt(els, statesStack, allStateAssms, insidePackageStmt)) case sil.Label(name, _) => {