From 2454f6402085f930be29ffa674f71f1cfce67ea0 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 11 May 2016 18:26:05 +0200
Subject: [PATCH] quick fix for old keyword
---
.../leon/xlang/ImperativeCodeElimination.scala | 16 ++++++++++++++++
1 file changed, 16 insertions(+)
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 6326ff8e4..cf70d2eb1 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -25,7 +25,23 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
} {
val (res, scope, _) = toFunction(body)(State(fd, Set(), Map()))
fd.body = Some(scope(res))
+
}
+
+ //probably not the cleanest way to do it, but if somehow we still have Old
+ //expressions at that point, they can be safely removed as the object is
+ //equals to its original value
+ for {
+ fd <- pgm.definedFunctions
+ } {
+ fd.postcondition = fd.postcondition.map(post => {
+ preMap{
+ case Old(v) => Some(v.toVariable)
+ case _ => None
+ }(post)
+ })
+ }
+
}
/* varsInScope refers to variable declared in the same level scope.
--
GitLab