From 8683c56a306f359238d586a9125b31578a6eac6d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Mon, 7 May 2012 01:44:32 +0000
Subject: [PATCH] stop using an dummy int for the translation of array update
---
src/main/scala/leon/ArrayTransformation.scala | 18 ++++++++----------
1 file changed, 8 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 6a2afc155..71ff17c26 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -90,16 +90,14 @@ object ArrayTransformation extends Pass {
val array = TupleSelect(ar, 1).setType(ArrayType(v.getType))
IfExpr(
And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
- Block(Seq(
- Assignment(
- id,
- Tuple(Seq(
- ArrayUpdated(array, ir, vr).setType(array.getType).setPosInfo(up),
- length)
- ).setType(TupleType(Seq(array.getType, Int32Type))))),
- IntLiteral(0)),
- Error("Index out of bound").setType(Int32Type).setPosInfo(up)
- ).setType(Int32Type)
+ Assignment(
+ id,
+ Tuple(Seq(
+ ArrayUpdated(array, ir, vr).setType(array.getType).setPosInfo(up),
+ length)
+ ).setType(TupleType(Seq(array.getType, Int32Type)))),
+ Error("Index out of bound").setType(UnitType).setPosInfo(up)
+ ).setType(UnitType)
}
case ArrayLength(a) => {
val ar = transform(a)
--
GitLab