func()

in releases/go/encryption-sdk/MessageBody/MessageBody.go [312:371]

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

func (_static *CompanionStruct_Default___) EncryptMessageBody(plaintext _dafny.Sequence, header m_Header.HeaderInfo, key _dafny.Sequence, crypto *m_AtomicPrimitives.AtomicPrimitivesClient) m_Wrappers.Result {
	var result m_Wrappers.Result = m_Wrappers.Result{}
	_ = result
	var _0_n _dafny.Int
	_ = _0_n
	var _1_sequenceNumber uint32
	_ = _1_sequenceNumber
	var _rhs0 _dafny.Int = _dafny.Zero
	_ = _rhs0
	var _rhs1 uint32 = Companion_Default___.START__SEQUENCE__NUMBER()
	_ = _rhs1
	_0_n = _rhs0
	_1_sequenceNumber = _rhs1
	var _2_regularFrames _dafny.Sequence
	_ = _2_regularFrames
	_2_regularFrames = _dafny.SeqOf()
	for ((_0_n).Plus(_dafny.IntOfUint32(((header).Dtor_body()).Dtor_frameLength()))).Cmp(_dafny.IntOfUint32((plaintext).Cardinality())) < 0 {
		var _3_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
		_ = _3_valueOrError0
		_3_valueOrError0 = m_Wrappers.Companion_Default___.Need((_1_sequenceNumber) < (Companion_Default___.ENDFRAME__SEQUENCE__NUMBER()), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("too many frames")))
		if (_3_valueOrError0).IsFailure() {
			result = (_3_valueOrError0).PropagateFailure()
			return result
		}
		var _4_plaintextFrame _dafny.Sequence
		_ = _4_plaintextFrame
		_4_plaintextFrame = (plaintext).Subsequence((_0_n).Uint32(), ((_0_n).Plus(_dafny.IntOfUint32(((header).Dtor_body()).Dtor_frameLength()))).Uint32())
		var _5_valueOrError1 m_Wrappers.Result = m_Wrappers.Result{}
		_ = _5_valueOrError1
		var _out0 m_Wrappers.Result
		_ = _out0
		_out0 = Companion_Default___.EncryptRegularFrame(key, header, _4_plaintextFrame, _1_sequenceNumber, crypto)
		_5_valueOrError1 = _out0
		if (_5_valueOrError1).IsFailure() {
			result = (_5_valueOrError1).PropagateFailure()
			return result
		}
		var _6_regularFrame m_Frames.Frame
		_ = _6_regularFrame
		_6_regularFrame = (_5_valueOrError1).Extract().(m_Frames.Frame)
		_2_regularFrames = _dafny.Companion_Sequence_.Concatenate(_2_regularFrames, _dafny.SeqOf(_6_regularFrame))
		_0_n = (_0_n).Plus(_dafny.IntOfUint32(((header).Dtor_body()).Dtor_frameLength()))
		_1_sequenceNumber = (_1_sequenceNumber) + (uint32(1))
	}
	var _7_valueOrError2 m_Wrappers.Result = m_Wrappers.Result{}
	_ = _7_valueOrError2
	var _out1 m_Wrappers.Result
	_ = _out1
	_out1 = Companion_Default___.EncryptFinalFrame(key, header, (plaintext).Drop((_0_n).Uint32()), _1_sequenceNumber, crypto)
	_7_valueOrError2 = _out1
	if (_7_valueOrError2).IsFailure() {
		result = (_7_valueOrError2).PropagateFailure()
		return result
	}
	var _8_finalFrame m_Frames.Frame
	_ = _8_finalFrame
	_8_finalFrame = (_7_valueOrError2).Extract().(m_Frames.Frame)
	result = m_Wrappers.Companion_Result_.Create_Success_(Companion_FramedMessageBody_.Create_FramedMessageBody_(_2_regularFrames, _8_finalFrame))
	return result
}