1 /*
2  * coreMQTT Agent v1.1.0
3  * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
4  *
5  * Permission is hereby granted, free of charge, to any person obtaining a copy of
6  * this software and associated documentation files (the "Software"), to deal in
7  * the Software without restriction, including without limitation the rights to
8  * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
9  * the Software, and to permit persons to whom the Software is furnished to do so,
10  * subject to the following conditions:
11  *
12  * The above copyright notice and this permission notice shall be included in all
13  * copies or substantial portions of the Software.
14  *
15  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
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
19  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
20  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
21  */
22 
23 /**
24  * @file mqtt_agent_cbmc_state.h
25  * @brief Allocation and assumption utilities for the MQTT Agent library CBMC proofs.
26  */
27 #ifndef MQTT_AGENT_CBMC_STATE_H_
28 #define MQTT_AGENT_CBMC_STATE_H_
29 
30 #include <stdbool.h>
31 
32 /* core_mqtt_agent.h must precede including this header. */
33 
34 /**
35  * @brief Allocate a #MQTTFixedBuffer_t object.
36  *
37  * @param[in] pBuffer #MQTTFixedBuffer_t object information.
38  *
39  * @return NULL or allocated #MQTTFixedBuffer_t memory.
40  */
41 MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pFixedBuffer );
42 
43 /**
44  * @brief Validate a #MQTTFixedBuffer_t object.
45  *
46  * @param[in] pBuffer #MQTTFixedBuffer_t object to validate.
47  *
48  * @return True if the #MQTTFixedBuffer_t object is valid, false otherwise.
49  *
50  * @note A NULL object is a valid object. This is for coverage of the NULL
51  * parameter checks in the function under proof.
52  */
53 bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pFixedBuffer );
54 
55 /**
56  * @brief Allocate a #MQTTAgentContext_t object.
57  *
58  * @param[in] pContext #MQTTAgentContext_t object information.
59  *
60  * @return NULL or allocated #MQTTAgentContext_t memory.
61  */
62 MQTTAgentContext_t * allocateMqttAgentContext( MQTTAgentContext_t * pContext );
63 
64 /**
65  * @brief Validate a #MQTTAgentContext_t object.
66  *
67  * @param[in] pContext #MQTTAgentContext_t object to validate.
68  *
69  * @return True if the #MQTTAgentContext_t object is valid, false otherwise.
70  *
71  * @note A NULL object is a valid object. This is for coverage of the NULL
72  * parameter checks in the function under proof.
73  */
74 bool isValidMqttAgentContext( const MQTTAgentContext_t * pContext );
75 
76 /**
77  * @brief Function to check if the status is a valid status for the MQTT Agent
78  * functions that send a command to the queue. The functions are:
79  *  - MQTTAgent_Connect
80  *  - MQTTAgent_Disconnect
81  *  - MQTTAgent_Subscribe
82  *  - MQTTAgent_Unsubscribe
83  *  - MQTTAgent_Ping
84  *  - MQTTAgent_Publish
85  *  - MQTTAgent_ProcessLoop
86  *  - MQTTAgent_Terminate
87  *
88  * @param[in] mqttStatus MQTT status to check if it is a valid MQTTAgent_Connect
89  * status.
90  *
91  * @return true if an MQTTAgent_Connect status, false otherwise.
92  */
93 bool isAgentSendCommandFunctionStatus( MQTTStatus_t mqttStatus );
94 
95 /**
96  * @brief Allocate a #MQTTAgentConnectArgs_t object.
97  *
98  * @param[in] pConnectArgs #MQTTAgentConnectArgs_t object information.
99  *
100  * @return NULL or allocated #MQTTAgentConnectArgs_t memory.
101  */
102 MQTTAgentConnectArgs_t * allocateConnectArgs( MQTTAgentConnectArgs_t * pConnectArgs );
103 
104 /**
105  * @brief Add Pending ACKs to the MQTTAgentContext.
106  *
107  * @param[in] pContext #MQTTAgentContext_t object to add ACKs.
108  */
109 void addPendingAcks( MQTTAgentContext_t * pContext );
110 
111 /**
112  * @brief Allocate a #MQTTAgentSubscribeArgs_t object.
113  *
114  * @param[in] pSubscribeArgs #MQTTAgentSubscribeArgs_t object information.
115  *
116  * @return NULL or allocated #MQTTAgentSubscribeArgs_t memory.
117  */
118 MQTTAgentSubscribeArgs_t * allocateSubscribeArgs( MQTTAgentSubscribeArgs_t * pSubscribeArgs );
119 
120 #endif /* ifndef MQTT_AGENT_CBMC_STATE_H_ */
121