File tree Expand file tree Collapse file tree 3 files changed +3
-3
lines changed
source/portable/NetworkInterface
test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1 Expand file tree Collapse file tree 3 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -980,5 +980,5 @@ size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetwo
980980 }
981981 }
982982
983- return ( BUFFER_SIZE_ROUNDED_UP - BUFFER_SIZE_ROUNDED_UP );
983+ return ( BUFFER_SIZE_ROUNDED_UP - ipBUFFER_PADDING );
984984}
Original file line number Diff line number Diff line change @@ -67,6 +67,7 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkB
6767size_t uxNetworkInterfaceAllocateRAMToBuffers ( NetworkBufferDescriptor_t pxNetworkBuffers [ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
6868{
6969 /* FIX ME. */
70+ return 0 ;
7071}
7172
7273BaseType_t xGetPhyLinkStatus ( void )
Original file line number Diff line number Diff line change @@ -34,12 +34,11 @@ size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetwo
3434 * configASSERT( ( uxMaxNetworkInterfaceAllocatedSizeBytes >= ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) ) );
3535 *
3636 */
37- size_t xAllocSize = 0 ;
37+ size_t xAllocSize = ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ;
3838
3939 for ( int x = 0 ; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ; x ++ )
4040 {
4141 NetworkBufferDescriptor_t * current = & pxNetworkBuffers [ x ];
42- xAllocSize = ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ;
4342 current -> pucEthernetBuffer = malloc ( xAllocSize );
4443 __CPROVER_assume ( current -> pucEthernetBuffer != NULL );
4544 current -> xDataLength = sizeof ( ARPPacket_t );
You can’t perform that action at this time.
0 commit comments