moninom1 · moninom1 · Aug 12, 2024 · May 24, 2024 · May 24, 2024 · Jun 4, 2024
diff --git a/.github/.cSpellWords.txt b/.github/.cSpellWords.txt
@@ -724,6 +724,7 @@ CMock
 CNBTR
 CNDA
 CNDTR
+CNOT
 CNTALOAD
 CNTAMAX
 CNTBLOAD

diff --git a/.github/scripts/core_checker.py b/.github/scripts/core_checker.py
@@ -307,6 +307,7 @@
     r'FreeRTOS/Demo/CORTEX_M4F_Infineon_XMC4000_Keil/.*',
     r'FreeRTOS/Demo/CORTEX_MPU_R4F_TI_RM46_HERCULES_GCC/BoardFiles/.*',
     r'FreeRTOS/Demo/CORTEX_MPU_R5F_TI_RM57_HERCULES_GCC/BoardFiles/.*',
+    r'FreeRTOS/Demo/CORTEX_No_GIC_R5F_TI_RM57_HERCULES_GCC/BoardFiles/.*',
     r'FreeRTOS/Demo/AVR_ATMega4809_Atmel_Studio/RTOSDemo/.*',
     r'FreeRTOS/Demo/AVR32_UC3/.*',
     r'FreeRTOS/Demo/AVR_ATMega4809_IAR/.*',

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -81,7 +81,7 @@ jobs:
           # Therefore, we can just download it.
           mkdir -p freertos/FreeRTOS-Plus/Source/Application-Protocols/coreMQTT-Agent/source/dependency/coreMQTT/docs/doxygen/output
           wget -O freertos/FreeRTOS-Plus/Source/Application-Protocols/coreMQTT-Agent/source/dependency/coreMQTT/docs/doxygen/output/mqtt.tag \
-          "https://freertos.org/Documentation/api-ref/coreMQTT/docs/doxygen/output/mqtt.tag"
+          "https://freertos.github.io/coreMQTT/main/mqtt.tag"
 
       - name: Generate doxygen ZIP
         uses: FreeRTOS/CI-CD-Github-Actions/doxygen@main
@@ -168,6 +168,8 @@ jobs:
 
       - name: Set up CBMC runner
         uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main
+        with:
+          cbmc_version: "5.95.1"
 
       - name: Run CBMC
         uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main

diff --git a/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Posix/main_networking.c b/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Posix/main_networking.c
@@ -135,6 +135,7 @@ static UBaseType_t ulNextRand;
 
 void main_tcp_echo_client_tasks( void )
 {
+    BaseType_t xResult;
     const uint32_t ulLongTime_ms = pdMS_TO_TICKS( 1000UL );
 
     /*
@@ -157,8 +158,6 @@ void main_tcp_echo_client_tasks( void )
     /* Initialise the network interface.*/
     FreeRTOS_debug_printf( ( "FreeRTOS_IPInit\r\n" ) );
 
-    memcpy( ipLOCAL_MAC_ADDRESS, ucMACAddress, sizeof( ucMACAddress ) );
-
     #if defined( ipconfigIPv4_BACKWARD_COMPATIBLE ) && ( ipconfigIPv4_BACKWARD_COMPATIBLE == 0 )
         extern NetworkInterface_t * pxLibslirp_FillInterfaceDescriptor( BaseType_t xEMACIndex,
                                                                         NetworkInterface_t * pxInterface );
@@ -173,12 +172,14 @@ void main_tcp_echo_client_tasks( void )
         }
         #endif /* ( ipconfigUSE_DHCP != 0 ) */
 
-        FreeRTOS_IPInit_Multi();
+        xResult = FreeRTOS_IPInit_Multi();
     #else /* if defined( ipconfigIPv4_BACKWARD_COMPATIBLE ) && ( ipconfigIPv4_BACKWARD_COMPATIBLE == 0 ) */
         /* Using the old /single /IPv4 library, or using backward compatible mode of the new /multi library. */
