Merge pull request #875 from viperproject/meilers_asserting

Support for new asserting expressions
viperproject · Nov 13, 2024 · 115f3f4 · 115f3f4
2 parents 26091b7 + 4ca6695
commit 115f3f4
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 1 deletion.
diff --git a/silver b/silver
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
@@ -1029,6 +1029,12 @@ object evaluator extends EvaluationRules {
           Option.when(withExp)(s.relevantQuantifiedVariables.map(_._2.get)), v))((s4, r4, v4)
           => Q(s4, r4._1, r4._2, v4))
 
+      case ast.Asserting(eAss, eIn) =>
+        consume(s, eAss, pve, v)((s2, _, v2) => {
+          val s3 = s2.copy(g = s.g, h = s.h)
+          eval(s3, eIn, pve, v2)(Q)
+        })
+
       /* Sequences */
 
       case ast.SeqContains(e0, e1) => evalBinOp(s, e1, e0, SeqIn, pve, v)((s1, t, e1New, e0New, v1) =>

diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
@@ -128,6 +128,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
       case loc: ast.LocationAccess => getOrFail(data.locToSnap, loc, toSort(loc.typ), Option.when(Verifier.config.enableDebugging())(extractPTypeFromExp(loc)))
       case ast.Unfolding(_, eIn) => translate(toSort)(eIn)
       case ast.Applying(_, eIn) => translate(toSort)(eIn)
+      case ast.Asserting(_, eIn) => translate(toSort)(eIn)
 
       case eFApp: ast.FuncApp =>
         val silverFunc = program.findFunction(eFApp.funcname)
+5 −0		src/main/scala/viper/silver/ast/Expression.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