Merge pull request viperproject#531 from viperproject/meilers_asserting

Support for new expression asserting a in e
viper-admin · Nov 13, 2024 · 0fe38f7 · 0fe38f7
2 parents d14a703 + 9e6697e
commit 0fe38f7
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
diff --git a/silver b/silver
diff --git 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) =>
+5 −0		src/main/scala/viper/silver/ast/Expression.scala
+1 −1		src/main/scala/viper/silver/ast/Program.scala
+2 −0		src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+4 −1		src/main/scala/viper/silver/ast/utility/Expressions.scala
+1 −0		src/main/scala/viper/silver/ast/utility/Nodes.scala
+7 −2		src/main/scala/viper/silver/parser/FastParser.scala
+6 −0		src/main/scala/viper/silver/parser/ParseAst.scala
+2 −0		src/main/scala/viper/silver/parser/ParseAstKeyword.scala
+2 −0		src/main/scala/viper/silver/parser/Translator.scala
+38 −0		src/test/resources/all/asserting/function.vpr
+19 −0		src/test/resources/all/asserting/other-fail.vpr
+44 −0		src/test/resources/all/asserting/qp.vpr
+73 −0		src/test/resources/all/asserting/simple-fail.vpr
+22 −0		src/test/resources/all/asserting/trigger.vpr
+17 −0		src/test/resources/all/asserting/wand.vpr