From ac90a9e0943b306329a9e39aee304b9446391aa6 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 15 Jan 2016 16:11:42 +0100
Subject: [PATCH] assert should be injected after xlang
---
.../scala/leon/utils/PreprocessingPhase.scala | 2 +-
.../scala/leon/verification/InjectAsserts.scala | 2 --
.../verification/xlang/valid/Array6.scala | 17 +++++++++++++++++
3 files changed, 18 insertions(+), 3 deletions(-)
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array6.scala
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 7bfeece2f..4a395912a 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -37,7 +37,6 @@ class PreprocessingPhase(desugarXLang: Boolean = false) extends LeonPhase[Progra
TypingPhase andThen
synthesis.ConversionPhase andThen
CheckADTFieldsTypes andThen
- InjectAsserts andThen
InliningPhase
val pipeX = if(desugarXLang) {
@@ -50,6 +49,7 @@ class PreprocessingPhase(desugarXLang: Boolean = false) extends LeonPhase[Progra
val phases =
pipeBegin andThen
pipeX andThen
+ InjectAsserts andThen
FunctionClosure andThen
AdaptationPhase andThen
debugTrees("Program after pre-processing")
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index a2ba463a6..4e126827b 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -30,8 +30,6 @@ object InjectAsserts extends SimpleLeonPhase[Program, Program] {
Assert(indexUpTo(i, ArrayLength(a)), Some("Array index out of range"), i).setPos(i),
v
).setPos(e))
- case e @ ArrayUpdate(a, i, _) =>
- Some(Assert(indexUpTo(i, ArrayLength(a)), Some("Array index out of range"), e).setPos(e))
case e @ MapApply(m,k) =>
Some(Assert(MapIsDefinedAt(m, k), Some("Map undefined at this index"), e).setPos(e))
diff --git a/src/test/resources/regression/verification/xlang/valid/Array6.scala b/src/test/resources/regression/verification/xlang/valid/Array6.scala
new file mode 100644
index 000000000..ffcc9e362
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array6.scala
@@ -0,0 +1,17 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object Array6 {
+
+ def test(): Int = {
+ var c = 1
+ val a = Array(0,1,2,3)
+ a({
+ if(a(0) == 0) { c = c+1; 1}
+ else { c = c+2; 2}
+ }) = { c = c*2; -1}
+ c
+ } ensuring(res => res == 4)
+
+}
--
GitLab