for (full) in projects: CoreMQTT-Agent-v1.1.0

Project(s)

Full Search
Definition
Symbol
File Path
History
Type

Searched full:for (Results 1 – 25 of 106) sorted by relevance

12 3 4 5

/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgent_CommandLoop/
H D	Makefile	7 # This should be a unique identifier for this proof, and will appear on the 13 # for proving the memory safety and making the proofs run faster. 16 # Bound for loop unwinding for the loops trying to read and write into the 19 # array size for the proofs. 22 # Bound for loop unwinding for the main loop in MQTTAgent_CommandLoop. Unwinding 23 # the loop 3 times will be enough for proving memory safety. 26 # Bound for loop unwinding for loop in processCommand function. Unwinding 27 # the loop 2 times will be enough for proving memory safety.
H D	README.md	4 This directory contains a memory safety proof for MQTTAgent_CommandLoop. 15 For this proof, stubs are used for the implementation of functions in the following interfaces and 16 function types. Since the implementation for these functions will be provided by the applications, 24 …In addition to the interfaces and the function types, stubs are used for the below listed function… 25 CBMC proofs are written for these functions separately. 48 * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proo… 49 * Use Makefile.arpa as the starting point for your proof Makefile by:
/CoreMQTT-Agent-v1.1.0/test/unit-test/config/
H D	core_mqtt_config.h	17 * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR 18 * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER 25 * @brief This represents the default values for the configuration macros 26 * for the MQTT library. 28 * @note This file SHOULD NOT be modified. If custom values are needed for 38 /* The macro definition for MQTT_DO_NOT_USE_CUSTOM_CONFIG is for Doxygen 57 * acknowledgment at a time, that are supported for incoming and outgoing 64 * context maintains, separately, for both incoming and outgoing direction of 67 * @note The MQTT context maintains separate state records for outgoing 69 * of memory is statically allocated for the state records. [all …]
/CoreMQTT-Agent-v1.1.0/test/cbmc/include/
H D	core_mqtt_config.h	17 * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR 18 * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER 25 * @brief This header sets configuration macros for the MQTT library. 30 /* Mock a network context for the CBMC proofs. / 38 acknowledgement at a time, that are supported for incoming and outgoing 45 * context maintains, separately, for both incoming and outgoing direction of 54 * @brief Retry count for reading CONNACK from network. 58 * receive for CONNACK will be retried MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT 59 * times before timing out. A value of 0 for this config will cause the 60 * transport receive for CONNACK to be invoked only once. [all …]
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgent_ResumeSession/
H D	README.md	4 This directory contains a memory safety proof for MQTTAgent_ResumeSession. 15 For this proof, stubs are used for the implementation of functions in the following interfaces and 16 function types. Since the implementation for these functions will be provided by the applications, 24 …In addition to the interfaces and the function types, stubs are used for the below listed function… 25 CBMC proofs are written for these functions separately. 42 * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proo… 43 * Use Makefile.arpa as the starting point for your proof Makefile by:
H D	Makefile	`7 # This should be a unique identifier for this proof, and will appear on the 13 # for proving the memory safety and making the proofs run faster. 16 # Bound for loop unwinding for the loops trying to read and write into the 19 # array size for the proofs. 22 # The maximum value for packet identifier for the packets to be filled in the 24 # finding a matching packet for query from MQTT_PublishToResend API.`
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgent_ProcessLoop/
H D	README.md	4 This directory contains a memory safety proof for MQTTAgent_ProcessLoop. 14 For this proof, stubs are used for the implementation of functions in the following interfaces and 15 function types. Since the implementation for these functions will be provided by the applications, 33 * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proo… 34 * Use Makefile.arpa as the starting point for your proof Makefile by:
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgent_Publish/
H D	README.md	4 This directory contains a memory safety proof for MQTTAgent_Publish. 14 For this proof, stubs are used for the implementation of functions in the following interfaces and 15 function types. Since the implementation for these functions will be provided by the applications, 33 * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proo… 34 * Use Makefile.arpa as the starting point for your proof Makefile by:
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgent_Connect/
H D	README.md	4 This directory contains a memory safety proof for MQTTAgent_Connect. 13 For this proof, stubs are used for the implementation of functions in the following interfaces and 14 function types. Since the implementation for these functions will be provided by the applications, 32 * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proo… 33 * Use Makefile.arpa as the starting point for your proof Makefile by:
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgent_Unsubscribe/
H D	README.md	4 This directory contains a memory safety proof for MQTTAgent_Unsubscribe. 14 For this proof, stubs are used for the implementation of functions in the following interfaces and 15 function types. Since the implementation for these functions will be provided by the applications, 33 * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proo… 34 * Use Makefile.arpa as the starting point for your proof Makefile by:
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgent_Terminate/
H D	README.md	4 This directory contains a memory safety proof for MQTTAgent_Terminate. 13 For this proof, stubs are used for the implementation of functions in the following interfaces and 14 function types. Since the implementation for these functions will be provided by the applications, 32 * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proo… 33 * Use Makefile.arpa as the starting point for your proof Makefile by:
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgent_Subscribe/
H D	README.md	4 This directory contains a memory safety proof for MQTTAgent_Subscribe. 14 For this proof, stubs are used for the implementation of functions in the following interfaces and 15 function types. Since the implementation for these functions will be provided by the applications, 33 * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proo… 34 * Use Makefile.arpa as the starting point for your proof Makefile by:
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgent_Ping/
H D	README.md	4 This directory contains a memory safety proof for MQTTAgent_Ping. 14 For this proof, stubs are used for the implementation of functions in the following interfaces and 15 function types. Since the implementation for these functions will be provided by the applications, 33 * Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proo… 34 * Use Makefile.arpa as the starting point for your proof Makefile by:
/CoreMQTT-Agent-v1.1.0/source/include/
H D	core_mqtt_agent.h	17 * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR 18 * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER 25 * @brief Functions for running a coreMQTT client in a dedicated thread. 44 * @brief The maximum number of pending acknowledgments to track for a single 61 * not using any CPU time) for a command to arrive in its command queue before 79 * @brief A type of command for interacting with the MQTT API. 105 uint8_t * pSubackCodes; /*< Array of SUBACK statuses, for a SUBSCRIBE command. / 110 * @brief Struct containing context for a specific command. 147 …MQTTAgentCommandContext_t * pCmdContext; /*< @brief Context for completion callback. … 152 @brief Information for a pending MQTT ack packet expected by the agent. [all …]
H D	core_mqtt_agent_command_functions.h	17 * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR 18 * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER 25 * @brief Functions for processing an MQTT agent command. 114 * @brief Function prototype for a command. 120 * @param[in] pArgs Arguments for the command. 132 * @brief Function to execute for a NONE command. This function does not call 149 * @brief Function to execute for a PUBLISH command. 153 * - MQTTAgentCommandFuncReturns_t.addAcknowledgment (for QoS > 0) 156 * @param[in] pPublishArg Publish information for MQTT_Publish(). 166 * @brief Function to execute for a SUBSCRIBE command. [all …]
H D	core_mqtt_agent_message_interface.h	17 * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR 18 * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER 63 * @param[in] blockTimeMs Block time to wait for a send. 79 * @param[in] blockTimeMs Block time to wait for a receive. 94 * SUBSCRIBE. The MQTTAgentCommand_t structure must persist for the duration of the command's 98 * Blocked state (so not consuming any CPU time) to wait for a MQTTAgentCommand_t structure to 113 * SUBSCRIBE. The MQTTAgentCommand_t structure must persist for the duration of the command's 128 * @brief Function pointers and contexts used for sending and receiving commands, 129 * and allocating memory for them. 136 MQTTAgentMessageRecv_t recv; /*< Function for the agent to receive a command. /
/CoreMQTT-Agent-v1.1.0/
H D	README.md	3 …MQTT library and reducing implementation overhead (e.g., removing the need for the application to … 7 See memory requirements for this library [here](./docs/doxygen/include/size_table.md). 28 …ions.h](source/include/core_mqtt_agent_command_functions.h). Documentation for these configuration… 30 To provide values for these configuration values, they must be either: 36 In order to use the MQTT Agent library on a platform, you need to supply thread safe functions for … 45 …AgentCommand_t` structure, which is used to hold information and arguments for a command to be exe… 48 Reference implementations for the interface functions can be found in the [reference examples](#ref… 55 …for MQTT topics. The receipt of any incoming PUBLISH packet will result in the invocation of a sin… 61 …he header include path from this repository. The same information is found for coreMQTT from `mqtt… 63 For a CMake example of building the MQTT Agent library with the `mqttAgentFilePaths.cmake` file, re… [all …]
H D	CHANGELOG.md	`1 # Changelog for coreMQTT Agent Library 6 …- [#59](https://github.com/FreeRTOS/coreMQTT-Agent/pull/59) Update doxygen version used for docume… 11 …- [#56](https://github.com/FreeRTOS/coreMQTT-Agent/pull/56) Add header guards for C++ linkage and …`
H D	.gitmodules	`8 [submodule "test/cbmc/aws-templates-for-cbmc-proofs"] 9 path = test/cbmc/aws-templates-for-cbmc-proofs 10 url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git`
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgentCommand_Terminate/
H D	Makefile	`7 # This should be a unique identifier for this proof, and will appear on the 13 # for proving the memory safety and making the proofs run faster. 18 # Bound for loop unwinding for the loops trying to read and write into the 21 # array size for the proofs.`
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/
H D	Makefile-template-defines	`14 # Name of this proof project, displayed in proof reports. For example, 15 # "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots, 16 # this may be overridden on the command-line to Make, for example`
/CoreMQTT-Agent-v1.1.0/tools/coverity/
H D	misra.config	`15 …reason: "Allow inclusion of unused types. Header files for coreMQTT, which are needed by all files… 23 …reason: "Allow unused types. coreMQTT Library headers define types intended for the application's … 31 …reason: "Allow unused macros. coreMQTT Library headers define macros intended for the application'… 35 reason: "Allow nested comments. Documentation blocks contain comments for example code."`
/CoreMQTT-Agent-v1.1.0/test/cbmc/proofs/MQTTAgent_CancelAll/
H D	Makefile	`7 # This should be a unique identifier for this proof, and will appear on the 13 # for proving the memory safety and making the proofs run faster. 18 # Bound for loop unwinding for the loops trying to read and write into the 21 # array size for the proofs.`
/CoreMQTT-Agent-v1.1.0/docs/doxygen/
H D	config.doxyfile	4 # doxygen (www.doxygen.org) for a project. 12 # For lists, items can also be appended using: 20 # This tag specifies the encoding used for all characters in the configuration 21 # file that follow. The default is UTF-8 which is also the encoding used for all 23 # iconv built into libc) for the transcoding. See 24 # https://www.gnu.org/software/libiconv/ for the list of possible encodings. 31 # project for which the documentation is generated. This name is used in the 38 # could be handy for archiving the generated documentation or if some version 44 # for a project that appears at the top of each page and should give viewer a 68 # performance problems for the file system. [all …]
/CoreMQTT-Agent-v1.1.0/test/unit-test/logging/
H D	logging_stack.h	17 * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR 18 * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER 31 /* Include header for logging level macros. / 39 / The macro definition for LIBRARY_LOG_NAME is for Doxygen 50 * Refer to #LOG_METADATA_FORMAT for the complete format of the metadata prefix in 59 #error "Please define LIBRARY_LOG_NAME for the library." 63 * @brief Macro to extract only the file name from file path to use for metadata in 80 * for logging functionality. 141 /* Doxygen documentation of logging interface macro definitions for Doxygen. / 148 This macro is only enabled for #LOG_DEBUG level configuration in this [all …]

12 3 4 5