io library using implicit state

library/io/StdIn.scala

+/* 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)
+
+}

src/test/resources/regression/verification/xlang/invalid/StdIn1.scala

+import leon.io._
+
+object StdIn1 {
+
+  def alwaysPos: Int = {
+    implicit val state = StdIn.newState
+    StdIn.readInt
+  } ensuring(_ >= 0)
+
+}

src/test/resources/regression/verification/xlang/invalid/StdIn2.scala

+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)
+
+}

src/test/resources/regression/verification/xlang/invalid/StdIn3.scala

+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)
+
+}

src/test/resources/regression/verification/xlang/invalid/StdIn4.scala

+import leon.io._
+
+object StdIn4 {
+
+  def readBoolCanBeFalse: Boolean = {
+    implicit val state = StdIn.newState
+    StdIn.readBoolean
+  } ensuring(res => res)
+
+}

src/test/resources/regression/verification/xlang/valid/StdIn1.scala

+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)
+
+}