func()

in releases/go/encryption-sdk/EncryptionContext/EncryptionContext.go [367:418]

• 52 lines of code
• 5 McCabe index (conditional complexity)

func (_static *CompanionStruct_Default___) ReadAADPairs(buffer m_SerializeFunctions.ReadableBuffer, accumulator _dafny.Sequence, keys _dafny.Set, count uint16, nextPair m_SerializeFunctions.ReadableBuffer) m_Wrappers.Result {
	goto TAIL_CALL_START
TAIL_CALL_START:
	if (_dafny.IntOfUint16(count)).Cmp(_dafny.IntOfUint32((accumulator).Cardinality())) > 0 {
		var _0_valueOrError0 m_Wrappers.Result = Companion_Default___.ReadAADPair(nextPair)
		_ = _0_valueOrError0
		if (_0_valueOrError0).IsFailure() {
			return (_0_valueOrError0).PropagateFailure()
		} else {
			var _let_tmp_rhs0 m_SerializeFunctions.SuccessfulRead = (_0_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead)
			_ = _let_tmp_rhs0
			var _1_pair m_SerializableTypes.Pair = _let_tmp_rhs0.Get_().(m_SerializeFunctions.SuccessfulRead_SuccessfulRead).Data.(m_SerializableTypes.Pair)
			_ = _1_pair
			var _2_newPos m_SerializeFunctions.ReadableBuffer = _let_tmp_rhs0.Get_().(m_SerializeFunctions.SuccessfulRead_SuccessfulRead).Tail
			_ = _2_newPos
			var _3_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(!(keys).Contains((_1_pair).Dtor_key().(_dafny.Sequence)), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Duplicate Encryption Context key value.")))
			_ = _3_valueOrError1
			if (_3_valueOrError1).IsFailure() {
				return (_3_valueOrError1).PropagateFailure()
			} else {
				var _4_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((((_2_newPos).Dtor_start()).Minus((buffer).Dtor_start())).Cmp(m_SerializableTypes.Companion_Default___.ESDK__CANONICAL__ENCRYPTION__CONTEXT__MAX__LENGTH()) < 0, m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Encryption Context exceeds maximum length.")))
				_ = _4_valueOrError2
				if (_4_valueOrError2).IsFailure() {
					return (_4_valueOrError2).PropagateFailure()
				} else {
					var _5_nextAcc _dafny.Sequence = _dafny.Companion_Sequence_.Concatenate(accumulator, _dafny.SeqOf(_1_pair))
					_ = _5_nextAcc
					var _6_nextKeys _dafny.Set = (keys).Union(Companion_Default___.KeysToSet(_dafny.SeqOf(_1_pair)))
					_ = _6_nextKeys
					var _in0 m_SerializeFunctions.ReadableBuffer = buffer
					_ = _in0
					var _in1 _dafny.Sequence = _5_nextAcc
					_ = _in1
					var _in2 _dafny.Set = _6_nextKeys
					_ = _in2
					var _in3 uint16 = count
					_ = _in3
					var _in4 m_SerializeFunctions.ReadableBuffer = _2_newPos
					_ = _in4
					buffer = _in0
					accumulator = _in1
					keys = _in2
					count = _in3
					nextPair = _in4
					goto TAIL_CALL_START
				}
			}
		}
	} else {
		return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_(accumulator, nextPair))
	}
}