Add opaque types for Double and Float

frontends/benchmarks/verification/valid/FPFledging.scala

@@ -0,0 +1,21 @@
+import stainless.math._
+
+object FPFledging {
+ def test1(x: Double): Unit = {
+ assert(Double.longBitsToDouble(Double.doubleToRawLongBits(x)) == x)
+ }
+
+ def test2(x: Long): Unit = {
+ Double.longBitsToDoublePost(x)
+ assert(Double.doubleToRawLongBits(Double.longBitsToDouble(x)) == x)
+ }
+
+ def test3(x: Float): Unit = {
+ assert(Float.intBitsToFloat(Float.floatToRawIntBits(x)) == x)
+ }
+
+ def test4(x: Int): Unit = {
+ Float.intBitsToFloatPost(x)
+ assert(Float.floatToRawIntBits(Float.intBitsToFloat(x)) == x)
+ }
+}

frontends/library/stainless/math/Double.scala

@@ -0,0 +1,26 @@
+package stainless
+package math
+
+import lang.StaticChecks._
+import annotation._
+
+@library
+case class Double(@extern @pure private val value: scala.Double) extends AnyVal
+
+@library
+object Double {
+ @extern @pure
+ def longBitsToDouble(l: Long): Double = {
+ Double(java.lang.Double.longBitsToDouble(l))
+ }
+
+ @extern @pure
+ def longBitsToDoublePost(l: Long): Unit = {
+ ()
+ } ensuring (_ => doubleToRawLongBits(longBitsToDouble(l)) == l)
+
+ @extern @pure
+ def doubleToRawLongBits(d: Double): Long = {
+ java.lang.Double.doubleToRawLongBits(d.value)
+ } ensuring (res => longBitsToDouble(res) == d)
+}

frontends/library/stainless/math/Float.scala

@@ -0,0 +1,26 @@
+package stainless
+package math
+
+import lang.StaticChecks._
+import annotation._
+
+@library
+case class Float(@extern @pure private val value: scala.Float) extends AnyVal
+
+@library
+object Float {
+ @extern @pure
+ def intBitsToFloat(i: Int): Float = {
+ Float(java.lang.Float.intBitsToFloat(i))
+ }
+
+ @extern @pure
+ def intBitsToFloatPost(i: Int): Unit = {
+ ()
+ } ensuring (_ => floatToRawIntBits(intBitsToFloat(i)) == i)
+
+ @extern @pure
+ def floatToRawIntBits(d: Float): Int = {
+ java.lang.Float.floatToRawIntBits(d.value)
+ } ensuring (res => intBitsToFloat(res) == d)
+}

libfiles.txt

@@ -20,6 +20,8 @@ stainless/covcollection/Option.scala
 stainless/equations/package.scala
 stainless/math/BitVectors.scala
 stainless/math/Nat.scala
+stainless/math/Float.scala
+stainless/math/Double.scala
 stainless/math/package.scala
 stainless/io/FileOutputStream.scala
 stainless/io/StdOut.scala