diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala index 6c4382ff71f676601f651b0e7aa6ea369e05e5bf..735462cd4acecaad24139b444b7f9e7f98fbbda0 100644 --- a/src/main/scala/leon/ArrayTransformation.scala +++ b/src/main/scala/leon/ArrayTransformation.scala @@ -49,6 +49,18 @@ object ArrayTransformation extends Pass { ).setType(UnitType) res } + case up@ArrayUpdated(a, i, v) => { + val ra = transform(a) + val ri = transform(i) + val rv = transform(v) + val length = ArrayLength(ra) + val res = IfExpr( + And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)), + ArrayUpdated(ra, ri, rv).setType(ra.getType).setPosInfo(up), + Error("Index out of bound").setType(ra.getType).setPosInfo(up) + ).setType(ra.getType) + res + } case Let(i, v, b) => { v.getType match { case ArrayType(_) => { diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala index b183a36fd0959b1847d8115a84d8e2c2075edf4a..13b6392edbaf0e61d0182c27e327610d76d64edc 100644 --- a/src/main/scala/leon/plugin/Extractors.scala +++ b/src/main/scala/leon/plugin/Extractors.scala @@ -636,6 +636,9 @@ trait Extractors { def unapply(tree: Apply): Option[(Tree,Tree,Tree)] = tree match { case Apply(TypeApply(Select(lhs, n), typeTreeList), List(from, to)) if (n.toString == "updated") => Some((lhs, from, to)) + case Apply( + Apply(TypeApply(Select(Apply(_, Seq(lhs)), n), _), Seq(index, value)), + List(Apply(_, _))) if (n.toString == "updated") => Some((lhs, index, value)) case _ => None } } @@ -667,9 +670,9 @@ trait Extractors { case Select(t, n) if (n.toString == "length") => Some(t) case _ => None } - } + object ExArrayFill { def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match { case Apply(