Skip to content

Commit c846cae

Browse files
fixup! Use vSocketCloseNextTime instead of FreeRTOS_closesocket
1 parent eeb5801 commit c846cae

File tree

2 files changed

+32
-0
lines changed

2 files changed

+32
-0
lines changed

test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,22 @@
3737

3838
#include "../../utility/memory_assignments.c"
3939

40+
/* Abstraction of xTaskGetCurrentTaskHandle */
41+
TaskHandle_t xTaskGetCurrentTaskHandle( void )
42+
{
43+
static int xIsInit = 0;
44+
static TaskHandle_t pxCurrentTCB;
45+
TaskHandle_t xRandomTaskHandle; /* not initialized on purpose */
46+
47+
if( xIsInit == 0 )
48+
{
49+
pxCurrentTCB = xRandomTaskHandle;
50+
xIsInit = 1;
51+
}
52+
53+
return pxCurrentTCB;
54+
}
55+
4056
/* This proof assumes that prvTCPPrepareSend and prvTCPReturnPacket are correct.
4157
* These functions are proved to be correct separately. */
4258

test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,22 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
3636
return safeMalloc( sizeof( FreeRTOS_Socket_t ) );
3737
}
3838

39+
/* Abstraction of xTaskGetCurrentTaskHandle */
40+
TaskHandle_t xTaskGetCurrentTaskHandle( void )
41+
{
42+
static int xIsInit = 0;
43+
static TaskHandle_t pxCurrentTCB;
44+
TaskHandle_t xRandomTaskHandle; /* not initialized on purpose */
45+
46+
if( xIsInit == 0 )
47+
{
48+
pxCurrentTCB = xRandomTaskHandle;
49+
xIsInit = 1;
50+
}
51+
52+
return pxCurrentTCB;
53+
}
54+
3955
/* Abstraction of pxTCPSocketLookup */
4056
FreeRTOS_Socket_t * pxTCPSocketLookup( uint32_t ulLocalIP,
4157
UBaseType_t uxLocalPort,

0 commit comments

Comments
 (0)