From f7c035fe4ed443fcd9863f423fcb64cabc7ccd1a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 28 Mar 2012 16:42:37 +0200
Subject: [PATCH] fixing some bug with the substitution of vars in the
postcondition
---
mytest/Abs.scala | 21 +++++++++++--------
.../leon/ImperativeCodeElimination.scala | 7 ++++---
2 files changed, 16 insertions(+), 12 deletions(-)
diff --git a/mytest/Abs.scala b/mytest/Abs.scala
index 3774d5daa..d18929903 100644
--- a/mytest/Abs.scala
+++ b/mytest/Abs.scala
@@ -3,19 +3,22 @@ import leon.Utils._
object Abs {
- def abs(tab: Map[Int, Int], size: Int, j: Int): Map[Int, Int] = {
- require(j >= 0 && j < size && tab.isDefinedAt(j) && size > 0)
+ def abs(tab: Map[Int, Int], size: Int, j: Int): Map[Int, Int] = ({
+ require(j >= 0 && j < size && size > 0)
var k = 0
var tabres = Map.empty[Int, Int]
(while(k < size) {
- if(tab(k) < 0)
- tabres = tabres.updated(k, -tab(k))
- else
- tabres = tabres.updated(k, tab(k))
+ if(tab.isDefinedAt(k)) {
+ if(tab(k) < 0)
+ tabres = tabres.updated(k, -tab(k))
+ else
+ tabres = tabres.updated(k, tab(k))
+ } else {
+ tabres = tabres.updated(k, 0)
+ }
k = k + 1
- }) invariant(k >= 0)
+ }) invariant(k >= 0 && (if(j < k) tabres(j) >= 0 else true))
tabres
-
- }
+ }) ensuring(res => res(j) >= 0)
}
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index 17248c50d..f59479c74 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -91,14 +91,15 @@ object ImperativeCodeElimination extends Pass {
Map(whileFunVars.head.toVariable -> resVar)
else
whileFunVars.zipWithIndex.map{ case (v, i) => (v.toVariable, TupleSelect(resVar, i+1).setType(v.getType)) }.toMap
- val modifiedVars2ResultVars: Map[Expr, Expr] = modifiedVars.map(v => (v.toVariable, modifiedVars2WhileFunVars(v.toVariable))).toMap
+ val modifiedVars2ResultVars: Map[Expr, Expr] = modifiedVars.map(v => (v.toVariable, whileFunVars2ResultVars(modifiedVars2WhileFunVars(v.toVariable)))).toMap
val trivialPostcondition: Option[Expr] = Some(Not(replace(whileFunVars2ResultVars, whileFunCond)))
val invariantPrecondition: Option[Expr] = wh.invariant.map(expr => replace(modifiedVars2WhileFunVars, expr))
+ val invariantPostcondition: Option[Expr] = wh.invariant.map(expr => replace(modifiedVars2ResultVars, expr))
whileFunDef.precondition = invariantPrecondition
whileFunDef.postcondition = trivialPostcondition.map(expr =>
- And(expr, invariantPrecondition match {
- case Some(e) => replace(modifiedVars2ResultVars, e)
+ And(expr, invariantPostcondition match {
+ case Some(e) => e
case None => BooleanLiteral(true)
}))
--
GitLab