Skip to content

Commit

Permalink
changed from ghost to pure - meth gets accessed from non ghost contex…
Browse files Browse the repository at this point in the history
…t in codec
  • Loading branch information
Filip Schramka committed Dec 4, 2023
1 parent 2497798 commit 975b79d
Showing 1 changed file with 6 additions and 4 deletions.
10 changes: 6 additions & 4 deletions asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala
Original file line number Diff line number Diff line change
Expand Up @@ -80,32 +80,34 @@ case class BitStream(
) { // all BisStream instances satisfy the following:
require(BitStream.invariant(currentBit, currentByte, buf.length))

@pure
private def remainingBits: Long = {
(buf.length.toLong * NO_OF_BITS_IN_BYTE) - (currentByte.toLong * NO_OF_BITS_IN_BYTE + currentBit)
}

@ghost
@pure
def validate_offset_bit(): Boolean = {
remainingBits >= 1
}.ensuring(_ => BitStream.invariant(this))

@ghost
@pure
def validate_offset_bits(bits: Long = 0): Boolean = {
require(bits >= 0)
remainingBits >= bits
}.ensuring(_ => BitStream.invariant(this))

@ghost
@pure
def validate_offset_byte(): Boolean = {
remainingBits >= NO_OF_BITS_IN_BYTE
}.ensuring(_ => BitStream.invariant(this))

@ghost
@pure
def validate_offset_bytes(bytes: Int): Boolean = {
require(bytes >= 0)
bytes <= remainingBits / NO_OF_BITS_IN_BYTE
}.ensuring(_ => BitStream.invariant(this))

@pure
def bitIndex(): Long = {
currentByte.toLong * 8 + currentBit.toLong
}.ensuring(res => 0 <= res && res <= 8 * buf.length.toLong &&& res == buf.length.toLong * 8 - remainingBits)
Expand Down

0 comments on commit 975b79d

Please sign in to comment.