Update to out of source makefile build and add run-cbmc-proofs.py
CBMC proofs can now be run with Litani with the command
"./run-cbmc-proofs.py"
Based on commits:
* 1646301 - Ignore CBMC proof failures, fail the build later (4 months ago) <Kareem Khazem>
* 7e8c91a - Fix Makefile prerequisite symbol for CBMC proofs (4 months ago) <Kareem Khazem>
* bee04be - Enable CBMC proofs to run in CI (4 months ago) <Kareem Khazem>
Found in https://github.com/FreeRTOS/FreeRTOS-Plus-TCP
It is recommended by the AWS IoT Jobs service to use DescribeJobExecution API for scaling purposes instead of StartNextPendingJobExecution API. Thus, update the Jobs demo to replace the latter API call with the former API call.
* Implement Kernel Unit Test Framework with CMock
* Add Readme.md to unit tests
* Add Posix build checker to git actions
* Add Ruby requirement
* Fix file header checks
* Fix header checks
* Add color output to test runs
* Clean up demo config for wolfSSL mutual auth.
* Add comment about picking the correct ROOT CA.
* uncrustify using_wolfSSL.c and some other code style changes.
* Apply suggestions from code review
Co-authored-by: Archit Aggarwal <architag@amazon.com>
FreeRTOS_send adds the packet to be sent to the IP task's queue for
later processing. The packet is sent later by the IP task. When
FreeRTOS is used in collaborative mode (i.e. configUSE_PREEMPTION is 0),
the Plaintext_FreeRTOS_send function returns without actually sending
the packet as the IP task never gets a chance to run.
The fact that Plaintext_FreeRTOS_send returns without actually sending
the packet causes an issue in the MQTT_Connect which expects the CONNECT
packet to be actually sent and waits for CONNACK.
This commit adds a taskYIELD call after calling FreeRTOS_send to ensure
that the IP task gets a chance to run and send the packet before the
Plaintext_FreeRTOS_send function returns.
* Add Posix build checker to git actions
* fix checker path
* Fix script, checkout recursively
* fix build check script return value
* clone submodules as well with posix checker
* Add quotes to true for submodules
* Fix Submodules
* Remove pcap dependency from Makefile
* install libpcap for build check
* Add networking build to posix
* Separate network build from normal build
* add libpcap after building normal posix
* Initial version where all deps are pylibs
* mechanism for undoing an autorelease
* misc refactor touchups
* +mechanism to baseline older commit into detached HEAD tag
* decouple kernel check configs + misc refactor improvements
* improved compatibility with git action
* Get pushes working in git action with release
* Fix header-check issue when same deletion occurs in parallel
* Add help message in case check fails
* Address PR feedback
* Add Full Demo to Qemu with MPS2
* Increase full demo heap memory
* Add Full Demo to Qemu MPS2
* Fix headers
* Fix header FreeRTOS version
* Remove commented line
* Remove commented line
* Fix header checker version, and corresponding files
* Fix checker version number requirements
* Fix build failure in STM32 Discovery MPU Projects
Privileged data region size needs to be increased because heap is now
placed in this region.
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
Add URL file links to the MQTT agent documentation page.
Add comment blocks into each demo that also point toward the MQTT agent documentation to ensure users are aware the agent method exists.
* Set mbedtls submodule tag to v2.24.0
* Update projects
Co-authored-by: Oscar Michael Abrina <abrinao@amazon.com>
Co-authored-by: Cobus van Eeden <35851496+cobusve@users.noreply.github.com>
From the FreeRTOS documentation, pdFREERTOS_ERRNO_ENOSPC means that timeout occurred before any data could be sent or received.
- In the plaintext transport-interface implementation, we would directly return `-pdFREERTOS_ERRNO_ENOSPC`. However, an error like this can occur when the TCP buffer is full, so this ought to be retriable. Libraries that consume the transport interface interpret a return value of 0 to mean that send/recv can be invoked again to get the data. As such, we should appropriately set the return value as 0 when the status is `-pdFREERTOS_ERRNO_ENOSPC`.
- In the mbedTLS port, we would directly return whatever `FreeRTOS_send` or `FreeRTOS_recv` returns. However, sometimes, the return value can be an error. In such cases, we ought to map an error from FreeRTOS+TCP to an equivalent error in mbedTLS. In the case of `-pdFREERTOS_ERRNO_ENOSPC`, we map that to `MBEDTLS_ERR_SSL_TIMEOUT`. When the mbedTLS transport-interface send/recv wrapper sees that value, it appropriately returns 0, so that the library can retry the send/recv. I've verified that when the mbedTLS port returns an error, that same error is returned by `mbedtls_ssl_write` & `mbedtls_ssl_read`.
- The TCP socket may have a receive block time. If bytesToRecv is greater than 1 then a frame is likely already part way through reception and blocking to wait for the desired number of bytes to be available is the
most efficient thing to do. If bytesToRecv is 1 then this may be a speculative call to read to find the start of a new frame, in which case blocking is not desirable as it could block an entire protocol agent task for the duration of the read block time and therefore negatively impact performance. So if bytesToRecv is 1 then don't call recv unless it is known that bytes are already available.
Co-authored-by: abhidixi11 <44424462+abhidixi11@users.noreply.github.com>
Co-authored-by: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Carl Lundin
alfred gedeon
Cobus van Eeden
Archit Aggarwal
David Chalco
TakayukiMatsuo
Marc-Antoine Lalonde
alfred gedeon
Joseph Julicher
Carl Lundin
Sukhmani Minhas
Archit Gupta
Oscar Michael Abrina
Gaurav-Aggarwal-AWS
RichardBarry
Ming Yue