-        FreeRTOS_IPInit( ucIPAddress, ucNetMask, ucGatewayAddress, ucDNSServerAddress, ucMACAddress );
+        xResult = FreeRTOS_IPInit( ucIPAddress, ucNetMask, ucGatewayAddress, ucDNSServerAddress, ucMACAddress );
     #endif /* if defined( ipconfigIPv4_BACKWARD_COMPATIBLE ) && ( ipconfigIPv4_BACKWARD_COMPATIBLE == 0 ) */
 
+    configASSERT( xResult == pdTRUE );
+
     /* Start the RTOS scheduler. */
     FreeRTOS_debug_printf( ( "vTaskStartScheduler\n" ) );
     vTaskStartScheduler();

diff --git a/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/FreeRTOSConfig.h b/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/FreeRTOSConfig.h
@@ -57,11 +57,8 @@ extern void vAssertCalled( void );
 #define configUSE_16_BIT_TICKS              0
 #define configIDLE_SHOULD_YIELD             0
 #define configMAX_PRIORITIES                ( 10 )
-#define configTIMER_QUEUE_LENGTH            20
-#define configTIMER_TASK_PRIORITY           ( configMAX_PRIORITIES - 3 )
 #define configUSE_COUNTING_SEMAPHORES       1
 #define configSUPPORT_DYNAMIC_ALLOCATION    1
-#define  configNUM_TX_DESCRIPTORS           15
 
 /* Set the following definitions to 1 to include the API function, or zero
  * to exclude the API function. */
@@ -74,7 +71,7 @@ extern void vAssertCalled( void );
 #define INCLUDE_vTaskDelete                     0
 #define INCLUDE_vTaskCleanUpResources           0
 #define INCLUDE_vTaskSuspend                    0
-#define INCLUDE_vTaskDelayUntil                 1
+#define INCLUDE_vTaskDelayUntil                 0
 #define INCLUDE_vTaskDelay                      1
 
 
@@ -89,7 +86,6 @@ extern void vAssertCalled( void );
 /* networking definitions */
 #define configMAC_ISR_SIMULATOR_PRIORITY    ( configMAX_PRIORITIES - 2 )
 #define ipconfigUSE_NETWORK_EVENT_HOOK      1
-/*#define ipconfigSOCK_DEFAULT_RECEIVE_BLOCK_TIME  pdMS_TO_TICKS(5000) */
 #define configNETWORK_INTERFACE_TO_USE      1L
 
 /* The address of an echo server that will be used by the two demo echo client
@@ -115,33 +111,33 @@ extern void vAssertCalled( void );
 #define configMAC_ADDR4    0x34
 #define configMAC_ADDR5    0xAD
 
-/* Default IP address configuration.  Used in ipconfigUSE_DNS is set to 0, or
- * ipconfigUSE_DNS is set to 1 but a DNS server cannot be contacted. */
+/* Default IP address configuration.  Used if ipconfigUSE_DHCP is set to 0, or
+ * ipconfigUSE_DHCP is set to 1 but a DHCP server cannot be contacted. */
 
 #define configIP_ADDR0    10
 #define configIP_ADDR1    211
 #define configIP_ADDR2    55
 #define configIP_ADDR3    5
 
-/* Default gateway IP address configuration.  Used in ipconfigUSE_DNS is set to
- * 0, or ipconfigUSE_DNS is set to 1 but a DNS server cannot be contacted. */
+/* Default gateway IP address configuration.  Used if ipconfigUSE_DHCP is set to
+ * 0, or ipconfigUSE_DHCP is set to 1 but a DHCP server cannot be contacted. */
 
 #define configGATEWAY_ADDR0    10
 #define configGATEWAY_ADDR1    211
 #define configGATEWAY_ADDR2    55
 #define configGATEWAY_ADDR3    1
 
 /* Default DNS server configuration.  OpenDNS addresses are 208.67.222.222 and
- * 208.67.220.220.  Used in ipconfigUSE_DNS is set to 0, or ipconfigUSE_DNS is set
- * to 1 but a DNS server cannot be contacted.*/
+ * 208.67.220.220.  Used if ipconfigUSE_DHCP is set to 0, or ipconfigUSE_DHCP is set
+ * to 1 but a DHCP server cannot be contacted.*/
 
 #define configDNS_SERVER_ADDR0    127
 #define configDNS_SERVER_ADDR1    0
 #define configDNS_SERVER_ADDR2    0
 #define configDNS_SERVER_ADDR3    53
 
