Skip to content

Commit

Permalink
Merge branch 'main' into dev-stream-buffer-const
Browse files Browse the repository at this point in the history
  • Loading branch information
@HTRamsey
HTRamsey authored Jan 2, 2024
2 parents 5429bba + fcd2de0 commit 317fcb6
Show file tree
Hide file tree
Showing 7 changed files with 66 additions and 62 deletions.
4 changes: 2 additions & 2 deletions source/FreeRTOS_Sockets.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1171,7 +1171,7 @@ static NetworkBufferDescriptor_t * prvRecvFromWaitForPacket( FreeRTOS_Socket_t c

if( lPacketCount > 0 )
{
taskENTER_CRITICAL();
vTaskSuspendAll();
{
/* The owner of the list item is the network buffer. */
pxNetworkBuffer = ( ( NetworkBufferDescriptor_t * ) listGET_OWNER_OF_HEAD_ENTRY( &( pxSocket->u.xUDP.xWaitingPacketsList ) ) );
Expand All @@ -1183,7 +1183,7 @@ static NetworkBufferDescriptor_t * prvRecvFromWaitForPacket( FreeRTOS_Socket_t c
( void ) uxListRemove( &( pxNetworkBuffer->xBufferListItem ) );
}
}
taskEXIT_CRITICAL();
( void ) xTaskResumeAll();
}

*pxEventBits = xEventBits;
Expand Down
7 changes: 0 additions & 7 deletions source/FreeRTOS_TCP_WIN.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1158,7 +1158,6 @@
pxWindow->usOurPortNumber,
( unsigned ) ( ulSequenceNumber - pxWindow->rx.ulFirstSequenceNumber ),
( unsigned ) listCURRENT_LIST_LENGTH( &pxWindow->xRxSegments ) ) );
FreeRTOS_flush_logging();
}

/* Return a positive value. The packet may be accepted
Expand Down Expand Up @@ -1391,7 +1390,6 @@
( int ) pxSegment->lDataLength,
( unsigned ) ( pxWindow->ulNextTxSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ),
( int ) pxSegment->lStreamPos ) );
FreeRTOS_flush_logging();
}

return lToWrite;
Expand Down Expand Up @@ -1703,7 +1701,6 @@
( int ) pxSegment->lDataLength,
( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ),
( unsigned ) pxSegment->ulSequenceNumber ) );
FreeRTOS_flush_logging();
}
}
else
Expand Down Expand Up @@ -1776,7 +1773,6 @@
( int ) pxSegment->lDataLength,
( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ),
( unsigned ) ulWindowSize ) );
FreeRTOS_flush_logging();
}
}

Expand Down Expand Up @@ -1823,7 +1819,6 @@
( int ) pxSegment->lDataLength,
( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ),
( unsigned ) ulWindowSize ) );
FreeRTOS_flush_logging();
}
}
else
Expand Down Expand Up @@ -2137,7 +2132,6 @@
FreeRTOS_debug_printf( ( "prvTCPWindowFastRetransmit: Requeue sequence number %u < %u\n",
( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ),
( unsigned ) ( ulFirst - pxWindow->tx.ulFirstSequenceNumber ) ) );
FreeRTOS_flush_logging();
}

/* Remove it from xWaitQueue. */
Expand Down Expand Up @@ -2222,7 +2216,6 @@
( unsigned ) ( ulFirst - pxWindow->tx.ulFirstSequenceNumber ),
( unsigned ) ( ulLast - pxWindow->tx.ulFirstSequenceNumber ),
( unsigned ) ( pxWindow->tx.ulCurrentSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ) ) );
FreeRTOS_flush_logging();
}

