Home
last modified time | relevance | path

Searched refs:uxBufferLength (Results 1 – 25 of 47) sorted by relevance

12

/FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/
DusGenerateProtocolChecksum_IPv6_harness.c86 size_t uxBufferLength ) in prvPrepareExtensionHeaders() argument
93 size_t uxReturn = uxBufferLength; in prvPrepareExtensionHeaders()
102 while( ( uxIndex + 8U ) < uxBufferLength ) in prvPrepareExtensionHeaders()
111 if( ( uxIndex + uxHopSize ) >= uxBufferLength ) in prvPrepareExtensionHeaders()
123 __CPROVER_assume( uxBufferLength - uxIndex >= sizeof( ProtocolHeaders_t ) ); in prvPrepareExtensionHeaders()
130 __CPROVER_assume( uxBufferLength - uxIndex >= sizeof( ProtocolHeaders_t ) ); in prvPrepareExtensionHeaders()
141 __CPROVER_assume( uxBufferLength - uxIndex >= sizeof( ProtocolHeaders_t ) ); in prvPrepareExtensionHeaders()
147 size_t uxBufferLength; in harness() local
153 …_CPROVER_assume( ( uxBufferLength >= ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( Protoc… in harness()
154 pucEthernetBuffer = safeMalloc( uxBufferLength ); in harness()
[all …]
/FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/Socket/prvRecvFrom_CopyPacket/
DRecvFrom_CopyPacket_harness.c23 size_t uxBufferLength,
31 size_t uxBufferLength; in harness() local
39 __CPROVER_assume( uxBufferLength > 0 && uxBufferLength < ipconfigNETWORK_MTU ); in harness()
47 pvBuffer = safeMalloc( uxBufferLength ); in harness()
49 …eRTOS_Sockets_c_prvRecvFrom_CopyPacket( pucEthernetBuffer, pvBuffer, uxBufferLength, xFlags, lData… in harness()
60 …RTOS_Sockets_c_prvRecvFrom_CopyPacket( pucEthernetBuffer, &pvBuffer, uxBufferLength, xFlags, lData… in harness()
/FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/
DusGenerateProtocolChecksum_harness.c51 size_t uxBufferLength; in harness() local
59 …__CPROVER_assume( uxBufferLength >= ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv4_HEADER + sizeof( Protoco… in harness()
60 pucEthernetBuffer = safeMalloc( uxBufferLength ); in harness()
71 …__CPROVER_assume( uxBufferLength >= ipSIZE_OF_ETH_HEADER + usHeaderLength + sizeof( ProtocolHeader… in harness()
73 …__CPROVER_assume( ( usHeaderLength <= ( uxBufferLength - ipSIZE_OF_ETH_HEADER ) ) && ( usHeaderLen… in harness()
78 ( void ) usGenerateProtocolChecksum( pucEthernetBuffer, uxBufferLength, xOutgoingPacket ); in harness()
/FreeRTOS-Plus-TCP-v4.0.0/source/
DFreeRTOS_IPv6_Utils.c75 size_t uxBufferLength, in prvChecksumIPv6Checks() argument
86 if( uxBufferLength < sizeof( IPPacket_IPv6_t ) ) in prvChecksumIPv6Checks()
93 …uxExtensionHeaderLength = usGetExtensionHeaderLength( pucEthernetBuffer, uxBufferLength, &pxSet->u… in prvChecksumIPv6Checks()
95 if( uxExtensionHeaderLength >= uxBufferLength ) in prvChecksumIPv6Checks()
114 if( uxBufferLength < uxNeeded ) in prvChecksumIPv6Checks()
133 BaseType_t prvChecksumICMPv6Checks( size_t uxBufferLength, in prvChecksumICMPv6Checks() argument
155 if( uxBufferLength < ( ipSIZE_OF_ETH_HEADER + pxSet->uxIPHeaderLength + xICMPLength ) ) in prvChecksumICMPv6Checks()
185 size_t uxBufferLength, in usGetExtensionHeaderLength() argument
195 size_t uxReturn = uxBufferLength; in usGetExtensionHeaderLength()
208 while( ( uxIndex + 8U ) < uxBufferLength ) in usGetExtensionHeaderLength()
[all …]
DFreeRTOS_IPv4_Utils.c79 size_t uxBufferLength, in prvChecksumIPv4Checks() argument
107 if( uxBufferLength < sizeof( IPPacket_t ) ) in prvChecksumIPv4Checks()
117 if( uxBufferLength < ( ipSIZE_OF_ETH_HEADER + pxSet->uxIPHeaderLength ) ) in prvChecksumIPv4Checks()
133 if( uxBufferLength < uxNeeded ) in prvChecksumIPv4Checks()
DFreeRTOS_IPv4.c57 size_t uxBufferLength );
73 size_t uxBufferLength ) in xCheckIPv4SizeFields() argument
92 if( uxBufferLength < sizeof( IPPacket_t ) ) in xCheckIPv4SizeFields()
113 if( uxBufferLength < ( ipSIZE_OF_ETH_HEADER + uxIPHeaderLength ) ) in xCheckIPv4SizeFields()
123 if( uxBufferLength < ( size_t ) ( ipSIZE_OF_ETH_HEADER + ( size_t ) usLength ) ) in xCheckIPv4SizeFields()
154 if( uxBufferLength < uxMinimumLength ) in xCheckIPv4SizeFields()
DFreeRTOS_IPv6.c70 size_t uxBufferLength );
90 size_t uxBufferLength ) in xCheckIPv6SizeFields() argument
110 if( uxBufferLength < sizeof( IPHeader_IPv6_t ) ) in xCheckIPv6SizeFields()
126 if( uxBufferLength < ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER ) ) in xCheckIPv6SizeFields()
135 …if( uxBufferLength != ( size_t ) ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + ( size_t ) usPay… in xCheckIPv6SizeFields()
152 … if( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + uxExtHeaderLength >= uxBufferLength ) in xCheckIPv6SizeFields()
158 if( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + uxExtHeaderLength >= uxBufferLength ) in xCheckIPv6SizeFields()
185 if( uxBufferLength < uxMinimumLength ) in xCheckIPv6SizeFields()
DFreeRTOS_IP_Utils.c121 static BaseType_t prvChecksumProtocolChecks( size_t uxBufferLength,
132 size_t uxBufferLength,
384 static BaseType_t prvChecksumProtocolChecks( size_t uxBufferLength, in prvChecksumProtocolChecks() argument
396 … ( uxBufferLength < ( ipSIZE_OF_ETH_HEADER + pxSet->uxIPHeaderLength + ipSIZE_OF_UDP_HEADER ) ) ) in prvChecksumProtocolChecks()
415 … ( uxBufferLength < ( ipSIZE_OF_ETH_HEADER + pxSet->uxIPHeaderLength + ipSIZE_OF_TCP_HEADER ) ) ) in prvChecksumProtocolChecks()
448 …( uxBufferLength < ( ipSIZE_OF_ETH_HEADER + pxSet->uxIPHeaderLength + ipSIZE_OF_ICMPv4_HEADER ) ) ) in prvChecksumProtocolChecks()
475 xReturn = prvChecksumICMPv6Checks( uxBufferLength, pxSet ); in prvChecksumProtocolChecks()
659 size_t uxBufferLength, in prvChecksumProtocolSetChecksum() argument
688 ( void ) uxBufferLength; in prvChecksumProtocolSetChecksum()
1029 size_t uxBufferLength, in usGenerateProtocolChecksum() argument
[all …]
/FreeRTOS-Plus-TCP-v4.0.0/test/unit-test/FreeRTOS_IP_Utils/
DFreeRTOS_IP_Utils_stubs.c84 BaseType_t prvChecksumICMPv6Checks_Valid( size_t uxBufferLength, in prvChecksumICMPv6Checks_Valid() argument
92 BaseType_t prvChecksumICMPv6Checks_BigHeaderLength( size_t uxBufferLength, in prvChecksumICMPv6Checks_BigHeaderLength() argument
101 size_t uxBufferLength, in prvChecksumIPv6Checks_Valid() argument
121 size_t uxBufferLength, in prvChecksumIPv4Checks_Valid() argument
141 size_t uxBufferLength, in prvChecksumIPv4Checks_UnknownProtocol() argument
145 prvChecksumIPv4Checks_Valid( pucEthernetBuffer, uxBufferLength, pxSet, NumCalls ); in prvChecksumIPv4Checks_UnknownProtocol()
153 size_t uxBufferLength, in prvChecksumIPv4Checks_InvalidLength() argument
159 prvChecksumIPv4Checks_Valid( pucEthernetBuffer, uxBufferLength, pxSet, NumCalls ); in prvChecksumIPv4Checks_InvalidLength()
161 if( uxBufferLength < sizeof( IPPacket_t ) ) in prvChecksumIPv4Checks_InvalidLength()
DFreeRTOS_IP_Utils_utest.c730 size_t uxBufferLength = usLength + ipSIZE_OF_ETH_HEADER; in test_usGenerateProtocolChecksum_UnknownProtocol() local
748 usReturn = usGenerateProtocolChecksum( pucEthernetBuffer, uxBufferLength, xOutgoingPacket ); in test_usGenerateProtocolChecksum_UnknownProtocol()
761 size_t uxBufferLength = sizeof( IPPacket_t ) - 1; in test_usGenerateProtocolChecksum_InvalidLength() local
769 usReturn = usGenerateProtocolChecksum( pucEthernetBuffer, uxBufferLength, xOutgoingPacket ); in test_usGenerateProtocolChecksum_InvalidLength()
787 size_t uxBufferLength = ucVersionHeaderLength + ipSIZE_OF_ETH_HEADER + ipSIZE_OF_UDP_HEADER - 1; in test_usGenerateProtocolChecksum_UDPInvalidLength() local
800 usReturn = usGenerateProtocolChecksum( pucEthernetBuffer, uxBufferLength, xOutgoingPacket ); in test_usGenerateProtocolChecksum_UDPInvalidLength()
818 size_t uxBufferLength = ucVersionHeaderLength + ipSIZE_OF_ETH_HEADER + ipSIZE_OF_UDP_HEADER; in test_usGenerateProtocolChecksum_UDPWrongCRCIncomingPacket() local
831 usReturn = usGenerateProtocolChecksum( pucEthernetBuffer, uxBufferLength, xOutgoingPacket ); in test_usGenerateProtocolChecksum_UDPWrongCRCIncomingPacket()
849 size_t uxBufferLength = ucVersionHeaderLength + ipSIZE_OF_ETH_HEADER + ipSIZE_OF_UDP_HEADER; in test_usGenerateProtocolChecksum_UDPOutgoingPacketLessProtocolLength() local
862 usReturn = usGenerateProtocolChecksum( pucEthernetBuffer, uxBufferLength, xOutgoingPacket ); in test_usGenerateProtocolChecksum_UDPOutgoingPacketLessProtocolLength()
[all …]
/FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/IPUtils/prvPacketBuffer_to_NetworkBuffer/
DprvPacketBuffer_to_NetworkBuffer_harness.c45 size_t uxBufferLength; in harness() local
49 …__CPROVER_assume( ( uxBufferLength > ipBUFFER_PADDING ) && ( uxBufferLength < ipBUFFER_PADDING + i… in harness()
50 __CPROVER_assume( uxOffset <= uxBufferLength - ipBUFFER_PADDING ); in harness()
55 pxNetworkBuffer->pucEthernetBuffer = safeMalloc( uxBufferLength ); in harness()
/FreeRTOS-Plus-TCP-v4.0.0/test/unit-test/FreeRTOS_IPv6_Utils/
DFreeRTOS_IPv6_Utils_utest.c110 size_t uxBufferLength = sizeof( IPHeader_IPv6_t ) - 1; in test_prvChecksumIPv6Checks_InvalidLength() local
117 usReturn = prvChecksumIPv6Checks( pucEthernetBuffer, uxBufferLength, &xSet ); in test_prvChecksumIPv6Checks_InvalidLength()
133 size_t uxBufferLength = ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER; in test_prvChecksumIPv6Checks_IncompleteIPv6Packet() local
144 usReturn = prvChecksumIPv6Checks( pucEthernetBuffer, uxBufferLength, &xSet ); in test_prvChecksumIPv6Checks_IncompleteIPv6Packet()
159 size_t uxBufferLength = ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + 1; in test_prvChecksumIPv6Checks_Success() local
169 usReturn = prvChecksumIPv6Checks( pucEthernetBuffer, uxBufferLength, &xSet ); in test_prvChecksumIPv6Checks_Success()
247 …size_t uxBufferLength = ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + ipSIZE_OF_ICMPv6_HEADER - 1; in test_prvChecksumICMPv6Checks_Default_InvalidLength() local
258 usReturn = prvChecksumICMPv6Checks( uxBufferLength, &xSet ); in test_prvChecksumICMPv6Checks_Default_InvalidLength()
270 …size_t uxBufferLength = ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + ipSIZE_OF_ICMPv6_HEADER + 1; in test_prvChecksumICMPv6Checks_Default_ValidLength() local
281 usReturn = prvChecksumICMPv6Checks( uxBufferLength, &xSet ); in test_prvChecksumICMPv6Checks_Default_ValidLength()
[all …]
/FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/ParseDNSReply/
DParseDNSReply_harness.c29 size_t uxBufferLength,
116 size_t uxBufferLength; in harness() local
118 uint8_t * pucUDPPayloadBuffer = malloc( uxBufferLength ); in harness()
123 __CPROVER_assume( uxBufferLength < CBMC_MAX_OBJECT_SIZE ); in harness()
124 __CPROVER_assume( uxBufferLength <= NETWORK_BUFFER_SIZE ); in harness()
128 uxBufferLength, in harness()
/FreeRTOS-Plus-TCP-v4.0.0/test/unit-test/FreeRTOS_IPv4_Utils/
DFreeRTOS_IPv4_Utils_utest.c78 size_t uxBufferLength = usLength + ipSIZE_OF_ETH_HEADER; in test_prvChecksumIPv4Checks_IPLengthLessThanHeaderLength() local
87 xReturn = prvChecksumIPv4Checks( pucEthernetBuffer, uxBufferLength, &xSet ); in test_prvChecksumIPv4Checks_IPLengthLessThanHeaderLength()
106 size_t uxBufferLength = ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv4_HEADER - 1; in test_prvChecksumIPv4Checks_BufferLessIPPacket() local
115 xReturn = prvChecksumIPv4Checks( pucEthernetBuffer, uxBufferLength, &xSet ); in test_prvChecksumIPv4Checks_BufferLessIPPacket()
134 size_t uxBufferLength = ipSIZE_OF_ETH_HEADER + ucVersionHeaderLength - 1; in test_prvChecksumIPv4Checks_BufferLessIPHeaderLength() local
143 xReturn = prvChecksumIPv4Checks( pucEthernetBuffer, uxBufferLength, &xSet ); in test_prvChecksumIPv4Checks_BufferLessIPHeaderLength()
162 size_t uxBufferLength = ipSIZE_OF_ETH_HEADER + usLength - 1; in test_prvChecksumIPv4Checks_BufferLessIPPayloadLength() local
171 xReturn = prvChecksumIPv4Checks( pucEthernetBuffer, uxBufferLength, &xSet ); in test_prvChecksumIPv4Checks_BufferLessIPPayloadLength()
189 size_t uxBufferLength = ipSIZE_OF_ETH_HEADER + usLength; in test_prvChecksumIPv4Checks_Pass() local
199 xReturn = prvChecksumIPv4Checks( pucEthernetBuffer, uxBufferLength, &xSet ); in test_prvChecksumIPv4Checks_Pass()
/FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/IPUtils/pxUDPPayloadBuffer_to_NetworkBuffer/
DpxUDPPayloadBuffer_to_NetworkBuffer_harness.c52 size_t uxBufferLength; in harness() local
62 __CPROVER_assume( uxBufferLength > sizeof( UDPPacket_IPv6_t ) + ipconfigBUFFER_PADDING ); in harness()
66 __CPROVER_assume( uxBufferLength > sizeof( UDPPacket_t ) + ipconfigBUFFER_PADDING ); in harness()
69 __CPROVER_assume( uxBufferLength < ipconfigNETWORK_MTU ); in harness()
74 pxNetworkBuffer->pucEthernetBuffer = safeMalloc( uxBufferLength ); in harness()
/FreeRTOS-Plus-TCP-v4.0.0/test/unit-test/FreeRTOS_DNS_Parser/
DFreeRTOS_DNS_Parser_utest.c722 size_t uxBufferLength; in test_DNS_TreatNBNS_Fail_MinimumBufferSize() local
742 size_t uxBufferLength; in test_DNS_TreatNBNS_Fail_NullPayload() local
762 size_t uxBufferLength; in test_DNS_TreatNBNS_success() local
790 size_t uxBufferLength; in test_DNS_TreatNBNS_FailNullPayload() local
815 size_t uxBufferLength; in test_DNS_TreatNBNS_FailLessBufferSize() local
840 size_t uxBufferLength; in test_DNS_TreatNBNS_success_nbns_mask() local
863 size_t uxBufferLength; in test_DNS_TreatNBNS_success_nbns_query_trailing_space() local
890 size_t uxBufferLength; in test_DNS_TreatNBNS_success_nbns_query() local
918 size_t uxBufferLength = 300; in test_DNS_TreatNBNS_success_nbns_query_network_buffer_null() local
932 uxBufferLength, in test_DNS_TreatNBNS_success_nbns_query_network_buffer_null()
[all …]
/FreeRTOS-Plus-TCP-v4.0.0/test/unit-test/FreeRTOS_DHCP/
DFreeRTOS_DHCP_stubs.c266 size_t uxBufferLength, in RecvFromStub() argument
297 size_t uxBufferLength, in FreeRTOS_recvfrom_Generic() argument
313 size_t uxBufferLength, in FreeRTOS_recvfrom_Generic_NullBuffer() argument
326 size_t uxBufferLength, in FreeRTOS_recvfrom_eWaitingOfferRecvfromLessBytesNoTimeout() argument
344 … size_t uxBufferLength, in FreeRTOS_recvfrom_ResetAndIncorrectStateWithSocketAlreadyCreated_validUDPmessage() argument
367 … size_t uxBufferLength, in FreeRTOS_recvfrom_ResetAndIncorrectStateWithSocketAlreadyCreated_validUDPmessage_TwoFlagOptions_nullbytes() argument
399 … size_t uxBufferLength, in FreeRTOS_recvfrom_ResetAndIncorrectStateWithSocketAlreadyCreated_validUDPmessage_TwoFlagOptions_nullbuffer() argument
427 … size_t uxBufferLength, in FreeRTOS_recvfrom_ResetAndIncorrectStateWithSocketAlreadyCreated_validUDPmessage_IncorrectDHCPCookie() argument
450 … size_t uxBufferLength, in FreeRTOS_recvfrom_ResetAndIncorrectStateWithSocketAlreadyCreated_validUDPmessage_IncorrectOpCode() argument
473 … size_t uxBufferLength, in FreeRTOS_recvfrom_eWaitingOfferRecvfromSucceedsFalseCookieNoTimeout() argument
[all …]
/FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/IPUtils/pxDuplicateNetworkBufferWithDescriptor/
DpxDuplicateNetworkBufferWithDescriptor_harness.c72 size_t uxBufferLength; in harness() local
76 __CPROVER_assume( uxBufferLength < ipconfigNETWORK_MTU ); in harness()
82 pxNetworkBuffer->pucEthernetBuffer = safeMalloc( uxBufferLength ); in harness()
86 pxNetworkBuffer->xDataLength = uxBufferLength; in harness()
/FreeRTOS-Plus-TCP-v4.0.0/source/include/
DFreeRTOS_IPv6_Utils.h58 size_t uxBufferLength,
61 extern BaseType_t prvChecksumICMPv6Checks( size_t uxBufferLength,
66 size_t uxBufferLength,
DFreeRTOS_DNS_Parser.h64 size_t uxBufferLength,
78 size_t uxBufferLength,
DFreeRTOS_IPv4_Utils.h58 size_t uxBufferLength,
/FreeRTOS-Plus-TCP-v4.0.0/test/unit-test/FreeRTOS_Sockets/
DFreeRTOS_Sockets_UDP_API_utest.c77 size_t uxBufferLength; in test_FreeRTOS_recvfrom_NullSocket() local
82 …lReturn = FreeRTOS_recvfrom( xSocket, pvBuffer, uxBufferLength, xFlags, pxSourceAddress, pxSourceA… in test_FreeRTOS_recvfrom_NullSocket()
96 size_t uxBufferLength; in test_FreeRTOS_recvfrom_TCPSocket() local
107 …lReturn = FreeRTOS_recvfrom( xSocket, pvBuffer, uxBufferLength, xFlags, pxSourceAddress, pxSourceA… in test_FreeRTOS_recvfrom_TCPSocket()
121 size_t uxBufferLength; in test_FreeRTOS_recvfrom_NonBlockingInterrupted() local
136 …lReturn = FreeRTOS_recvfrom( xSocket, pvBuffer, uxBufferLength, xFlags, pxSourceAddress, pxSourceA… in test_FreeRTOS_recvfrom_NonBlockingInterrupted()
150 size_t uxBufferLength; in test_FreeRTOS_recvfrom_NonBlocking() local
165 …lReturn = FreeRTOS_recvfrom( xSocket, pvBuffer, uxBufferLength, xFlags, pxSourceAddress, pxSourceA… in test_FreeRTOS_recvfrom_NonBlocking()
179 size_t uxBufferLength; in test_FreeRTOS_recvfrom_NonBlockingFlagSet() local
193 …lReturn = FreeRTOS_recvfrom( xSocket, pvBuffer, uxBufferLength, xFlags, pxSourceAddress, pxSourceA… in test_FreeRTOS_recvfrom_NonBlockingFlagSet()
[all …]
DFreeRTOS_Sockets_TCP_API_utest.c373 size_t uxBufferLength = 1500; in test_FreeRTOS_recv_InvalidValues() local
380 xReturn = FreeRTOS_recv( &xSocket, pvBuffer, uxBufferLength, xFlags ); in test_FreeRTOS_recv_InvalidValues()
384 xReturn = FreeRTOS_recv( NULL, pvBuffer, uxBufferLength, xFlags ); in test_FreeRTOS_recv_InvalidValues()
390 xReturn = FreeRTOS_recv( &xSocket, pvBuffer, uxBufferLength, xFlags ); in test_FreeRTOS_recv_InvalidValues()
396 xReturn = FreeRTOS_recv( &xSocket, NULL, uxBufferLength, xFlags ); in test_FreeRTOS_recv_InvalidValues()
408 size_t uxBufferLength = 1500; in test_FreeRTOS_recv_NotConnectedAndNoMemory() local
415 xReturn = FreeRTOS_recv( &xSocket, pvBuffer, uxBufferLength, xFlags ); in test_FreeRTOS_recv_NotConnectedAndNoMemory()
423 xReturn = FreeRTOS_recv( &xSocket, pvBuffer, uxBufferLength, xFlags ); in test_FreeRTOS_recv_NotConnectedAndNoMemory()
435 size_t uxBufferLength = 1500; in test_FreeRTOS_recv_EstablishedConnection_NoWait() local
446 xReturn = FreeRTOS_recv( &xSocket, pvBuffer, uxBufferLength, xFlags ); in test_FreeRTOS_recv_EstablishedConnection_NoWait()
[all …]
/FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/
DProcessICMPMessage_IPv6_harness.c48 size_t uxBufferLength, in usGenerateProtocolChecksum() argument
54 …__CPROVER_assert( __CPROVER_r_ok( pucEthernetBuffer, uxBufferLength ), "pucEthernetBuffer should b… in usGenerateProtocolChecksum()
/FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/ND/prvReturnICMP_IPv6/
DReturnICMP_IPv6_harness.c48 size_t uxBufferLength, in usGenerateProtocolChecksum() argument
54 …__CPROVER_assert( __CPROVER_r_ok( pucEthernetBuffer, uxBufferLength ), "pucEthernetBuffer should b… in usGenerateProtocolChecksum()

12