func()

in releases/go/encryption-sdk/Frames/Frames.go [397:439]
43 lines of code
6 McCabe index (conditional complexity)

func (_static *CompanionStruct_Default___) ReadNonFrame(buffer m_SerializeFunctions.ReadableBuffer, header m_Header.HeaderInfo) m_Wrappers.Result {
	var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetIvLength((header).Dtor_suite())))
	_ = _0_valueOrError0
	if (_0_valueOrError0).IsFailure() {
		return (_0_valueOrError0).PropagateFailure()
	} else {
		var _1_iv m_SerializeFunctions.SuccessfulRead = (_0_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead)
		_ = _1_iv
		var _2_valueOrError1 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.ReadUInt64((_1_iv).Dtor_tail())
		_ = _2_valueOrError1
		if (_2_valueOrError1).IsFailure() {
			return (_2_valueOrError1).PropagateFailure()
		} else {
			var _3_contentLength m_SerializeFunctions.SuccessfulRead = (_2_valueOrError1).Extract().(m_SerializeFunctions.SuccessfulRead)
			_ = _3_contentLength
			var _4_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint64((_3_contentLength).Dtor_data().(uint64))).Cmp(Companion_Default___.SAFE__MAX__ENCRYPT()) < 0, m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Frame exceeds AES-GCM cryptographic safety for a single key/iv.")))
			_ = _4_valueOrError2
			if (_4_valueOrError2).IsFailure() {
				return (_4_valueOrError2).PropagateFailure()
			} else {
				var _5_valueOrError3 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.ReadUint64Seq((_1_iv).Dtor_tail())
				_ = _5_valueOrError3
				if (_5_valueOrError3).IsFailure() {
					return (_5_valueOrError3).PropagateFailure()
				} else {
					var _6_encContent m_SerializeFunctions.SuccessfulRead = (_5_valueOrError3).Extract().(m_SerializeFunctions.SuccessfulRead)
					_ = _6_encContent
					var _7_valueOrError4 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_6_encContent).Dtor_tail(), _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetTagLength((header).Dtor_suite())))
					_ = _7_valueOrError4
					if (_7_valueOrError4).IsFailure() {
						return (_7_valueOrError4).PropagateFailure()
					} else {
						var _8_authTag m_SerializeFunctions.SuccessfulRead = (_7_valueOrError4).Extract().(m_SerializeFunctions.SuccessfulRead)
						_ = _8_authTag
						var _9_nonFramed Frame = Companion_Frame_.Create_NonFramed_(header, (_1_iv).Dtor_data().(_dafny.Sequence), (_6_encContent).Dtor_data().(_dafny.Sequence), (_8_authTag).Dtor_data().(_dafny.Sequence))
						_ = _9_nonFramed
						return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_(_9_nonFramed, (_8_authTag).Dtor_tail()))
					}
				}
			}
		}
	}
}