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>
* 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
* 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.
---------
* Add in a comment of the step name on the Install Dependencies job step to create a nicer log on github
* See if we can use the owner of the repo as the check for if the CBMC proofs should run
* Allow manually running the CBMC proofs
---------
Co-authored-by: Rahul Kar <118818625+kar-rahul-aws@users.noreply.github.com>
Add x64 configuration to Win32-MSVC demo.
This was originally contributed in this PR - #1139
---------
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
Co-authored-by: José Simões <jose.simoes@eclo.solutions>
Co-authored-by: Rahul Kar <118818625+kar-rahul-aws@users.noreply.github.com>
* Bump up to MBed-TLS V3.5.1, make changes to Visual Studio Projects to account for this.
* Update MBedTLS Transport files to call psa_crypto_init() if the MBEDTLS_PSA_CRYPTO_C is set.
* Add WIN32_LEAN_AND_MEAN to the corePKCS11_MQTT_Mutual_Auth_Windows_Simulator demo. Add in a check for MBEDTLS_ERR_SSL_RECEIVED_NEW_SESSION_TICKET when making a TLS handshake.
* Change transport interface files from using void * to mbedtls_pk_context * instead per changes in the MbedTLS API.
* Changes to Fleet Provisioning Demo and Demo Setup to use ECDSA keys
* Remove non-32 bit configs from various VisualStudio Projects. Enforce all projects using WIN32_LEAN_AND_MEAN as well as winsock2.h
This PR updates FreeRTOS-Plus-Trace to a submodule pointer and
updates the relevant project files. Percepio recommends to use
streaming to ring buffer on a 64-bit system instead of snapshot
and therefore, POSIX demo is updated to use streaming to ring
buffer.
* Use new version of CI-CD Actions, checkout@v3 instead of checkout@v2 on all jobs
* Use cSpell spell check, and use ubuntu-20.04 for formatting check
* Add in bot formatting action
* Update freertos_demo.yml and freertos_plus_demo.yml files to increase github log readability
* Add in a Qemu demo onto the workflows.
The WolfSSL-FIPS-Ready distribution is licensed under the GPLv3 or
a commercial license. Only MIT licensed code is allowed in this
repository. Refer to the FreeRTOS_Plus_WolfSSL_Windows_Simulator Demo
for future WolfSSL integrations.
Enable Werror for Posix Demo Coverage Test target
Werror cannot be enabled for the non coverage test because tracelyzer
code generates warnings in that target.
Also add "Build Posix_GCC Demo for Coverage Test" in the PR checks to
catch warnings from kernel code in PR checks.
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
* Add libslirp to the existing FreeRTOS+TCP static project
* Update demos to run with libslirp
* Add ipconfigUSE_LIBSLIRP
* Call developer command prompt and update meson build options
---------
Co-authored-by: Xiaodong Li <xiaodonn@amazon.com>
* Changing uncrustify to print out git difference after fixing
* Updating workflow for freertos_demos to use echo groups, updating ci.yml formatting
---------
* Update freertos-plus-tcp-echo-posix git workflow to include echo server setup with port 5000, update Ubuntu runner version to 22.04, install glib and libslirp, and add git run action with TRACE_ON_ENTER=0 which disables trace output saved msg
* Update ipconfigNETWORK_MTU to 1500, ipconfigBUFFER_PADDING on 64-bit platforms, and FreeRTOS-Plus-TCP submodule libslirp version number in backend file
* Format code, update lexicon.txt and create ReadMe
---------
Co-authored-by: Xiaodong Li <xiaodonn@amazon.com>
* test full demo
* Revert "test full demo"
This reverts commit 09efa00ec0.
revert back to origin
* pre-define user demo to blinky demo
* pre-define user demo to blinky demo with -j
* test run win32-msvc demo
* test run win32-msvc demo
* test run win32-msvc demo
* update git workflow to run WIN32-MSVC demo
* update git workflow to run WIN32-MSVC demo
* update git workflow to run WIN32-MSVC demo
* update git workflow to run WIN32-MSVC demo
* update git workflow to run WIN32-MSVC demo
* update git workflow to run WIN32-MSVC demo
* update git workflow to run WIN32-MSVC demo
* update trigger action
* build and run WIN32-MSVC blinky demo
* build and run WIN32-MSVC blinky demo
* build and run WIN32-MSVC blinky demo
* update WIN32-MSVC workflow
* update WIN32-MSVC Demo main.c file to remove buffer
* Update main.c files to remove buffer when running executable_monitor file for Git Action
* update formatting for WIN32-MSVC demos
* update formatting for Posix demo
* update comment for setvbuf function used in main.c
* add git build and run action for WIN32-MingW Full and Blinky demos; update main.c file to set buffer size as 0
* add git build and run action for WIN32-MingW Full and Blinky demos; update main.c file to set buffer size as 0
* remove whitespace for freertos_demos.yml file
* add function to Force stdout to write immediately by setting the buffer size for it to 0 in demo main.c file when running git Run Action; Correct formatting error for WIN32-MingW main.c file
* add function to Force stdout to write immediately by setting the buffer size for it to 0 in demo main.c file when running git Run Action
* update git run action commands for Posix_GCC demo
* update git run action commands for Posix_GCC demo
* update git run action commands for Posix_GCC demo
* reduce timeout and correct formatting issue
* reduce timeout
---------
Co-authored-by: Xiaodong Li <xiaodonn@amazon.com>
* Undo syntax changes preventing VeriFast parsing
* Update proofs inline with source changes
Outstanding:
- xQueueGenericReset return code
- Not using prvIncrementQueueTxLock or prvIncrementQueueRxLock macros
* Remove git hash check
* Document new changes between proven code and implementation
* Update copyright header
* VeriFast proofs: turn off uncrustify checks
Uncrustify requires formatting of comments that is at odds with VeriFast's
proof annotations, which are contained within comments.
* Update ci.yml
Co-authored-by: Joseph Julicher <jjulicher@mac.com>
Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
As the manifest verification script has been moved to FreeRTOS/CI-CD-Github-Actions as a GitHub Action along with the added functionality of verifying that manifest.yml versions match the current submoduled pointers in the repository, this PR updates the CI check for manifest verification to take advantage of the new manifest-verifier action from the repository.
To validate that the FreeRTOS/CI-CD-Github-Actions/memory_statistics/paths.json configuration is correct, this PR adds a CI check mechanism to generate the memory statistics report in JSON format. Additionally, the CI check also uploads the report as an artifact (for main and release-candidate branches ONLY) for user accessibility of the generated report.
* Added spell check
* All words
* Add a missing word
* Fix header checks
* Fix header checks v1
* Fix header check v2
* Updated freertos link in header
* Fixed afr link in the header
* Fix last of header checks
* Update the spell check script to check amazon licensed files only
* Fixed paths and added comments
* Try with modified repo
* Add inplace substitute option to sed
* Use official repo as the spell checker source
* Add vendor file to the ignored list
Co-authored-by: root <root@ip-172-31-5-28.us-west-2.compute.internal>
Rohit Madan
Monika Singh
Michael Tautschnig
Tony Josi
Soren Ptak
Gaurav-Aggarwal-AWS
Anubhav Rawal
kar-rahul-aws
Paul Bartell
ActoryOu
Xiaodong Li
chinglee-iot
xuelix
Kareem Khazem
alfred gedeon
jasonpcarroll
Soren Ptak
Kody Stribrny
Nathan Chong
Paul Bartell
swaldhoer
Archit Aggarwal
Aniruddha Kanhere