- Update core_mqtt_config.h to specify logging level as LOG_NONE
- Update GA to set logging level as LOG_DEBUG
- Fix compile error in LogDebug of recvExact
### Problem
The `MQTT_ProcessLoop` and `MQTT_ReceiveLoop` read incoming MQTT packet payload over the network by calling the `recvExact` function. The `recvExact` function can be called multiple times to read the expected number of bytes for the MQTT packet but it also implements a timeout functionality of receiving the expected number of payload within the timeout value passed to the function.
This causes problems when the `Transport_Recv` call returns less than requested number of bytes, and there is a timeout (for example, when calling `MQTT_ProcessLoop` with 0ms duration) which causes the function to assume failure instead of reading the remaining payload of the MQTT packet by calling `Transport_Recv` again. Thus, in such cases, the MQTT connection is severed prematurely even though there is a high probability of receiving the remaining bytes of the MQTT packet over the network.
### Solution
Instead of implementing a timeout on the entire duration of receiving the expected number of remaining MQTT packet bytes in `recvExact`, the use of timeout is being changed to be relevant only on the total time of receiving 0 bytes over the network over multiple calls to `Transport_Recv`.
As this modified meaning of the timeout duration is now unrelated to the timeout duration that the `MQTT_ProcessLoop` or `MQTT_ReceiveLoop` functions are called, a new configuration constant for the `recvExact` timeout value, `MQTT_RECV_POLLING_TIMEOUT_MS`, has been added to the library which will carry a default value of 10ms.
Co-authored-by: Sarena Meas <sarem@amazon.com>
This follows changes from FreeRTOS/FreeRTOS@398abba. The const qualifier is removed from send/recv because there are transport implementations that require a member of the network context to be modified such as in the case of mbedtls.
Removed MQTT_INCLUDE_PRIVATE_DIRS from the CMake config files
because there are no header files in there and files in that directory are
not referenced in any #include in any library source, tests, or demos.
This commit updates the template starter kit and modifies the proofs and
Makefiles so that they conform to the latest standard. In particular,
this PR introduces the PROOF_UID variable to give each proof a unique
name.
This commit adds some comments that explain how the run-cbmc-proofs.py
script diverges from similar scripts that we use for other projects. The
comments begin with "# PROJECT SPECIFIC".
This commit makes Litani run make with the EXTERNAL_SAT_SOLVER variable
set. The template Makefile uses the value of this variable to determine
which external SAT solver CBMC should call out to. We're using Kissat
because the default SAT solver takes too long on two of the proofs,
MQTT_SerializeConnect and MQTT_Connect.
* Set publish payload to NULL when zero length
* Add unit test for zero length payload
* Fix unit tests for deserialize publish
* Rename setupWillInfo to setupPublishInfo
* Remove void * from memset
* Add version numbers
* Add missing @file tags
* Update lexicon.txt
* Update @brief tag for MQTT cbmc state
Co-authored-by: Gary Wicker <14828980+gkwicker@users.noreply.github.com>
* Add license where needed in the test files.
* Remove default configs from the test core_mqtt_config.h.
Co-authored-by: SarenaAWS <6563840+sarenameas@users.noreply.github.com>
* Update CMake infrastructure for repository to be self-sufficient for building targets
* Update GitHub CI workflow to only use build infrastructure of the repository
