From 0b2aa0d3b808cb7fa3bf55534edc890ccc74088b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 7 Apr 2016 16:53:00 +0200
Subject: [PATCH] update epsilon tests
---
.../leon/xlang/XLangDesugaringPhase.scala | 2 ++
.../verification/xlang/invalid/Epsilon7.scala | 19 ++++++++++++++
.../verification/xlang/invalid/Epsilon8.scala | 12 +++++++++
.../verification/xlang/invalid/Epsilon9.scala | 26 +++++++++++++++++++
.../verification/xlang/valid/Epsilon2.scala | 16 ------------
5 files changed, 59 insertions(+), 16 deletions(-)
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Epsilon7.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Epsilon8.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Epsilon9.scala
delete mode 100644 src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
diff --git a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
index b00935fcd..ae216dc62 100644
--- a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
+++ b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
@@ -17,7 +17,9 @@ object XLangDesugaringPhase extends LeonPhase[Program, Program] {
PrintTreePhase(title).when(ctx.reporter.isDebugEnabled(DebugSectionTrees))
val phases =
+ debugTrees("Program before starting xlang-desugaring") andThen
IntroduceGlobalStatePhase andThen
+ debugTrees("Program after introduce-global-state") andThen
AntiAliasingPhase andThen
debugTrees("Program after anti-aliasing") andThen
EpsilonElimination andThen
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon7.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon7.scala
new file mode 100644
index 000000000..3bbfde20d
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon7.scala
@@ -0,0 +1,19 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+import leon.lang._
+import leon.lang.xlang._
+
+object Epsilon7 {
+
+ def rand(): Int = epsilon((x: Int) => true)
+
+ //this used to be VALID until the introduction
+ //of a global state that can tracks epsilon calls
+ //and ensure each epsilon is invoked with a different
+ //seed value
+ def wrongProperty1(): Boolean = {
+ rand() == rand()
+ }.holds
+
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon8.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon8.scala
new file mode 100644
index 000000000..a95ff4ea7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon8.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+import leon.lang._
+import leon.lang.xlang._
+
+object Epsilon8 {
+
+ def wrongProp: Boolean = {
+ epsilon((y: Int) => true) == epsilon((y: Int) => true)
+ } holds
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon9.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon9.scala
new file mode 100644
index 000000000..c21e5333e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon9.scala
@@ -0,0 +1,26 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+import leon.lang._
+import leon.lang.xlang._
+
+object Epsilon9 {
+
+ def random(): BigInt = epsilon((x: BigInt) => true)
+
+ /*
+ * The implementation relies on a potential bug in random(), when
+ * two calls of random with the same args (0 here) will return
+ * the same value. If that's the case, then we can prove the
+ * postcondition. Epsilon should behave really randomly, so that
+ * postcondition should be invalid.
+ */
+ def findPositive(): BigInt = {
+ val x = random()
+ if(x < 0) {
+ -random()
+ } else {
+ x
+ }
+ } ensuring(res => res >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
deleted file mode 100644
index 6506c4d97..000000000
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-import leon.lang._
-import leon.lang.xlang._
-
-object Epsilon2 {
-
- def rand(): Int = epsilon((x: Int) => true)
-
- //this should hold, that is the expected semantic of our epsilon
- def property1(): Boolean = {
- rand() == rand()
- }.holds
-
-
-}
--
GitLab