func()

in releases/go/encryption-sdk/MessageBody/MessageBody.go [587:647]

• 61 lines of code
• 7 McCabe index (conditional complexity)

func (_static *CompanionStruct_Default___) ReadFramedMessageBody(buffer m_SerializeFunctions.ReadableBuffer, header m_Header.HeaderInfo, regularFrames _dafny.Sequence, continuation m_SerializeFunctions.ReadableBuffer) m_Wrappers.Result {
	goto TAIL_CALL_START
TAIL_CALL_START:
	var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.ReadUInt32(continuation)
	_ = _0_valueOrError0
	if (_0_valueOrError0).IsFailure() {
		return (_0_valueOrError0).PropagateFailure()
	} else {
		var _1_sequenceNumber m_SerializeFunctions.SuccessfulRead = (_0_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead)
		_ = _1_sequenceNumber
		if ((_1_sequenceNumber).Dtor_data().(uint32)) != (Companion_Default___.ENDFRAME__SEQUENCE__NUMBER()) /* dircomp */ {
			var _2_valueOrError1 m_Wrappers.Result = m_Frames.Companion_Default___.ReadRegularFrame(continuation, header)
			_ = _2_valueOrError1
			if (_2_valueOrError1).IsFailure() {
				return (_2_valueOrError1).PropagateFailure()
			} else {
				var _3_regularFrame m_SerializeFunctions.SuccessfulRead = (_2_valueOrError1).Extract().(m_SerializeFunctions.SuccessfulRead)
				_ = _3_regularFrame
				var _4_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32(((_3_regularFrame).Dtor_data().(m_Frames.Frame)).Dtor_seqNum())).Cmp((_dafny.IntOfUint32((regularFrames).Cardinality())).Plus(_dafny.One)) == 0, m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Sequence number out of order.")))
				_ = _4_valueOrError2
				if (_4_valueOrError2).IsFailure() {
					return (_4_valueOrError2).PropagateFailure()
				} else {
					var _5_nextRegularFrames _dafny.Sequence = _dafny.Companion_Sequence_.Concatenate(regularFrames, _dafny.SeqOf((_3_regularFrame).Dtor_data().(m_Frames.Frame)))
					_ = _5_nextRegularFrames
					var _in0 m_SerializeFunctions.ReadableBuffer = buffer
					_ = _in0
					var _in1 m_Header.HeaderInfo = header
					_ = _in1
					var _in2 _dafny.Sequence = _5_nextRegularFrames
					_ = _in2
					var _in3 m_SerializeFunctions.ReadableBuffer = (_3_regularFrame).Dtor_tail()
					_ = _in3
					buffer = _in0
					header = _in1
					regularFrames = _in2
					continuation = _in3
					goto TAIL_CALL_START
				}
			}
		} else {
			var _6_valueOrError3 m_Wrappers.Result = m_Frames.Companion_Default___.ReadFinalFrame(continuation, header)
			_ = _6_valueOrError3
			if (_6_valueOrError3).IsFailure() {
				return (_6_valueOrError3).PropagateFailure()
			} else {
				var _7_finalFrame m_SerializeFunctions.SuccessfulRead = (_6_valueOrError3).Extract().(m_SerializeFunctions.SuccessfulRead)
				_ = _7_finalFrame
				var _8_valueOrError4 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32(((_7_finalFrame).Dtor_data().(m_Frames.Frame)).Dtor_seqNum())).Cmp((_dafny.IntOfUint32((regularFrames).Cardinality())).Plus(_dafny.One)) == 0, m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Sequence number out of order.")))
				_ = _8_valueOrError4
				if (_8_valueOrError4).IsFailure() {
					return (_8_valueOrError4).PropagateFailure()
				} else {
					var _9_body FramedMessageBody = Companion_FramedMessageBody_.Create_FramedMessageBody_(regularFrames, (_7_finalFrame).Dtor_data().(m_Frames.Frame))
					_ = _9_body
					return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_(_9_body, (_7_finalFrame).Dtor_tail()))
				}
			}
		}
	}
}