renaming

esa · Aug 23, 2024 · ae41167 · ae41167
1 parent 4c2482d
commit ae41167
Show file tree

Hide file tree

Showing 5 changed files with 23 additions and 22 deletions.
diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm.scala
@@ -335,7 +335,7 @@ def GetCharIndex(ch: UByte, charSet: Array[UByte]): Int =
         i += 1
       ).invariant(i >= 0 &&& i <= charSet.length && ret < charSet.length && ret >= 0)
     ret
-} ensuring(res => charSet.length == 0 || res >= 0 && res < charSet.length)
+}.ensuring(res => charSet.length == 0 || res >= 0 && res < charSet.length)
 
 def NullType_Initialize(): NullType = {
     0

diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala
@@ -106,7 +106,7 @@ object BitStream {
       lemmaIsPrefixTransitive(r1, w1, w2)
       lemmaIsPrefixTransitive(r1, w2, r2)
       (r1, r2)
-   } ensuring(res =>
+   }.ensuring(res =>
       res._1.isPrefixOf(res._2)
       && res._1.isPrefixOf(w1)
       && res._2.isPrefixOf(w2)
@@ -840,7 +840,7 @@ case class BitStream private [asn1scala](
    def resetAt(b: BitStream): BitStream = {
       require(b.buf.length == buf.length)
       BitStream(snapshot(buf), b.currentByte, b.currentBit)
-   } ensuring(res => invariant(res))
+   }.ensuring(res => invariant(res))
 
    // ****************** Append Bit Functions **********************
 
@@ -1568,7 +1568,7 @@ case class BitStream private [asn1scala](
       else
          val bit = bitStreamSnap.readBit()
          Cons(bit, bitStreamReadBitsIntoList(bitStreamSnap, nBits - 1))
-   } ensuring( res => if(nBits == 0) then res.isEmpty else res.length > 0 ) // we'd like to prove res.length == nBits but it's not possible because of type mismatch
+   }.ensuring( res => if(nBits == 0) then res.isEmpty else res.length > 0 ) // we'd like to prove res.length == nBits but it's not possible because of type mismatch
 
    @ghost
    @opaque
@@ -1593,7 +1593,7 @@ case class BitStream private [asn1scala](
          val bitStream1Snap = snapshot(bitStream1)
          assert(bitStream1.readBitPure()._2 == listBits.head)
          ()
-   } ensuring(_ =>
+   }.ensuring(_ =>
       bitStreamReadBitsIntoList(bitStream2, nBits - 1) == listBits.tail
    )
 
@@ -1677,7 +1677,7 @@ case class BitStream private [asn1scala](
 
       if nBits > 0 then
          lemmaSameBitContentListThenbyteArrayBitContentSame(arr1, arr2, fromArr1 + 1, fromArr2 + 1, nBits - 1)
-   } ensuring(_ => byteArrayBitContentSame(arr1, arr2, fromArr1, fromArr2, nBits))
+   }.ensuring(_ => byteArrayBitContentSame(arr1, arr2, fromArr1, fromArr2, nBits))
 
 
 
