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

Project(s)

Full Search
Definition
Symbol
File Path
History
Type

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

12 3 4 5

/CoreMQTT-Agent-v1.2.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.2.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.2.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.2.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.2.0/test/cbmc/proofs/lib/
H D	summarize.py	`9 ret = [len(item) + 1 for item in data[0]] 10 for row in data[1:]: 11 for idx, item in enumerate(row): 18 for max_length_of_word_in_col in max_length_per_column_list: 26 for row in row_data: 28 for idx, word in enumerate(row): 41 for idx, entry in enumerate(entries): 67 for proof_pipeline in run_dict["pipelines"]: 76 for status, count in count_statuses.items(): 89 for summary in _get_status_and_proof_summaries(run_dict):`
/CoreMQTT-Agent-v1.2.0/source/include/
H D	core_mqtt_agent_default_logging.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 logging macros for the MQTT-Agent 28 * @note This file SHOULD NOT be modified. If custom values are needed for 45 * @brief Macro that is called in the MQTT-Agent library for logging "Error" level 52 * double parentheses to be ISO C89/C90 standard compliant. For a reference 57 * <b>Default value</b>: Error logging is turned off, and no code is generated for calls 65 * @brief Macro that is called in the MQTT-Agent library for logging "Warning" level messages. 71 * double parentheses to be ISO C89/C90 standard compliant. For a reference 76 * <b>Default value</b>: Warning logs are turned off, and no code is generated for calls [all …]
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. 47 * @brief A type of command for interacting with the MQTT API. 73 uint8_t * pSubackCodes; /*< Array of SUBACK statuses, for a SUBSCRIBE command. / 78 * @brief Struct containing context for a specific command. 115 …MQTTAgentCommandContext_t * pCmdContext; /*< @brief Context for completion callback. … 120 @brief Information for a pending MQTT ack packet expected by the agent. 155 …_t agentInterface; /*< Struct of function pointers for agent messaging. / 157 …MQTTAgentIncomingPublishCallback_t pIncomingCallback; /**< Callback to invoke for in… [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_config_defaults.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-Agent library. 28 * @note This file SHOULD NOT be modified. If custom values are needed for 52 /* The macro definition for MQTT_AGENT_DO_NOT_USE_CUSTOM_CONFIG is for Doxygen 70 * @brief The maximum number of pending acknowledgments to track for a single 87 * not using any CPU time) for a command to arrive in its command queue before
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.2.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.2.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.2.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.2.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.2.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.2.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.2.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.2.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 …]
/CoreMQTT-Agent-v1.2.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.2.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.2.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.2.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.2.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 …]

12 3 4 5