From 643d6fb5d3f2682797146ce7536b48651322e18e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Sat, 16 Apr 2016 01:17:55 +0200
Subject: [PATCH] io library using implicit state

---
 library/io/StdIn.scala                        | 57 +++++++++++++++++++
 .../verification/xlang/invalid/StdIn1.scala   | 10 ++++
 .../verification/xlang/invalid/StdIn2.scala   | 13 +++++
 .../verification/xlang/invalid/StdIn3.scala   | 12 ++++
 .../verification/xlang/invalid/StdIn4.scala   | 10 ++++
 .../verification/xlang/valid/StdIn1.scala     | 11 ++++
 6 files changed, 113 insertions(+)
 create mode 100644 library/io/StdIn.scala
 create mode 100644 src/test/resources/regression/verification/xlang/invalid/StdIn1.scala
 create mode 100644 src/test/resources/regression/verification/xlang/invalid/StdIn2.scala
 create mode 100644 src/test/resources/regression/verification/xlang/invalid/StdIn3.scala
 create mode 100644 src/test/resources/regression/verification/xlang/invalid/StdIn4.scala
 create mode 100644 src/test/resources/regression/verification/xlang/valid/StdIn1.scala

diff --git a/library/io/StdIn.scala b/library/io/StdIn.scala
new file mode 100644
index 000000000..57012be57
--- /dev/null
+++ b/library/io/StdIn.scala
@@ -0,0 +1,57 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.io
+
+import leon.annotation._
+
+object StdIn {
+
+  @library
+  case class State(var seed: BigInt)
+
+  @library
+  def newState: State = State(0)
+
+  @library
+  @isabelle.noBody()
+  def readInt(implicit state: State): Int = {
+    state.seed += 1
+    nativeReadInt
+  }
+
+  @library
+  @extern
+  @isabelle.noBody()
+  private def nativeReadInt(implicit state: State): Int = {
+    scala.io.StdIn.readInt
+  } ensuring((x: Int) => true)
+
+  @library
+  @isabelle.noBody()
+  def readBigInt(implicit state: State): BigInt = {
+    state.seed += 1
+    nativeReadBigInt
+  }
+
+  @library
+  @extern
+  @isabelle.noBody()
+  private def nativeReadBigInt(implicit state: State): BigInt = {
+    BigInt(scala.io.StdIn.readInt)
+  } ensuring((x: BigInt) => true)
+
+  @library
+  @isabelle.noBody()
+  def readBoolean(implicit state: State): Boolean = {
+    state.seed += 1
+    nativeReadBoolean
+  }
+
+  @library
+  @extern
+  @isabelle.noBody()
+  private def nativeReadBoolean(implicit state: State): Boolean = {
+    scala.io.StdIn.readBoolean
+  } ensuring((x: Boolean) => true)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/StdIn1.scala b/src/test/resources/regression/verification/xlang/invalid/StdIn1.scala
new file mode 100644
index 000000000..aa3a326ff
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/StdIn1.scala
@@ -0,0 +1,10 @@
+import leon.io._
+
+object StdIn1 {
+
+  def alwaysPos: Int = {
+    implicit val state = StdIn.newState
+    StdIn.readInt
+  } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/StdIn2.scala b/src/test/resources/regression/verification/xlang/invalid/StdIn2.scala
new file mode 100644
index 000000000..f9a240212
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/StdIn2.scala
@@ -0,0 +1,13 @@
+import leon.io._
+
+object StdIn2 {
+
+  def anyTwoNumbers: Boolean = {
+    implicit val state = StdIn.newState
+    val n1 = StdIn.readInt
+    val n2 = StdIn.readInt
+
+    n1 == n2
+  } ensuring(res => res)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/StdIn3.scala b/src/test/resources/regression/verification/xlang/invalid/StdIn3.scala
new file mode 100644
index 000000000..9511b21fd
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/StdIn3.scala
@@ -0,0 +1,12 @@
+import leon.io._
+
+object StdIn3 {
+
+  //should be invalid because of MinInt
+  def abs: Int = {
+    implicit val state = StdIn.newState
+    val n = StdIn.readInt
+    if(n < 0) -n else n
+  } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/StdIn4.scala b/src/test/resources/regression/verification/xlang/invalid/StdIn4.scala
new file mode 100644
index 000000000..79c357b1d
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/StdIn4.scala
@@ -0,0 +1,10 @@
+import leon.io._
+
+object StdIn4 {
+
+  def readBoolCanBeFalse: Boolean = {
+    implicit val state = StdIn.newState
+    StdIn.readBoolean
+  } ensuring(res => res)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/StdIn1.scala b/src/test/resources/regression/verification/xlang/valid/StdIn1.scala
new file mode 100644
index 000000000..1fad9efd6
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/StdIn1.scala
@@ -0,0 +1,11 @@
+import leon.io._
+
+object StdIn1 {
+
+  def abs: BigInt = {
+    implicit val state = StdIn.newState
+    val n = StdIn.readBigInt
+    if(n < 0) -n else n
+  } ensuring(_ >= 0)
+
+}
-- 
GitLab