@@ -2038,7 +2038,7 @@ case class BitStream private [asn1scala](
       val arr: Array[Byte] = Array.fill(arrLen)(0 : Byte)
       readBitsLoop(nBits, arr, 0, nBits)
       UByte.fromArrayRaws(arr)
-   } ensuring(res =>
+   }.ensuring(res =>
       buf == old(this).buf
       &&& BitStream.bitIndex(old(this).buf.length, old(this).currentByte, old(this).currentBit) + nBits == BitStream.bitIndex(this.buf.length, this.currentByte, this.currentBit)
       &&& BitStream.invariant(this.currentBit, this.currentByte, this.buf.length)
@@ -2106,7 +2106,7 @@ case class BitStream private [asn1scala](
       require(BitStream.validate_offset_bits(buf.length.toLong, currentByte.toLong, currentBit.toLong, nBits))
       val arr = readBits(nBits)
       Vector.fromScala(arr.toVector)
-   } ensuring(res =>
+   }.ensuring(res =>
       buf == old(this).buf && BitStream.bitIndex(old(this).buf.length, old(this).currentByte, old(this).currentBit) + nBits == BitStream.bitIndex(this.buf.length, this.currentByte, this.currentBit) &&
       BitStream.invariant(this.currentBit, this.currentByte, this.buf.length) &&
       res.length == ((nBits + NO_OF_BITS_IN_BYTE - 1) / NO_OF_BITS_IN_BYTE).toInt

diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala
@@ -419,7 +419,7 @@ case class Codec(bitStream: BitStream) {
             min
          else
             res
-   } ensuring( res =>
+   }.ensuring( res =>
       buf == old(this).buf &&
       res >= min && res <= max &&
       BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length) &&
@@ -1348,7 +1348,7 @@ case class Codec(bitStream: BitStream) {
          ghostExpr(check(nCurOffset1 >= 0 ))
          ghostExpr(check(nRemainingItemsVar1 <= 0x4000 ))
          (nRemainingItemsVar1, nCurOffset1)
-   } ensuring(res =>
+   }.ensuring(res =>
          BitStream.bitIndex(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit ) <= bitIndex + (nRemainingItemsVar1 / 0x4000) * 8 + nRemainingItemsVar1 * 8 - res._1 * 8 &&
          BitStream.validate_offset_bytes(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, res._1 + 2) &&
          BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length) &&
@@ -1397,7 +1397,7 @@ case class Codec(bitStream: BitStream) {
          assert(bitIndexAfterRecursive == bitIndexBeforeRecursive  + (to - from - 1) * NO_OF_BITS_IN_BYTE)
          assert(NO_OF_BITS_IN_BYTE + (to - from - 1) * NO_OF_BITS_IN_BYTE == (to - from) * NO_OF_BITS_IN_BYTE)
          assert(bitIndexAfterRecursive == bitIndexBeforeAppending + NO_OF_BITS_IN_BYTE + (to - from - 1) * NO_OF_BITS_IN_BYTE)
-   } ensuring(_ =>
+   }.ensuring(_ =>
       val oldBitStream = old(this).bitStream
       BitStream.bitIndex(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit ) == bitIndex + (to - from) * NO_OF_BITS_IN_BYTE &&
       oldBitStream.buf.length == bitStream.buf.length
@@ -1409,14 +1409,14 @@ case class Codec(bitStream: BitStream) {
    @inlineOnce
    def lemmaGetBitCountUnsignedFFEqualsEight(): Unit = {
 
-   } ensuring(_ => GetBitCountUnsigned(stainless.math.wrapping(0xFF).toRawULong) == 8)
+   }.ensuring(_ => GetBitCountUnsigned(stainless.math.wrapping(0xFF).toRawULong) == 8)
 
    @ghost
    @opaque
    @inlineOnce
    def lemmaGetBitCountUnsigned7FFFEquals15(): Unit = {
 
-   } ensuring(_ => GetBitCountUnsigned(stainless.math.wrapping(0x7FFF).toRawULong) == 15)
+   }.ensuring(_ => GetBitCountUnsigned(stainless.math.wrapping(0x7FFF).toRawULong) == 15)
 
    @ghost
    @opaque
@@ -1429,7 +1429,7 @@ case class Codec(bitStream: BitStream) {
       require(offsetBits == offsetBytes * 8)
       require(BitStream.validate_offset_bits(bufLength, currentByte, currentBit, offsetBits))
 
-   } ensuring(_ => BitStream.validate_offset_bytes(bufLength, currentByte, currentBit, offsetBytes))
+   }.ensuring(_ => BitStream.validate_offset_bytes(bufLength, currentByte, currentBit, offsetBytes))
    /**
      * Takes more than 100sec to verify, that's why it is extracted to a lemma, even though it does not need a specific proof
      *
@@ -1463,7 +1463,7 @@ case class Codec(bitStream: BitStream) {
          require(bitIndex2 - bitIndex1 <= offset1Bits - offset2Bits)
          require(BitStream.validate_offset_bits(bufLength, currentByte1, currentBit1, offset1Bits))
 
-      } ensuring(_ => BitStream.validate_offset_bits(bufLength, currentByte2, currentBit2, offset2Bits))
+      }.ensuring(_ => BitStream.validate_offset_bits(bufLength, currentByte2, currentBit2, offset2Bits))
 
 
       /**
@@ -1550,7 +1550,7 @@ case class Codec(bitStream: BitStream) {
       val newArr: Array[UByte] = Array.fill(nLengthTmp1.toInt)(0.toRawUByte)
       arrayCopyOffsetLen(arr, newArr, 0, 0, newArr.length)
       newArr
-   } ensuring(_ => BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length))
+   }.ensuring(_ => BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length))
 
 
    /**
@@ -1654,7 +1654,7 @@ case class Codec(bitStream: BitStream) {
       assert(arr.length == asn1SizeMax.toInt)
       decodeOctetString_fragmentation_innerWhile(arr, asn1SizeMax, newNCurOffset1)
 
-   } ensuring(res =>
+   }.ensuring(res =>
       (res._2 >= 0 && res._2 <= asn1SizeMax || res == (-1L, -1L)) &&
       BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length) &&
       old(this).bitStream.buf.length == bitStream.buf.length &&
@@ -1701,7 +1701,7 @@ case class Codec(bitStream: BitStream) {
       decodeOctetString_fragmentation_innerMostWhile(arr, asn1SizeMax, from + 1, to)
       ()
 
-   } ensuring(_ =>
+   }.ensuring(_ =>
       old(this).buf.length == bitStream.buf.length &&
       arr.length == asn1SizeMax.toInt &&
       BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length) &&
@@ -1887,7 +1887,7 @@ case class Codec(bitStream: BitStream) {
          assert(BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, newRemaingItems + 8*(newRemaingItems / 0x4000) + 16))
 
          encodeBitString_while(arr, nCount, asn1SizeMin, asn1SizeMax, newRemaingItems, newOffset, newBitIndex)
-   } ensuring (res =>
+   }.ensuring (res =>
       BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length) &&
       // BitStream.bitIndex(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit ) <= bitIndex + (nRemainingItemsVar1 / 0x4000) * 8 + nRemainingItemsVar1 - res._1 &&
       BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, res._1 + 16) &&
@@ -2062,7 +2062,7 @@ case class Codec(bitStream: BitStream) {
          return (-1L, -1L)
       decodeBitString_while(asn1SizeMin, asn1SizeMax, newNCurOffset1, arr)
 
-   } ensuring (res =>
+   }.ensuring (res =>
       res == (-1L, -1L)
       ||
       res._1 >= 0 && res._1 <= 0xFF &&

diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Verification.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Verification.scala
@@ -33,14 +33,14 @@ def arrayCopyOffset[T](@pure src: Array[T], dst: Array[T], fromSrc: Int, toSrc:
     dst(fromDst) = src(fromSrc)
     arrayCopyOffset(src, dst, fromSrc + 1, toSrc, fromDst + 1)
   }
-} ensuring ( _ => old(dst).length == dst.length)
+}.ensuring ( _ => old(dst).length == dst.length)
 
 def arrayCopyOffsetLen[T](@pure src: Array[T], dst: Array[T], fromSrc: Int, fromDst: Int, len: Int): Unit = {
   require(0 <= len && len <= src.length && len <= dst.length)
   require(0 <= fromSrc && fromSrc <= src.length - len)
   require(0 <= fromDst && fromDst <= dst.length - len)
   arrayCopyOffset(src, dst, fromSrc, fromSrc + len, fromDst)
-} ensuring ( _ => old(dst).length == dst.length)
+}.ensuring ( _ => old(dst).length == dst.length)
 
 @pure
 def arrayBitIndices(fromBit: Long, toBit: Long): (Int, Int, Int, Int) = {

diff --git a/asn1scala/verify_bitStream.sh b/asn1scala/verify_bitStream.sh
@@ -3,6 +3,7 @@ src/main/scala/asn1scala/asn1jvm.scala  \
 src/main/scala/asn1scala/asn1jvm_Verification.scala  \
 src/main/scala/asn1scala/asn1jvm_Helper.scala \
 src/main/scala/asn1scala/asn1jvm_Bitstream.scala \
+src/main/scala/asn1scala/asn1jvm_Vector.scala \
 --config-file=stainless.conf \
 -D-parallel=5 \
 $1