-/* Default netmask configuration.  Used in ipconfigUSE_DNS is set to 0, or
- * ipconfigUSE_DNS is set to 1 but a DNS server cannot be contacted. */
+/* Default netmask configuration.  Used if ipconfigUSE_DHCP is set to 0, or
+ * ipconfigUSE_DHCP is set to 1 but a DHCP server cannot be contacted. */
 #define configNET_MASK0           255
 #define configNET_MASK1           255
 #define configNET_MASK2           255

diff --git a/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/Makefile b/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/Makefile
@@ -1,4 +1,5 @@
 CC = arm-none-eabi-gcc
+SIZE = arm-none-eabi-size
 BIN := freertos_tcp_mps2_demo.axf
 
 BUILD_DIR := build
@@ -29,7 +30,6 @@ INCLUDE_DIRS += -I$(KERNEL_DIR)/include
 SOURCE_FILES += $(KERNEL_DIR)/tasks.c
 SOURCE_FILES += $(KERNEL_DIR)/list.c
 SOURCE_FILES += $(KERNEL_DIR)/queue.c
-SOURCE_FILES += $(KERNEL_DIR)/timers.c
 SOURCE_FILES += $(KERNEL_DIR)/event_groups.c
 
 # FreeRTOS Kernel ARM Cortex-M3 Port
@@ -51,30 +51,33 @@ SOURCE_FILES += ${FREERTOS_TCP}/source/portable/BufferManagement/BufferAllocatio
 SOURCE_FILES += ${FREERTOS_TCP}/source/portable/NetworkInterface/MPS2_AN385/NetworkInterface.c
 SOURCE_FILES += ${FREERTOS_TCP}/source/portable/NetworkInterface/MPS2_AN385/ether_lan9118/smsc9220_eth_drv.c
 
-DEFINES := -DQEMU_SOC_MPS2 -DHEAP3
-
-LDFLAGS = -T mps2_m3.ld -specs=nano.specs --specs=rdimon.specs -lc -lrdimon
-LDFLAGS += -Xlinker -Map=${BUILD_DIR}/output.map
-
-CFLAGS += -nostartfiles -mthumb -mcpu=cortex-m3 -Wno-error=implicit-function-declaration
-CFLAGS += -Wno-builtin-declaration-mismatch -Werror
+DEFINES := -DHEAP3
+CPPFLAGS += $(DEFINES)
 
+CFLAGS += -mthumb -mcpu=cortex-m3
 ifeq ($(DEBUG), 1)
-    CFLAGS += -ggdb3 -Og
+    CFLAGS += -g3 -Og -ffunction-sections -fdata-sections
 else
-    CFLAGS += -O3
+    CFLAGS += -Os -ffunction-sections -fdata-sections
 endif
-    CFLAGS += -fstrict-aliasing -Wstrict-aliasing -Wno-error=address-of-packed-member
+CFLAGS += -MMD
+CFLAGS += -Wall -Wextra -Wshadow
+#CFLAGS += -Wpedantic -fanalyzer
+#CFLAGS += -flto
+CFLAGS += $(INCLUDE_DIRS)
 
-OBJ_FILES := $(SOURCE_FILES:%.c=$(BUILD_DIR)/%.o)
+LDFLAGS = -T mps2_m3.ld
+LDFLAGS += -Xlinker -Map=${BUILD_DIR}/output.map
+LDFLAGS += -Xlinker --gc-sections
+LDFLAGS += -nostartfiles -specs=nano.specs -specs=nosys.specs -specs=rdimon.specs
 
-CPPFLAGS += $(DEFINES)
-CFLAGS += $(INCLUDE_DIRS)
+OBJ_FILES := $(SOURCE_FILES:%.c=$(BUILD_DIR)/%.o)
 
 .PHONY: clean
 
 $(BUILD_DIR)/$(BIN) : $(OBJ_FILES)
