removed unused real enc / dec

fixed F# errors (only with latest VS - were warning before)
verfied some stuff

BackendAst/DAstACN.fs

@@ -149,13 +149,16 @@ let handleAlignemntForAsn1Types (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (code
     | Some al   -> 
         let alStr, nAligmVal = 
             match al with
-            | AcnGenericTypes.NextByte   -> match ST.lang with
+            | AcnGenericTypes.NextByte -> 
+                match ST.lang with
                 | Scala -> "Byte", 8I
                 | _ -> "NextByte", 8I
-            | AcnGenericTypes.NextWord   -> match ST.lang with
+            | AcnGenericTypes.NextWord -> 
+                match ST.lang with
                 | Scala -> "Short", 16I
                 | _ -> "NextWord", 16I
-            | AcnGenericTypes.NextDWord   -> match ST.lang with
+            | AcnGenericTypes.NextDWord -> 
+                match ST.lang with
                 | Scala -> "Int", 32I
                 | _ -> "NextDWord", 32I
         let newFuncBody st errCode prms p =

asn1scala/src/main/scala/asn1scala/asn1jvm.scala

@@ -33,6 +33,8 @@ val NO_OF_BITS_IN_LONG = 64
 val NO_OF_BYTES_IN_JVM_SHORT = 2
 val NO_OF_BYTES_IN_JVM_INT = 4
 val NO_OF_BYTES_IN_JVM_LONG = 8
+val NO_OF_BYTES_IN_JVM_FLOAT = 4
+val NO_OF_BYTES_IN_JVM_DOUBLE = 8
 val OBJECT_IDENTIFIER_MAX_LENGTH = 20
 
 val NOT_INITIALIZED_ERR_CODE = 1337

asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala

@@ -556,7 +556,7 @@ case class BitStream(
     *
     */
    def readPartialByte(nBits: Int): UByte = {
-      require(nBits >= 0 && nBits < NO_OF_BITS_IN_BYTE)
+      require(nBits >= 0 && nBits <= NO_OF_BITS_IN_BYTE)
       require(validate_offset_bits(nBits))
 
       @ghost val oldThis = snapshot(this)

asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala

@@ -57,7 +57,6 @@ def BitString_equal(arr1: Array[UByte], arr2: Array[UByte]): Boolean = {
  *
  * @param count represents the number of bytes in the internal buffer
  */
-@mutable
 trait Codec {
 
    def bitStream: BitStream
@@ -177,17 +176,17 @@ trait Codec {
       //    return decodeNonNegativeInteger32Neg(v, nBits)
    }
 
-   def encodeNonNegativeIntegerNeg(v: ULong, negate: Boolean): Unit = {
+   def encodeNonNegativeIntegerNeg(v: ULong): Unit = {
       if v >>> 32 == 0 then
-         encodeNonNegativeInteger32Neg(v.toInt, negate)
+         encodeNonNegativeInteger32Neg(v.toInt, true)
       else
          // TODO: Check Int/Long
          val hi = (v >>> 32).toInt
          var lo = v.toInt
-         encodeNonNegativeInteger32Neg(hi, negate)
+         encodeNonNegativeInteger32Neg(hi, true)
 
          /*bug !!!!*/
-         if negate then
+         if true then // TODO, the negate flag was always true
             lo = ~lo
          val nBits = GetNumberOfBitsForNonNegativeInteger(lo.toLong)
          appendNBitZero(32 - nBits)
@@ -379,7 +378,7 @@ trait Codec {
          encodeNonNegativeInteger(v)
       else
          appendNBitOne(nBytes * 8 - GetNumberOfBitsForNonNegativeInteger((-v - 1)))
-         encodeNonNegativeIntegerNeg((-v - 1), true)
+         encodeNonNegativeIntegerNeg((-v - 1))
    }
 
 
@@ -1064,13 +1063,15 @@ trait Codec {
       isValidPrecondition
    }
 
-   def readPartialByte(nbits: UByte): Option[UByte] = {
-      val isValidPrecondition = bitStream.validate_offset_bits(nbits)
+   def readPartialByte(nBits: Int): Option[UByte] = {
+      require(nBits >= 0 && nBits <= NO_OF_BITS_IN_BYTE)
+
+      val isValidPrecondition = bitStream.validate_offset_bits(nBits)
       stainlessAssert(isValidPrecondition)
       assert(isValidPrecondition)
 
       isValidPrecondition match
-         case true => Some(bitStream.readPartialByte(nbits))
+         case true => Some(bitStream.readPartialByte(nBits))
          case false => None()
    }
 

asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala

@@ -1,7 +1,7 @@
 package asn1scala
 
 import stainless.lang.StaticChecks.assert
-import stainless.lang.{None, Option, Some}
+import stainless.lang.{None => None, ghost => ghostExpr, Option => Option, _}
 
 val FAILED_READ_ERR_CODE = 5400
 
@@ -203,7 +203,7 @@ case class ACN(bitStream: BitStream) extends Codec {
 
       else
          appendNBitOne(encodedSizeInBits - GetNumberOfBitsForNonNegativeInteger(-intVal - 1))
-         encodeNonNegativeIntegerNeg(-intVal - 1, true)
+         encodeNonNegativeIntegerNeg(-intVal - 1)
    }
 
 
@@ -691,118 +691,108 @@ case class ACN(bitStream: BitStream) extends Codec {
       Right(0)
    }
 
-
-   /*Real encoding functions*/
+   /* Real encoding functions */
    def enc_Real_IEEE754_32_big_endian(realValue: Float): Unit = {
-      val b: Array[Byte] = java.nio.ByteBuffer.allocate(4).putFloat(realValue).array
+      val b: Array[Byte] = java.nio.ByteBuffer.allocate(NO_OF_BYTES_IN_JVM_FLOAT).putFloat(realValue).array
 
       var i: Int = 0
-      while i < 4 do
+      while i < NO_OF_BYTES_IN_JVM_FLOAT do
          appendByte(b(i))
          i += 1
    }
 
-   def dec_Real_IEEE754_32_big_endian(): Option[Double] = {
-      val b: Array[Byte] = Array.fill(4)(0)
-      var i: Int = 0
-      while i < 4 do
-         readByte() match
-            case None() => return None()
-            case Some(ub) => b(i) = ub
-         i += 1
+   def enc_Real_IEEE754_32_little_endian(realValue: Float): Unit = {
+      val b: Array[Byte] = java.nio.ByteBuffer.allocate(NO_OF_BYTES_IN_JVM_FLOAT).putFloat(realValue).array
 
-      val dat1 = BigInt(b).toInt
-      Some(java.lang.Float.intBitsToFloat(dat1).toDouble)
+      var i: Int = NO_OF_BYTES_IN_JVM_FLOAT - 1
+      while i >= 0 do
+         appendByte(b(i))
+         i -= 1
    }
 
-   def dec_Real_IEEE754_32_big_endian_fp32(): Option[Float] = {
-      val b: Array[Byte] = Array.fill(4)(0)
+   def enc_Real_IEEE754_64_big_endian(realValue: Double): Unit = {
+      val b: Array[Byte] = java.nio.ByteBuffer.allocate(NO_OF_BYTES_IN_JVM_DOUBLE).putDouble(realValue).array
+
       var i: Int = 0
-      while i < 4 do
-         readByte() match
-            case None() => return None()
-            case Some(ub) => b(i) = ub
+      while i < NO_OF_BYTES_IN_JVM_DOUBLE do
+         appendByte(b(i))
          i += 1
-
-      val dat1 = BigInt(b).toInt
-      Some(java.lang.Float.intBitsToFloat(dat1))
    }
 
+   def enc_Real_IEEE754_64_little_endian(realValue: Double): Unit = {
+      val b: Array[Byte] = java.nio.ByteBuffer.allocate(NO_OF_BYTES_IN_JVM_DOUBLE).putDouble(realValue).array
 
-   def enc_Real_IEEE754_64_big_endian(realValue: Double): Unit = {
-      val b: Array[Byte] = java.nio.ByteBuffer.allocate(8).putDouble(realValue).array
-
-      var i: Int = 0
-      while i < 8 do
+      var i: Int = NO_OF_BYTES_IN_JVM_DOUBLE - 1
+      while i >= 0 do
          appendByte(b(i))
-         i += 1
+         i -= 1
    }
 
-   def dec_Real_IEEE754_64_big_endian(): Option[Double] = {
-      val b: Array[Byte] = Array.fill(8)(0)
-      var i: Int = 0
-      while i < 8 do
+   /* Real decoding functions */
+   def dec_Real_IEEE754_32_big_endian(): Option[Float] = {
+      var ret: Int = 0
+      var i: Int = 1
+
+      assert(NO_OF_BYTES_IN_JVM_INT == NO_OF_BYTES_IN_JVM_FLOAT)
+
+      while i <= NO_OF_BYTES_IN_JVM_INT do
          readByte() match
             case None() => return None()
-            case Some(ub) => b(i) = ub
+            case Some(b) =>
+               ret |= b.unsignedToInt << (NO_OF_BYTES_IN_JVM_INT - i) * NO_OF_BITS_IN_BYTE
          i += 1
 
-      val dat1 = BigInt(b).toLong
-      Some(java.lang.Double.longBitsToDouble(dat1))
+      Some(java.lang.Float.intBitsToFloat(ret))
    }
 
+   def dec_Real_IEEE754_32_little_endian(): Option[Float] = {
+      var ret: Int = 0
+      var i: Int = 0
 
-   def enc_Real_IEEE754_32_little_endian(realValue: Double): Unit = {
-      val b: Array[Byte] = java.nio.ByteBuffer.allocate(4).putFloat(realValue.toFloat).array
+      assert(NO_OF_BYTES_IN_JVM_INT == NO_OF_BYTES_IN_JVM_FLOAT)
 
-      var i: Int = 3
-      while i >= 0 do
-         appendByte(b(i))
-         i -= 1
-   }
+      while i < NO_OF_BYTES_IN_JVM_INT do
+         readByte() match
+            case None() => return None()
+            case Some(b) =>
+               ret |= b.unsignedToInt << i * NO_OF_BITS_IN_BYTE
+         i += 1
 
-   def dec_Real_IEEE754_32_little_endian(): Option[Double] = {
-      dec_Real_IEEE754_32_little_endian_fp32() match
-         case None() => None()
-         case Some(f) => Some(f.toDouble)
+      Some(java.lang.Float.intBitsToFloat(ret))
    }
 
-   def dec_Real_IEEE754_32_little_endian_fp32(): Option[Float] = {
-      val b: Array[Byte] = Array.fill(4)(0)
-      var i: Int = 3
-      while i >= 0 do
+   def dec_Real_IEEE754_64_big_endian(): Option[Double] = {
+      var ret: Long = 0
+      var i: Int = 1
+
+      assert(NO_OF_BYTES_IN_JVM_LONG == NO_OF_BYTES_IN_JVM_DOUBLE)
+
+      while i <= NO_OF_BYTES_IN_JVM_LONG do
          readByte() match
             case None() => return None()
-            case Some(ub) => b(i) = ub
-               i -= 1
+            case Some(b) =>
+               ret |= b.unsignedToLong << (NO_OF_BYTES_IN_JVM_LONG - i) * NO_OF_BITS_IN_BYTE
+         i += 1
 
-      val dat1 = BigInt(b).toInt
-      Some(java.lang.Float.intBitsToFloat(dat1))
+      Some(java.lang.Double.longBitsToDouble(ret))
    }
 
-   def enc_Real_IEEE754_64_little_endian(realValue: Double): Unit = {
-      val b: Array[Byte] = java.nio.ByteBuffer.allocate(8).putDouble(realValue).array
+   def dec_Real_IEEE754_64_little_endian(): Option[Double] = {
+      var ret: Long = 0
+      var i: Int = 0
 
-      var i: Int = 7
-      while i >= 0 do
-         appendByte(b(i))
-         i -= 1
-   }
+      assert(NO_OF_BYTES_IN_JVM_LONG == NO_OF_BYTES_IN_JVM_DOUBLE)
 
-   def dec_Real_IEEE754_64_little_endian(): Option[Double] = {
-      val b: Array[Byte] = Array.fill(8)(0)
-      var i: Int = 7
-      while i >= 0 do
+      while i < NO_OF_BYTES_IN_JVM_LONG do
          readByte() match
             case None() => return None()
-            case Some(ub) => b(i) = ub
-               i -= 1
+            case Some(b) =>
+               ret |= b.unsignedToLong << i * NO_OF_BITS_IN_BYTE
+         i += 1
 
-      val dat1 = BigInt(b).toLong
-      Some(java.lang.Double.longBitsToDouble(dat1))
+      Some(java.lang.Double.longBitsToDouble(ret))
    }
 
-
    /* String functions*/
    def enc_String_Ascii_FixSize(max: Long, strVal: Array[ASCIIChar]): Unit = {
       var i: Long = 0

asn1scala/src/main/scala/asn1scala/asn1jvm_Helper.scala

@@ -27,7 +27,7 @@ val MASK_POS_INT    = 0x7F_FF_FF_FFL
 * Meths to upcast unsigned integer data types on the JVM
 */
 extension (ubL: UByte) {
-   def unsignedToLong: Long = ubL & MASK_BYTE_L
+   def unsignedToLong: Long = ubL.toLong & MASK_BYTE_L
    def unsignedToInt: Int = ubL.toInt & MASK_BYTE
 
    @targetName("unsigned right shift on Bytes")