From a8f9f3b694897867663bd1b8a7362eeaa05dcd20 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 21 Jul 2015 01:40:59 +0200
Subject: [PATCH] Remove mutation in tactics. Fix path-conditions of matchs
with guards
---
src/main/scala/leon/purescala/TransformerWithPC.scala | 7 ++++---
src/main/scala/leon/verification/Tactic.scala | 1 -
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala
index d098bedf9..f6dfaa543 100644
--- a/src/main/scala/leon/purescala/TransformerWithPC.scala
+++ b/src/main/scala/leon/purescala/TransformerWithPC.scala
@@ -33,10 +33,11 @@ abstract class TransformerWithPC extends Transformer {
val patternExprPos = conditionForPattern(rs, c.pattern, includeBinders = true)
val patternExprNeg = conditionForPattern(rs, c.pattern, includeBinders = false)
val map = mapForPattern(rs, c.pattern)
- val guard = replaceFromIDs(map, c.optGuard.getOrElse(BooleanLiteral(true)))
+ val guardOrTrue = c.optGuard.getOrElse(BooleanLiteral(true))
+ val guardMapped = replaceFromIDs(map, guardOrTrue)
- val subPath = register(patternExprPos, soFar)
- soFar = register(not(and(patternExprNeg, guard)), soFar)
+ val subPath = register(and(patternExprPos, guardOrTrue), soFar)
+ soFar = register(not(and(patternExprNeg, guardMapped)), soFar)
MatchCase(c.pattern, c.optGuard, rec(c.rhs,subPath)).copiedFrom(c)
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index b6cb76117..105c61d61 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -11,7 +11,6 @@ abstract class Tactic(vctx: VerificationContext) {
val description : String
def generateVCs(fd: FunDef): Seq[VC] = {
- fd.fullBody = matchToIfThenElse(fd.fullBody)
generatePostconditions(fd) ++
generatePreconditions(fd) ++
generateCorrectnessConditions(fd)
--
GitLab