-	$(CC) -ffunction-sections -fdata-sections $(CFLAGS) $(LDFLAGS) $+ -o $(@)
+	$(CC) $(CFLAGS) $(LDFLAGS) $+ -o $(@)
+	$(SIZE) $(@)
 
 %.d: %.c
 	@set -e; rm -f $@; \
@@ -87,7 +90,7 @@ INCLUDES := $(SOURCE_FILES:%.c=$(BUILD_DIR)/%.d)
 
 ${BUILD_DIR}/%.o : %.c Makefile
 	-mkdir -p $(@D)
-	$(CC)  $(CPPFLAGS) $(CFLAGS) -MMD -c $< -o $@
+	$(CC) $(CFLAGS) $(CPPFLAGS) -c $< -o $@
 
 clean:
 	-rm -rf build
diff --git a/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/TCPEchoClient_SingleTasks.c b/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/TCPEchoClient_SingleTasks.c
@@ -206,18 +206,18 @@
                     lStringLength = prvCreateTxData( pcTransmittedString, echoBUFFER_SIZES );
 
                     /* Add in some unique text at the front of the string. */
-                    sprintf( pcTransmittedString, "TxRx message number %u", ulTxCount );
+                    sprintf( pcTransmittedString, "TxRx message number %lu", ulTxCount );
                     ulTxCount++;
 
