diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h')
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h | 237 |
1 files changed, 237 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h new file mode 100644 index 000000000..28de2bd15 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h @@ -0,0 +1,237 @@ +/* + * FreeRTOS Kernel V10.0.1 + * Copyright (C) 2017 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +#ifndef FREERTOS_CONFIG_H +#define FREERTOS_CONFIG_H + +/*----------------------------------------------------------- +* Application specific definitions. +* +* These definitions should be adjusted for your particular hardware and +* application requirements. +* +* THESE PARAMETERS ARE DESCRIBED WITHIN THE 'CONFIGURATION' SECTION OF THE +* FreeRTOS API DOCUMENTATION AVAILABLE ON THE FreeRTOS.org WEB SITE. +* http://www.freertos.org/a00110.html +* +* The bottom of this file contains some constants specific to running the UDP +* stack in this demo. Constants specific to FreeRTOS+TCP itself (rather than +* the demo) are contained in FreeRTOSIPConfig.h. +*----------------------------------------------------------*/ +#define configENABLE_BACKWARD_COMPATIBILITY 1 +#define configUSE_PREEMPTION 1 +#define configUSE_PORT_OPTIMISED_TASK_SELECTION 1 +#define configMAX_PRIORITIES ( 7 ) +#define configTICK_RATE_HZ ( 1000 ) /* In this non-real time simulated environment the tick frequency has to be at least a multiple of the Win32 tick frequency, and therefore very slow. */ +#define configMINIMAL_STACK_SIZE ( ( unsigned short ) 60 ) /* In this simulated case, the stack only has to hold one small structure as the real stack is part of the Win32 thread. */ +#define configTOTAL_HEAP_SIZE ( ( size_t ) ( 2048U * 1024U ) ) +#define configMAX_TASK_NAME_LEN ( 15 ) +#define configUSE_16_BIT_TICKS 0 +#define configIDLE_SHOULD_YIELD 1 +#define configUSE_CO_ROUTINES 0 +#ifndef configUSE_MUTEXES + #define configUSE_MUTEXES 1 +#endif +#ifndef configUSE_RECURSIVE_MUTEXES + #define configUSE_RECURSIVE_MUTEXES 1 +#endif +#define configQUEUE_REGISTRY_SIZE 0 +#define configUSE_APPLICATION_TASK_TAG 1 +#define configUSE_COUNTING_SEMAPHORES 1 +#define configUSE_ALTERNATIVE_API 0 +#define configNUM_THREAD_LOCAL_STORAGE_POINTERS 3 /* FreeRTOS+FAT requires 2 pointers if a CWD is supported. */ +#define configRECORD_STACK_HIGH_ADDRESS 1 + +/* Hook function related definitions. */ +#ifndef configUSE_TICK_HOOK + #define configUSE_TICK_HOOK 0 +#endif +#define configUSE_IDLE_HOOK 1 +#define configUSE_MALLOC_FAILED_HOOK 1 +#define configCHECK_FOR_STACK_OVERFLOW 0 /* Not applicable to the Win32 port. */ + +/* Software timer related definitions. */ +#define configUSE_TIMERS 1 +#define configTIMER_TASK_PRIORITY ( configMAX_PRIORITIES - 1 ) +#define configTIMER_QUEUE_LENGTH 5 +#define configTIMER_TASK_STACK_DEPTH ( configMINIMAL_STACK_SIZE * 2 ) + +/* Event group related definitions. */ +#define configUSE_EVENT_GROUPS 1 + +/* Co-routine definitions. */ +#define configUSE_CO_ROUTINES 0 +#define configMAX_CO_ROUTINE_PRIORITIES ( 2 ) + +/* Memory allocation strategy. */ +#ifndef configSUPPORT_DYNAMIC_ALLOCATION + #define configSUPPORT_DYNAMIC_ALLOCATION 1 +#endif +#ifndef configSUPPORT_STATIC_ALLOCATION + #define configSUPPORT_STATIC_ALLOCATION 1 +#endif + + +/* Set the following definitions to 1 to include the API function, or zero + * to exclude the API function. */ +#define INCLUDE_vTaskPrioritySet 1 +#define INCLUDE_uxTaskPriorityGet 1 +#define INCLUDE_vTaskDelete 1 +#define INCLUDE_vTaskCleanUpResources 0 +#ifndef INCLUDE_vTaskSuspend + #define INCLUDE_vTaskSuspend 1 +#endif +#define INCLUDE_vTaskDelayUntil 1 +#define INCLUDE_vTaskDelay 1 +#define INCLUDE_uxTaskGetStackHighWaterMark 1 +#ifndef INCLUDE_xTaskGetSchedulerState + #define INCLUDE_xTaskGetSchedulerState 1 +#endif +#define INCLUDE_xTimerGetTimerTaskHandle 0 +#define INCLUDE_xTaskGetIdleTaskHandle 0 +#define INCLUDE_xQueueGetMutexHolder 1 +#define INCLUDE_eTaskGetState 1 +#define INCLUDE_xEventGroupSetBitsFromISR 1 +#define INCLUDE_xTimerPendFunctionCall 1 +#define INCLUDE_xTaskGetCurrentTaskHandle 1 +#define INCLUDE_xTaskAbortDelay 1 + +/* This demo makes use of one or more example stats formatting functions. These + * format the raw data provided by the uxTaskGetSystemState() function in to human + * readable ASCII form. See the notes in the implementation of vTaskList() within + * FreeRTOS/Source/tasks.c for limitations. configUSE_STATS_FORMATTING_FUNCTIONS + * is set to 2 so the formatting functions are included without the stdio.h being + * included in tasks.c. That is because this project defines its own sprintf() + * functions. */ +#define configUSE_STATS_FORMATTING_FUNCTIONS 1 + +/* Assert call defined for debug builds. */ +extern void vAssertCalled( const char * pcFile, + uint32_t ulLine ); +#ifndef configASSERT +#define configASSERT( x ) if( ( x ) == 0 ) vAssertCalled( __FILE__, __LINE__ ) +#endif + +/* Remove logging in formal verification */ +#define configPRINTF( X ) + +/* Non-format version thread-safe print. */ +#define configPRINT_STRING( X ) + +/* Application specific definitions follow. **********************************/ + +/* If configINCLUDE_DEMO_DEBUG_STATS is set to one, then a few basic IP trace + * macros are defined to gather some UDP stack statistics that can then be viewed + * through the CLI interface. */ +#define configINCLUDE_DEMO_DEBUG_STATS 1 + +/* The size of the global output buffer that is available for use when there + * are multiple command interpreters running at once (for example, one on a UART + * and one on TCP/IP). This is done to prevent an output buffer being defined by + * each implementation - which would waste RAM. In this case, there is only one + * command interpreter running, and it has its own local output buffer, so the + * global buffer is just set to be one byte long as it is not used and should not + * take up unnecessary RAM. */ +#define configCOMMAND_INT_MAX_OUTPUT_SIZE 1 + +/* Only used when running in the FreeRTOS Windows simulator. Defines the + * priority of the task used to simulate Ethernet interrupts. */ +#define configMAC_ISR_SIMULATOR_PRIORITY ( configMAX_PRIORITIES - 1 ) + +/* This demo creates a virtual network connection by accessing the raw Ethernet + * or WiFi data to and from a real network connection. Many computers have more + * than one real network port, and configNETWORK_INTERFACE_TO_USE is used to tell + * the demo which real port should be used to create the virtual port. The ports + * available are displayed on the console when the application is executed. For + * example, on my development laptop setting configNETWORK_INTERFACE_TO_USE to 4 + * results in the wired network being used, while setting + * configNETWORK_INTERFACE_TO_USE to 2 results in the wireless network being + * used. */ +#define configNETWORK_INTERFACE_TO_USE ( 0L ) + +/* The address of an echo server that will be used by the two demo echo client + * tasks: + * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Echo_Clients.html, + * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/UDP_Echo_Clients.html. */ +#define configECHO_SERVER_ADDR0 192 +#define configECHO_SERVER_ADDR1 168 +#define configECHO_SERVER_ADDR2 2 +#define configECHO_SERVER_ADDR3 6 +#define configTCP_ECHO_CLIENT_PORT 7 + +/* Default MAC address configuration. The demo creates a virtual network + * connection that uses this MAC address by accessing the raw Ethernet/WiFi data + * to and from a real network connection on the host PC. See the + * configNETWORK_INTERFACE_TO_USE definition above for information on how to + * configure the real network connection to use. */ +#define configMAC_ADDR0 0x00 +#define configMAC_ADDR1 0x11 +#define configMAC_ADDR2 0x22 +#define configMAC_ADDR3 0x33 +#define configMAC_ADDR4 0x44 +#define configMAC_ADDR5 0x21 + +/* Default IP address configuration. Used in ipconfigUSE_DHCP is set to 0, or + * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configIP_ADDR0 192 +#define configIP_ADDR1 168 +#define configIP_ADDR2 0 +#define configIP_ADDR3 105 + +/* Default gateway IP address configuration. Used in ipconfigUSE_DHCP is set to + * 0, or ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configGATEWAY_ADDR0 192 +#define configGATEWAY_ADDR1 168 +#define configGATEWAY_ADDR2 0 +#define configGATEWAY_ADDR3 1 + +/* Default DNS server configuration. OpenDNS addresses are 208.67.222.222 and + * 208.67.220.220. Used in ipconfigUSE_DHCP is set to 0, or ipconfigUSE_DHCP is + * set to 1 but a DNS server cannot be contacted.*/ +#define configDNS_SERVER_ADDR0 208 +#define configDNS_SERVER_ADDR1 67 +#define configDNS_SERVER_ADDR2 222 +#define configDNS_SERVER_ADDR3 222 + +/* Default netmask configuration. Used in ipconfigUSE_DHCP is set to 0, or + * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configNET_MASK0 255 +#define configNET_MASK1 255 +#define configNET_MASK2 255 +#define configNET_MASK3 0 + +/* The UDP port to which print messages are sent. */ +#define configPRINT_PORT ( 15000 ) + +#define configPROFILING ( 0 ) + +/* Pseudo random number generater used by some demo tasks. */ +extern uint32_t ulRand(); +#define configRAND32() ulRand() + +/* The platform that FreeRTOS is running on. */ +#define configPLATFORM_NAME "WinSim" + +#endif /* FREERTOS_CONFIG_H */ |