func()

in releases/go/encryption-sdk/Frames/Frames.go [332:396]

• 65 lines of code
• 9 McCabe index (conditional complexity)

func (_static *CompanionStruct_Default___) ReadFinalFrame(buffer m_SerializeFunctions.ReadableBuffer, header m_Header.HeaderInfo) m_Wrappers.Result {
	var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.ReadUInt32(buffer)
	_ = _0_valueOrError0
	if (_0_valueOrError0).IsFailure() {
		return (_0_valueOrError0).PropagateFailure()
	} else {
		var _1_finalFrameSignal m_SerializeFunctions.SuccessfulRead = (_0_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead)
		_ = _1_finalFrameSignal
		var _2_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((_1_finalFrameSignal).Dtor_data().(uint32)) == (Companion_Default___.ENDFRAME__SEQUENCE__NUMBER()), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Final frame sequence number MUST be the end-frame sequence number.")))
		_ = _2_valueOrError1
		if (_2_valueOrError1).IsFailure() {
			return (_2_valueOrError1).PropagateFailure()
		} else {
			var _3_valueOrError2 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.ReadUInt32((_1_finalFrameSignal).Dtor_tail())
			_ = _3_valueOrError2
			if (_3_valueOrError2).IsFailure() {
				return (_3_valueOrError2).PropagateFailure()
			} else {
				var _4_sequenceNumber m_SerializeFunctions.SuccessfulRead = (_3_valueOrError2).Extract().(m_SerializeFunctions.SuccessfulRead)
				_ = _4_sequenceNumber
				var _5_valueOrError3 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_4_sequenceNumber).Dtor_tail(), _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetIvLength((header).Dtor_suite())))
				_ = _5_valueOrError3
				if (_5_valueOrError3).IsFailure() {
					return (_5_valueOrError3).PropagateFailure()
				} else {
					var _6_iv m_SerializeFunctions.SuccessfulRead = (_5_valueOrError3).Extract().(m_SerializeFunctions.SuccessfulRead)
					_ = _6_iv
					var _7_valueOrError4 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.ReadUInt32((_6_iv).Dtor_tail())
					_ = _7_valueOrError4
					if (_7_valueOrError4).IsFailure() {
						return (_7_valueOrError4).PropagateFailure()
					} else {
						var _8_contentLength m_SerializeFunctions.SuccessfulRead = (_7_valueOrError4).Extract().(m_SerializeFunctions.SuccessfulRead)
						_ = _8_contentLength
						var _9_valueOrError5 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((_8_contentLength).Dtor_data().(uint32)) <= (((header).Dtor_body()).Dtor_frameLength()), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Content length MUST NOT exceed the frame length.")))
						_ = _9_valueOrError5
						if (_9_valueOrError5).IsFailure() {
							return (_9_valueOrError5).PropagateFailure()
						} else {
							var _10_valueOrError6 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.ReadUint32Seq((_6_iv).Dtor_tail())
							_ = _10_valueOrError6
							if (_10_valueOrError6).IsFailure() {
								return (_10_valueOrError6).PropagateFailure()
							} else {
								var _11_encContent m_SerializeFunctions.SuccessfulRead = (_10_valueOrError6).Extract().(m_SerializeFunctions.SuccessfulRead)
								_ = _11_encContent
								var _12_valueOrError7 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_11_encContent).Dtor_tail(), _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetTagLength((header).Dtor_suite())))
								_ = _12_valueOrError7
								if (_12_valueOrError7).IsFailure() {
									return (_12_valueOrError7).PropagateFailure()
								} else {
									var _13_authTag m_SerializeFunctions.SuccessfulRead = (_12_valueOrError7).Extract().(m_SerializeFunctions.SuccessfulRead)
									_ = _13_authTag
									var _14_finalFrame Frame = Companion_Frame_.Create_FinalFrame_(header, (_4_sequenceNumber).Dtor_data().(uint32), (_6_iv).Dtor_data().(_dafny.Sequence), (_11_encContent).Dtor_data().(_dafny.Sequence), (_13_authTag).Dtor_data().(_dafny.Sequence))
									_ = _14_finalFrame
									return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_(_14_finalFrame, (_13_authTag).Dtor_tail()))
								}
							}
						}
					}
				}
			}
		}
	}
}