The upcoming CBMC version 6 release includes changes that may affect
existing proofs. This PR will make sure that FreeRTOS PRs are not
negatively impacted by this release. After releasing CBMC version 6 we
will issue a follow-up PR that will return FreeRTOS to using CBMC's
latest release, and will include any changes to proofs that may be
necessary to support the new version.
Co-authored-by: Rahul Kar <118818625+kar-rahul-aws@users.noreply.github.com>
Co-authored-by: Nikhil Kamath <110539926+amazonKamath@users.noreply.github.com>
From CORTEX_MPU_M3_MPS2_QEMU_GCC remove unused configNUM_TX_DESCRIPTORS
define and remove HEAP3 from as heap_4.c is used.
Signed-off-by: Florian La Roche <Florian.LaRoche@gmail.com>
Co-authored-by: Rahul Kar <118818625+kar-rahul-aws@users.noreply.github.com>
Posix_GCC: update compiler options
1. Add to CFLAGS
- add -O0 optimization for debug builds.
- add -O3 optimization for release builds.
2. Update signal handler `handle_sigint()` to use
`_exit()` instead of `exit()`. Normal exit() is not allowed
within a signal handler.
Signed-off-by: Florian La Roche <Florian.LaRoche@gmail.com>
For Demo/CORTEX_MPS2_QEMU_IAR_GCC gcc Makefile:
- simplify IMAGE var to already include full path
- clean target also removes mapfile
Signed-off-by: Florian La Roche <Florian.LaRoche@gmail.com>
Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
In FreeRTOS/Demo/CORTEX_MPU_M3_MPS2_QEMU_GCC/syscall.c the
extern definition of g_ulBase ist not used, so remove it.
Also move _heap_bottom and _heap_top to where they are used
in syscall.c.
Signed-off-by: Florian La Roche <Florian.LaRoche@gmail.com>
* Rename .\FreeRTOS-Plus\Demo\AWS\Fleet_Provisioning_Windows_Simulator\Fleet_Provisioning_With_CSR_Demo\ to .\FreeRTOS-Plus\Demo\AWS\Fleet_Provisioning_Windows_Simulator\CSR_Demo\ to reduce path length limit on Windows (260)
* Fix warnings in fleet provisioning demo
* Update path in CI actions script
* Fix formatting
Optimize _sbrk() from runtime to compiletime initialization.
Fix compiler warnings by adjusting (void *) and (char *) types.
Complete function declarations for uart_init() and _getpid().
Signed-off-by: Florian La Roche <Florian.LaRoche@gmail.com>
Co-authored-by: Rahul Kar <118818625+kar-rahul-aws@users.noreply.github.com>
Demo/Posix_GCC cleanup
- Guard prvSaveTraceFile() function definition.
- Remove "cid" as it is unused.
- handle_sigint(): quiet compiler warning about unused param.
- main_full.c: prvCheckTask(): Remove unused var "xHeapStats".
Signed-off-by: Florian La Roche <Florian.LaRoche@gmail.com>
* Exclude unnecessary directories from build.
1. "FreeRTOS/Source/example"
2. "FreeRTOS+Trace Recorder/extras"
3. "FreeRTOS+Trace Recorder/kernelports/BareMetal"
4. "FreeRTOS+Trace Recorder/kernelports/ESP-IDF_FreeRTOS"
5. "FreeRTOS+Trace Recorder/kernelports/ThreadX"
6. "FreeRTOS+Trace Recorder/kernelports/Zephyr"
1 is applied to both of "Debug" configuration and "Debug_CodeCoverage" configuration.
Others are applied to only "Debug" configuration because those directories are already excluded from build on "Debug_Coverage" configuration.
* Include path setting is modified.
1.Directory name is modified.("Include" -> "include")
2.New path is added.(FreeRTOS+Trace Recorder/kernelports/FreeRTOS/include)
These modifications are needed to build "Debug" configuration. They are not needed for "Debug_CodeCoverage" configuration because these paths are not used. But these modifications are applied to both of "Debug" configuration and "Debug_CodeCoverage" configuration because of future potential risk.
* [WIN32-MingW Demo] Replace "Exclude from Build" by "Resource Filter".
"Resource Filter" is better than "Exclude from Build" because "Resource Filter" makes excluded directories invisible on Eclipse GUI. But some directories are still "Exclude from Build" because they should be excluded only on "Debug_CodeCoverage" configuration. "Resource Filter" cannot be specified to each configuration separately.
* Code review suggestions
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
---------
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
Co-authored-by: Rahul Kar <118818625+kar-rahul-aws@users.noreply.github.com>
Co-authored-by: Gaurav Aggarwal <aggarg@amazon.com>
* [RISC-V-Qemu-virt_GCC Demo] Add picolibc support
Add minimal picolibc support:
* Use --specs=picolibc.specs to direct gcc at picolibc
* Use -DPICOLIBC_INTEGER_PRINTF_SCANF to enable smaller printf implementation
* Enable configUSE_PICOLIBC_TLS for thread local storage
* Add TLS section to linker script
Signed-off-by: Keith Packard <keithpac@amazon.com>
* [CORTEX_MPU_M3_MPS2_QEMU_GCC Demo] Add picolibc support
Add minimal picolibc support to this demo
* Use --specs=picolibc.specs to direct gcc at picolibc
* Use -DPICOLIBC_INTEGER_PRINTF_SCANF to enable smaller printf implementation
* Enable configUSE_PICOLIBC_TLS for thread local storage
* Add TLS section to linker script
* Replace newlib syscall hooks with picolibc ones
Signed-off-by: Keith Packard <keithpac@amazon.com>
---------
Signed-off-by: Keith Packard <keithpac@amazon.com>
Co-authored-by: Keith Packard <keithpac@amazon.com>
* [WIN32-MSVC Demo] Add tick type width definition based on the target platform.(32bit/64bit)
32bit TickType_t is used on Win32 target. 64bit TickType_t is used on x64 target.
Reason of change: Before this change, 32bit TickType_t is always used in MSVC demo. It is inefficient for 64bit target. In addition, compiler reported warnings for the cast operation between TickType_t and (void *) pointer if the target is x64 because of different width. 64bit TickType_t should be used instead of 32bit if target is 64bit.
* [WIN32-MSVC Demo] Change type of some variables from uint32_t to UBaseType_t.
Reason of change: These variables are cast to/from pointer type in existing codes. x64 compiler reports warnings for the cast operations between uint32_t and pointer type. UBaseType_t solves those warnings because it has same width as pointer type on both of Win32 platform and x64 platform.
* [WIN32-MSVC Demo]Correct prefix of variables and indent to follow coding style guide.
* [WIN32-MSVC Demo]Correct type of the argument in vApplicationGetIdleTaskMemory() prototype declaration.
It is corrected to match original declaration described in task.h.
* [WIN32-MSVC] Add cast operation to solve compiler warnings on x64 platform.
Before this change, compiler claimed that the cast operation to wider type should be applied before other arithmetic operations because of overflow risk. There is no overflow risk here but it is modified to solve compiler warnings.
* [WIN32-MingW Demo] Add tick type width definition based on compiler type.(32bit/64bit)
32bit TickType_t is used if compiler is MinGW32. 64bit TickType_t is used if compiler is MinGW64.
Reason of change: Before this change, 32bit TickType_t is always used in MinGW demo. It is inefficient for 64bit compiler. In addition, MinGW64 reported warnings for the cast operation between TickType_t and (void *) pointer because of different width. 64bit TickType_t should be used instead of 32bit if compiler is 64bit.
* [WIN32-MingW Demo] Change printf() format specifiers from %u to %llu.
Reason of change: %u specifier corrupts 64bit tick count because it supports only 32bit value. %llu can be used for both of 64bit value and 32bit value.(After casting to 64bit)
* [WIN32-MingW Demo] Change type of some variables from uint32_t to UBaseType_t.
Reason of change: These variables are cast to/from pointer type in existing codes. 64bit compiler(MinGW64) reports warnings for the cast operations between uint32_t and pointer type. UBaseType_t solves those warnings because it has same width as pointer type on both of MinGW32 and MinGW64.
* [WIN32-MingW Demo] Change type of some variables from uint32_t to UBaseType_t.
Same change as previous commit is applied to source codes which are built only on Debug configuration.
* [WIN32-MingW Demo] Add brackets to the condition in #if statement. Behavior is not changed. Reason of change is to follow coding style guide of FreeRTOS.
* Update "FreeRTOS/Source" submodule(FreeRTOS-kernel) to #1008.
* [WIN32-MingW Demo] Change type of one more variable from uint32_t to UBaseType_t.
Additional modification for solving compiler warnings for the cast operation on MinGW64.
* Update FreeRTOS-kernel submodule version in manifest.yml.
* Modify prefix of variables to follow coding style guide.
* Code review suggestions
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
---------
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
Co-authored-by: ActoryOu <ousc@amazon.com>
Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
Co-authored-by: Gaurav Aggarwal <aggarg@amazon.com>
* Add in a Cortex R5F MPU demo for the Hercules RM57 Development Kit.
* Add in a Cortex R4F MPU demo for the Hercules RM46 Development Kit.
* Provide a Code Composer Studio (CCS) project for running these demos.
* Provide a CMakeLists.txt file to allow for compilation of the demos without use of an IDE.
* Add a CI-CD build of these demos using CMake with Fetch-Content.
* Include necessary README to explain the new demos.
---------
Monika Singh
chinglee-iot
Rahul Kar
Gaurav-Aggarwal-AWS
Michael Tautschnig
Niklas
Florian La Roche
Tony Josi
xuelix
wat
Keith Packard
Soren Ptak
ActoryOu