func()

in releases/go/encryption-sdk/MessageBody/MessageBody.go [527:563]

• 37 lines of code
• 3 McCabe index (conditional complexity)

func (_static *CompanionStruct_Default___) BodyAADByFrameType(frame m_Frames.Frame) _dafny.Sequence {
	var _let_tmp_rhs0 _dafny.Tuple = func() _dafny.Tuple {
		var _source0 m_Frames.Frame = frame
		_ = _source0
		{
			if _source0.Is_RegularFrame() {
				var _0_header m_Header.HeaderInfo = _source0.Get_().(m_Frames.Frame_RegularFrame).Header
				_ = _0_header
				var _1_seqNum uint32 = _source0.Get_().(m_Frames.Frame_RegularFrame).SeqNum
				_ = _1_seqNum
				return _dafny.TupleOf(_1_seqNum, Companion_BodyAADContent_.Create_AADRegularFrame_(), uint64(((_0_header).Dtor_body()).Dtor_frameLength()))
			}
		}
		{
			if _source0.Is_FinalFrame() {
				var _2_seqNum uint32 = _source0.Get_().(m_Frames.Frame_FinalFrame).SeqNum
				_ = _2_seqNum
				var _3_encContent _dafny.Sequence = _source0.Get_().(m_Frames.Frame_FinalFrame).EncContent
				_ = _3_encContent
				return _dafny.TupleOf(_2_seqNum, Companion_BodyAADContent_.Create_AADFinalFrame_(), uint64((_3_encContent).Cardinality()))
			}
		}
		{
			var _4_encContent _dafny.Sequence = _source0.Get_().(m_Frames.Frame_NonFramed).EncContent
			_ = _4_encContent
			return _dafny.TupleOf(Companion_Default___.NONFRAMED__SEQUENCE__NUMBER(), Companion_BodyAADContent_.Create_AADSingleBlock_(), uint64((_4_encContent).Cardinality()))
		}
	}()
	_ = _let_tmp_rhs0
	var _5_sequenceNumber uint32 = (*(_let_tmp_rhs0).IndexInt(0)).(uint32)
	_ = _5_sequenceNumber
	var _6_bc BodyAADContent = (*(_let_tmp_rhs0).IndexInt(1)).(BodyAADContent)
	_ = _6_bc
	var _7_length uint64 = (*(_let_tmp_rhs0).IndexInt(2)).(uint64)
	_ = _7_length
	return Companion_Default___.BodyAAD((((frame).Dtor_header()).Dtor_body()).Dtor_messageId(), _6_bc, _5_sequenceNumber, _7_length)
}