return ulAckCount;
Expand Down
10 changes: 3 additions & 7 deletions source/FreeRTOS_UDP_IPv4.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -445,13 +445,9 @@ BaseType_t xProcessReceivedUDPPacket_IPv4( NetworkBufferDescriptor_t * pxNetwork
{
vTaskSuspendAll();
{
taskENTER_CRITICAL();
{
/* Add the network packet to the list of packets to be
* processed by the socket. */
vListInsertEnd( &( pxSocket->u.xUDP.xWaitingPacketsList ), &( pxNetworkBuffer->xBufferListItem ) );
}
taskEXIT_CRITICAL();
/* Add the network packet to the list of packets to be
* processed by the socket. */
vListInsertEnd( &( pxSocket->u.xUDP.xWaitingPacketsList ), &( pxNetworkBuffer->xBufferListItem ) );
}
( void ) xTaskResumeAll();

Expand Down
10 changes: 3 additions & 7 deletions source/FreeRTOS_UDP_IPv6.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -536,13 +536,9 @@ BaseType_t xProcessReceivedUDPPacket_IPv6( NetworkBufferDescriptor_t * pxNetwork
{
vTaskSuspendAll();
{
taskENTER_CRITICAL();
{
/* Add the network packet to the list of packets to be
* processed by the socket. */
vListInsertEnd( &( pxSocket->u.xUDP.xWaitingPacketsList ), &( pxNetworkBuffer->xBufferListItem ) );
}
taskEXIT_CRITICAL();
/* Add the network packet to the list of packets to be
* processed by the socket. */
vListInsertEnd( &( pxSocket->u.xUDP.xWaitingPacketsList ), &( pxNetworkBuffer->xBufferListItem ) );
}
( void ) xTaskResumeAll();

Expand Down
23 changes: 0 additions & 23 deletions source/include/FreeRTOSIPConfigDefaults.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3111,29 +3111,6 @@

/*---------------------------------------------------------------------------*/

/*
* FreeRTOS_flush_logging
*
* Type: Macro Function
*
* Macro that is called in cases where a lot of logging is produced.
*
* This gives the logging module a chance to flush the data.
*/

#ifndef FreeRTOS_flush_logging
#define FreeRTOS_flush_logging() \
if( ipconfigHAS_PRINTF || ipconfigHAS_DEBUG_PRINTF ) \
{ \
do {} while( ipFALSE_BOOL ); \
} \
else \
{ \
}
#endif

/*---------------------------------------------------------------------------*/

/*
* ipconfigTCP_IP_SANITY
*
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/CheckOptionsInner/Makefile.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
"CBMCFLAGS": [
"--unwind 1",
"--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowTxCheckAck.0:2",
"--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowFastRetransmit.1:2"
"--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowFastRetransmit.0:2"
],
"OPT":
[
Expand Down
72 changes: 57 additions & 15 deletions test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_UDP_API_utest.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -380,9 +380,14 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_JustUDPHeader( void )

listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 );

listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
vTaskSuspendAll_Expect();

uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 );
{
listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );

uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 );
}
xTaskResumeAll_ExpectAndReturn( pdFALSE );

uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER );

Expand Down Expand Up @@ -441,9 +446,13 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_Packet100( void )

listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 );

listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
vTaskSuspendAll_Expect();
{
listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );

uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 );
uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 );
}
xTaskResumeAll_ExpectAndReturn( pdFALSE );

uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER );

Expand Down Expand Up @@ -503,9 +512,13 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_Packet100SizeSmall( void

listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 );

listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
vTaskSuspendAll_Expect();
{
listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );

uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 );
uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 );
}
xTaskResumeAll_ExpectAndReturn( pdFALSE );

uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER );

Expand Down Expand Up @@ -566,7 +579,13 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_Packet100SizeSmall_Peek(

listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 );

listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
vTaskSuspendAll_Expect();

{
listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
}

xTaskResumeAll_ExpectAndReturn( pdFALSE );

uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER );

Expand Down Expand Up @@ -624,7 +643,12 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_Packet100SizeSmall_Peek_

listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 );

listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
vTaskSuspendAll_Expect();

{
listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
}
xTaskResumeAll_ExpectAndReturn( pdFALSE );

uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER );

Expand Down Expand Up @@ -681,9 +705,15 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_Packet100SizeSmall_ZeroC

listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 );

listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
vTaskSuspendAll_Expect();

{
listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );

uxListRemove_ExpectAndReturn( &xNetworkBuffer.xBufferListItem, 0U );
}

uxListRemove_ExpectAndReturn( &xNetworkBuffer.xBufferListItem, 0U );
xTaskResumeAll_ExpectAndReturn( pdFALSE );

uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER );

Expand Down Expand Up @@ -733,7 +763,11 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBegining_Packet100SizeSmall_Zero
xListItem.pvOwner = &xNetworkBuffer;
xSocket->u.xUDP.xWaitingPacketsList.xListEnd.pxNext = &xListItem;

listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
vTaskSuspendAll_Expect();
{
listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
}
xTaskResumeAll_ExpectAndReturn( pdFALSE );

uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER );

Expand Down Expand Up @@ -789,9 +823,13 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_IPv6Packet100( void )

listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 );

listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
vTaskSuspendAll_Expect();
{
listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );

uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 );
uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 );
}
xTaskResumeAll_ExpectAndReturn( pdFALSE );

uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv6_HEADER );

Expand Down Expand Up @@ -850,9 +888,13 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_UnknownIPHeaderSize( voi

listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 );

listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );
vTaskSuspendAll_Expect();
{
listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer );

uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 );
uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 );
}
xTaskResumeAll_ExpectAndReturn( pdFALSE );

uxIPHeaderSizePacket_IgnoreAndReturn( 0xFF );

Expand Down

0 comments on commit 317fcb6

Please sign in to comment.