Merge pull request #1965 from yanjos-dev/cbmc/prvRequestJob_MQTT

Add CBMC OTA proof for prvRequestJob_MQTT

tools/cbmc/proofs/OTA/prvRequestJob_MQTT/Makefile.json

@@ -0,0 +1,47 @@
+{
+  "ENTRY": "prvRequestJob_MQTT",
+
+  "CBMCFLAGS":
+  [
+    "--unwind 1"
+  ],
+
+  "OBJS":
+  [
+    "$(ENTRY)_harness.goto",
+    "$(FREERTOS)/libraries/freertos_plus/aws/ota/src/mqtt/aws_iot_ota_mqtt.goto",
+    "$(FREERTOS)/libraries/freertos_plus/aws/ota/src/aws_iot_ota_agent.goto",
+    "$(FREERTOS)/libraries/freertos_plus/aws/ota/src/aws_iot_ota_interface.goto",
+    "$(FREERTOS)/libraries/3rdparty/mbedtls/library/base64.goto"
+  ],
+  "DEF":
+  [
+      "_CONSOLE",
+      "_CRT_SECURE_NO_WARNINGS",
+      "__free_rtos__"
+  ],
+
+  "INC":
+  [
+    "$(FREERTOS)/libraries/freertos_plus/aws/ota/src",
+    "$(FREERTOS)/libraries/3rdparty/mbedtls/include",
+    "$(FREERTOS)/libraries/freertos_plus/aws/ota/include",
+    "$(FREERTOS)/libraries/freertos_plus/standard/crypto/include",
+    "$(FREERTOS)/freertos_kernel/include",
+    "$(FREERTOS)/freertos_kernel/portable/MSVC-MingW",
+    "$(FREERTOS)/vendors/pc/boards/windows/aws_demos/config_files",
+    "$(FREERTOS)/vendors/pc/boards/windows/aws_demos/application_code",
+    "$(FREERTOS)/demos/include",
+    "$(FREERTOS)/libraries/3rdparty/tracealyzer_recorder/Include",
+    "$(FREERTOS)/libraries/c_sdk/standard/mqtt/include",
+    "$(FREERTOS)/libraries/c_sdk/standard/common/include",
+    "$(FREERTOS)/libraries/abstractions/platform/include",
+    "$(FREERTOS)/libraries/abstractions/platform/freertos/include",
+    "$(FREERTOS)/libraries/abstractions/secure_sockets/include",
+    "$(FREERTOS)/libraries/c_sdk/standard/common/include/private",
+    "$(FREERTOS)/libraries/3rdparty/tinycbor",
+    "$(FREERTOS)/libraries/c_sdk/standard/https/include",
+    "$(FREERTOS)/libraries/3rdparty/jsmn",
+    "$(FREERTOS)/libraries/c_sdk/standard/mqtt/include/types"
+  ]
+}

tools/cbmc/proofs/OTA/prvRequestJob_MQTT/prvRequestJob_MQTT_harness.c

@@ -0,0 +1,37 @@
+/* Standard includes. */
+#include <stdio.h>
+
+/* prvRequestJob_Mqtt includes. */
+#include "aws_iot_ota_agent.h"          /* OTA_Err_t */
+#include "aws_iot_ota_agent_internal.h" /* OTA_AgentContext_t */
+#include "iot_mqtt_types.h"             /* IotMqttError_t */
+
+IotMqttError_t IotMqtt_TimedPublish(IotMqttConnection_t mqttConnection, const IotMqttPublishInfo_t *pPublishInfo, uint32_t flags, uint32_t timeoutMs)
+{
+  /* We may want to havoc parts of mqttConnection */
+  IotMqttError_t unconstrainedIotMqttError;
+  return unconstrainedIotMqttError;
+}
+
+IotMqttError_t IotMqtt_TimedSubscribe( IotMqttConnection_t mqttConnection,
+                                       const IotMqttSubscription_t * pSubscriptionList,
+                                       size_t subscriptionCount,
+                                       uint32_t flags,
+                                       uint32_t timeoutMs )
+{
+  /* We may want to havoc parts of mqttConnection */
+  IotMqttError_t unconstrainedIotMqttError;
+  return unconstrainedIotMqttError;
+}
+
+/* This is the function signature for the function under test */
+OTA_Err_t prvRequestJob_Mqtt( OTA_AgentContext_t * pxAgentCtx );
+
+void harness() {
+  OTA_AgentContext_t pxAgentCtx;
+  OTA_ConnectionContext_t connContext;
+  pxAgentCtx.pvConnectionContext = nondet_bool() ? &connContext:NULL;
+  __CPROVER_assume(pxAgentCtx.pvConnectionContext != NULL);
+
+  prvRequestJob_Mqtt(&pxAgentCtx);
+}