From a932f79bf7ec02c56509af5c02ae9b6d78a97c27 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 26 Sep 2024 21:01:15 +0200 Subject: [PATCH 1/3] asserting (a) in e --- src/main/scala/rules/Evaluator.scala | 5 +++++ .../functions/HeapAccessReplacingExpressionTranslator.scala | 1 + 2 files changed, 6 insertions(+) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 943002243..11046c651 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -1029,6 +1029,11 @@ 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)((_, _, _) => { + eval(s, eIn, pve, v)(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 index 02dd6d9f0..4b70d2140 100644 --- 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) From 562b9fe3b90f5b55c5cd3da0ee3b540227cef52d Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 27 Sep 2024 10:55:12 +0200 Subject: [PATCH 2/3] Update silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 10b1b26a2..f649c0baf 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 10b1b26a20957e5f000bf1bbcd4017145148afd7 +Subproject commit f649c0baf2fc133a5d99261dbb567b8a33732588 From 52f94d26e9d66693e28fa7489368b5ee350accec Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 4 Oct 2024 13:32:13 +0200 Subject: [PATCH 3/3] Resetting heap instead of throwing away entire state after checking assertion --- src/main/scala/rules/Evaluator.scala | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 11046c651..b0d116432 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -1030,8 +1030,9 @@ object evaluator extends EvaluationRules { => Q(s4, r4._1, r4._2, v4)) case ast.Asserting(eAss, eIn) => - consume(s, eAss, pve, v)((_, _, _) => { - eval(s, eIn, pve, v)(Q) + consume(s, eAss, pve, v)((s2, _, v2) => { + val s3 = s2.copy(g = s.g, h = s.h) + eval(s3, eIn, pve, v2)(Q) }) /* Sequences */