From 8638bfab901dc27e0e5a9a679774be4f43119024 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 27 Sep 2024 10:54:38 +0200 Subject: [PATCH 1/2] Initial implementation of asserting a in e --- silver | 2 +- .../viper/carbon/modules/impls/DefaultExpModule.scala | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/silver b/silver index 10b1b26a..f649c0ba 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 10b1b26a20957e5f000bf1bbcd4017145148afd7 +Subproject commit f649c0baf2fc133a5d99261dbb567b8a33732588 diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala index 73c7a296..ff81c55a 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala @@ -79,6 +79,7 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes case sil.Unfolding(_, exp) => translateExp(exp) case sil.Applying(_, exp) => translateExp(exp) + case sil.Asserting(_, exp) => translateExp(exp) case sil.Old(exp) => val prevState = stateModule.state stateModule.replaceState(stateModule.oldState) @@ -378,6 +379,13 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes checkDefinednessImpl(e1, error, makeChecks = makeChecks, definednessStateOpt) :: // short-circuiting evaluation: If(UnExp(Not, translateExp(e1)), checkDefinednessImpl(e2, error, makeChecks = makeChecks, definednessStateOpt), Statements.EmptyStmt) :: Nil + case sil.Asserting(assertion, e) => + val checkAssDefined = checkDefinedness(assertion, error, makeChecks = makeChecks) + val (stateStmt, state) = stateModule.freshTempState("asserting") + val checkAssHolds = MaybeComment("Exhale assertion of asserting", exhale(Seq((assertion, error, Some(error))))) + stateModule.replaceState(state) + val checkEDefined = checkDefinedness(e, error, makeChecks = makeChecks) + checkAssDefined :: stateStmt :: checkAssHolds :: checkEDefined :: Nil case w@sil.MagicWand(_, _) => checkDefinednessWand(w, error, makeChecks = makeChecks) case sil.Let(v, e, body) => From 9e6697eb3f527f3e651a1700321473d9007fd226 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 13 Nov 2024 17:00:10 +0100 Subject: [PATCH 2/2] Updating silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index f649c0ba..5f5c0220 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit f649c0baf2fc133a5d99261dbb567b8a33732588 +Subproject commit 5f5c02202030b67c0cf90d8540d26ca3d71c9bd6