-                    printf( "sending data to the echo server size %d original %d\n",
+                    printf( "sending data to the echo server size %ld original %d\n",
                             lStringLength,
                             echoBUFFER_SIZES );
                     /* Send the string to the socket. */
                     lTransmitted = FreeRTOS_send( xSocket,                        /* The socket being sent to. */
                                                   ( void * ) pcTransmittedString, /* The data being sent. */
                                                   lStringLength,                  /* The length of the data being sent. */
                                                   0 );                            /* No flags. */
-                    printf( "FreeRTOS_send returned...transmitted %d\n",
+                    printf( "FreeRTOS_send returned...transmitted %ld\n",
                             lTransmitted );
 
                     if( lTransmitted < 0 )
@@ -398,15 +398,24 @@
         #if ( ipconfigIPv4_BACKWARD_COMPATIBLE == 1 )
             eDHCPCallbackAnswer_t xApplicationDHCPHook( eDHCPCallbackPhase_t eDHCPPhase,
                                                         uint32_t ulIPAddress )
+            {
+                ( void ) eDHCPPhase;
+                ( void ) ulIPAddress;
+
+                return eDHCPContinue;
+            }
         #else /* ( ipconfigIPv4_BACKWARD_COMPATIBLE == 1 ) */
             eDHCPCallbackAnswer_t xApplicationDHCPHook_Multi( eDHCPCallbackPhase_t eDHCPPhase,
                                                               struct xNetworkEndPoint * pxEndPoint,
                                                               IP_Address_t * pxIPAddress )
+            {
+                ( void ) eDHCPPhase;
+                ( void ) pxEndPoint;
+                ( void ) pxIPAddress;
+
+                return eDHCPContinue;
+            }
         #endif /* ( ipconfigIPv4_BACKWARD_COMPATIBLE == 1 ) */
-        {
-            /* Provide a stub for this function. */
-            return eDHCPContinue;
-        }
 
     #endif /* if ( ipconfigUSE_DHCP_HOOK != 0 )*/
 

diff --git a/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/main.c b/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/main.c
@@ -40,9 +40,7 @@ void main_tcp_echo_client_tasks( void );
 void vApplicationIdleHook( void );
 void vApplicationTickHook( void );
 
-extern void initialise_monitor_handles( void );
-
-int main()
+int main( void )
 {
     main_tcp_echo_client_tasks();
     return 0;
@@ -84,8 +82,6 @@ void vApplicationStackOverflowHook( TaskHandle_t pxTask,
 
 void vApplicationIdleHook( void )
 {
-    volatile size_t xFreeHeapSpace;
-
     /* This is just a trivial example of an idle hook.  It is called on each
      * cycle of the idle task.  It must *NOT* attempt to block.  In this case the
      * idle task just queries the amount of FreeRTOS heap that remains.  See the

diff --git a/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/main_networking.c b/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/main_networking.c
@@ -140,6 +140,7 @@ static UBaseType_t ulNextRand;
 
 void main_tcp_echo_client_tasks( void )
 {
+    BaseType_t xReturn;
     const uint32_t ulLongTime_ms = pdMS_TO_TICKS( 1000UL );
 
     /*
@@ -180,14 +181,13 @@ void main_tcp_echo_client_tasks( void )
         }
         #endif /* ( ipconfigUSE_DHCP != 0 ) */
 
-        memcpy( ipLOCAL_MAC_ADDRESS, ucMACAddress, sizeof( ucMACAddress ) );
-
-        FreeRTOS_IPInit_Multi();
+        xReturn = FreeRTOS_IPInit_Multi();
     #else /* if defined( ipconfigIPv4_BACKWARD_COMPATIBLE ) && ( ipconfigIPv4_BACKWARD_COMPATIBLE == 0 ) */
         /* Using the old /single /IPv4 library, or using backward compatible mode of the new /multi library. */
-        FreeRTOS_IPInit( ucIPAddress, ucNetMask, ucGatewayAddress, ucDNSServerAddress, ucMACAddress );
+        xReturn = FreeRTOS_IPInit( ucIPAddress, ucNetMask, ucGatewayAddress, ucDNSServerAddress, ucMACAddress );
     #endif /* defined( ipconfigIPv4_BACKWARD_COMPATIBLE ) && ( ipconfigIPv4_BACKWARD_COMPATIBLE == 0 ) */
 
+    configASSERT( xReturn == pdTRUE );
 
     /* Start the RTOS scheduler. */
     FreeRTOS_debug_printf( ( "vTaskStartScheduler\n" ) );
@@ -224,6 +224,10 @@ BaseType_t xTasksAlreadyCreated = pdFALSE;
     uint32_t ulDNSServerAddress;
     char cBuffer[ 16 ];
 
+    #if defined( ipconfigIPv4_BACKWARD_COMPATIBLE ) && ( ipconfigIPv4_BACKWARD_COMPATIBLE == 0 )
+        ( void ) pxEndPoint;
+    #endif /* defined( ipconfigIPv4_BACKWARD_COMPATIBLE ) && ( ipconfigIPv4_BACKWARD_COMPATIBLE == 0 ) */
+
     /* If the network has just come up...*/
     if( eNetworkEvent == eNetworkUp )
     {
@@ -335,6 +339,10 @@ static void prvMiscInitialisation( void )
     {
         BaseType_t xReturn;
 
+        #if defined( ipconfigIPv4_BACKWARD_COMPATIBLE ) && ( ipconfigIPv4_BACKWARD_COMPATIBLE == 0 )
+            ( void ) pxEndPoint;
+        #endif /* defined( ipconfigIPv4_BACKWARD_COMPATIBLE ) && ( ipconfigIPv4_BACKWARD_COMPATIBLE == 0 ) */
+
         /* Determine if a name lookup is for this node.  Two names are given
          * to this node: that returned by pcApplicationHostnameHook() and that set
          * by mainDEVICE_NICK_NAME. */

diff --git a/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/mps2_m3.ld b/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Echo_Qemu_mps2/mps2_m3.ld
@@ -128,7 +128,7 @@ SECTIONS
         _heap_top = .;
         . = . + _Min_Stack_Size;
         . = ALIGN(8);
-       } >RAM
+    } >RAM
 
    /* Set stack top to end of RAM, and stack limit move down by
     * size of stack_dummy section */
-Original file line number
+Diff line change
@@ Expand Up / @@ -724,6 +724,7 @@ CMock @@
     CNBTR
     CNDA
     CNDTR
+    CNOT
     CNTALOAD
     CNTAMAX
     CNTBLOAD
@@ Expand Down @@