Remove unused FreeRTOS_flush_logging (#1066)

* Remove unused FreeRTOS_flush_logging * Fix CBMC failures --------- Co-authored-by: tony-josi-aws <[email protected]>
FreeRTOS · Jan 2, 2024 · fcd2de0 · fcd2de0
1 parent af07ccf
commit fcd2de0
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 31 deletions.
diff --git a/source/FreeRTOS_TCP_WIN.c b/source/FreeRTOS_TCP_WIN.c
@@ -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
@@ -1391,7 +1390,6 @@
                                          ( int ) pxSegment->lDataLength,
                                          ( unsigned ) ( pxWindow->ulNextTxSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ),
                                          ( int ) pxSegment->lStreamPos ) );
-                FreeRTOS_flush_logging();
             }
 
             return lToWrite;
@@ -1703,7 +1701,6 @@
                                                  ( int ) pxSegment->lDataLength,
                                                  ( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ),
                                                  ( unsigned ) pxSegment->ulSequenceNumber ) );
-                        FreeRTOS_flush_logging();
                     }
                 }
                 else
@@ -1776,7 +1773,6 @@
                                              ( int ) pxSegment->lDataLength,
                                              ( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ),
                                              ( unsigned ) ulWindowSize ) );
-                    FreeRTOS_flush_logging();
                 }
             }
 
@@ -1823,7 +1819,6 @@
                                              ( int ) pxSegment->lDataLength,
                                              ( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ),
                                              ( unsigned ) ulWindowSize ) );
-                    FreeRTOS_flush_logging();
                 }
             }
             else
@@ -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. */
@@ -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;

diff --git a/source/include/FreeRTOSIPConfigDefaults.h b/source/include/FreeRTOSIPConfigDefaults.h
@@ -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
  *

diff --git a/test/cbmc/proofs/CheckOptionsInner/Makefile.json b/test/cbmc/proofs/CheckOptionsInner/Makefile.json
@@ -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":
   [