Merge CBMC-proof branch with main

.github/CONTRIBUTING.md

@@ -26,6 +26,10 @@ Contributions via pull requests are much appreciated. Before sending us a pull r
 1. You are working against the latest source on the *main* branch.
 2. You check existing open, and recently merged, pull requests to make sure someone else hasn't addressed the problem already.
 3. You open an issue to discuss any significant work - we would hate for your time to be wasted.
+4. The size of the PR is small. If the issue requires sizeable code change, you can go with the following:
+    * Break down the PR into independent components(that do not break the library functionality) and create separate PRs.
+    * Else, break down the changes into smaller commits and ensure you have a descriptive commit message.
+    * Provide a helpful description of the change.
 
 To send us a pull request, please:
 

.github/PULL_REQUEST_TEMPLATE.md

@@ -0,0 +1,17 @@
+<!--- Title -->
+
+Description
+-----------
+<!--- Describe your changes in detail -->
+
+Checklist:
+----------
+<!--- Go over all the following points, and put an `x` in all the boxes that apply. -->
+<!--- If you're unsure about any of these, don't hesitate to ask. We're here to help! -->
+<!--- Please refer to CONTRIBUTING.md for further guidelines -->
+- [ ] I have tested my changes. No regression in existing tests.
+- [ ] My code is formatted using Uncrustify.
+- [ ] I have read and applied the rules stated in CONTRIBUTING.md. 
+
+
+By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

.github/workflows/ci.yml

@@ -7,6 +7,7 @@ on:
     branches:
       - main
       - development
+      - cbmc-proof
   workflow_dispatch:
 
 jobs:
@@ -115,7 +116,9 @@ jobs:
         uses: FreeRTOS/CI-CD-Github-Actions/formatting@main
         with:
           path: ./
-          exclude-dirs: docs
+          exclude-dirs: |
+            docs
+            .github
 
   git-secrets:
     runs-on: ubuntu-latest

.gitmodules

@@ -8,3 +8,11 @@
 	path = test/unit-test/CMock
 	url = https://github.com/ThrowTheSwitch/CMock.git
 	update = none
+[submodule "test/cbmc/aws-templates-for-cbmc-proofs"]
+	path = test/cbmc/aws-templates-for-cbmc-proofs
+	url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git
+	update = none
+[submodule "test/cbmc/litani"]
+	path = test/cbmc/litani
+	url = https://github.com/awslabs/aws-build-accumulator.git
+	update = none

.vscode/settings.json

@@ -0,0 +1,5 @@
+{
+    "files.associations": {
+        "ota_mqtt_private.h": "c"
+    }
+}

README.md

@@ -101,7 +101,7 @@ For pre-generated documentation, please see the documentation linked in the loca
 Note that the latest included version of coreMQTT may differ across repositories.
 ### Generating documentation
 
-The Doxygen references were created using Doxygen version 1.8.20. To generate the
+The Doxygen references were created using Doxygen version 1.9.2. To generate the
 Doxygen pages, please run the following command from the root of this repository:
 
 ```shell

source/ota_http.c

@@ -51,7 +51,7 @@ OtaErr_t initFileTransfer_Http( OtaAgentContext_t * pAgentCtx )
     OtaFileContext_t * fileContext = NULL;
 
     LogDebug( ( "Invoking initFileTransfer_Http" ) );
-    assert( pAgentCtx != NULL && pAgentCtx->pOtaInterface != NULL );
+    assert( ( pAgentCtx != NULL ) && ( pAgentCtx->pOtaInterface != NULL ) && ( pAgentCtx->pOtaInterface->http.init != NULL ) );
 
     /* File context from OTA agent. */
     fileContext = &( pAgentCtx->fileContext );
@@ -85,7 +85,7 @@ OtaErr_t requestDataBlock_Http( OtaAgentContext_t * pAgentCtx )
 
     OtaFileContext_t * fileContext = NULL;
 
-    assert( pAgentCtx != NULL && pAgentCtx->pOtaInterface != NULL );
+    assert( ( pAgentCtx != NULL ) && ( pAgentCtx->pOtaInterface != NULL ) && ( pAgentCtx->pOtaInterface->http.request != NULL ) );
     LogDebug( ( "Invoking requestDataBlock_Http" ) );
 
     fileContext = &( pAgentCtx->fileContext );
@@ -163,7 +163,8 @@ OtaErr_t cleanupData_Http( const OtaAgentContext_t * pAgentCtx )
 {
     OtaHttpStatus_t httpStatus = OtaHttpSuccess;
 
-    assert( pAgentCtx != NULL && pAgentCtx->pOtaInterface != NULL );
+    assert( ( pAgentCtx != NULL ) && ( pAgentCtx->pOtaInterface != NULL ) && ( pAgentCtx->pOtaInterface->http.deinit != NULL ) );
+
     httpStatus = pAgentCtx->pOtaInterface->http.deinit();
 
     /* Reset currBlock. */

test/cbmc/.gitignore

@@ -0,0 +1,24 @@
+# Emitted when running CBMC proofs
+proofs/**/logs
+proofs/**/gotos
+proofs/**/report
+proofs/**/html
+proofs/output
+
+# Emitted by CBMC Viewer
+TAGS-*
+
+# Emitted by Arpa
+arpa_cmake/
+arpa-validation-logs/
+Makefile.arpa
+
+# Emitted by litani
+.ninja_deps
+.ninja_log
+.litani_cache_dir
+
+# These files should be overwritten whenever prepare.py runs
+cbmc-batch.yaml
+
+__pycache__/

test/cbmc/proofs/Makefile-project-defines

@@ -0,0 +1,37 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+################################################################
+# Use this file to give project-specific definitions of the command
+# line arguments to pass to CBMC tools like goto-cc to build the goto
+# binaries and cbmc to do the property and coverage checking.
+#
+# Use this file to override most default definitions of variables in
+# Makefile.common.
+################################################################
+
+# Flags to pass to goto-cc for compilation (typically those passed to gcc -c)
+# COMPILE_FLAGS =
+
+# Flags to pass to goto-cc for linking (typically those passed to gcc)
+# LINK_FLAGS =
+
+# Preprocessor include paths -I...
+# Consider adding
+#     INCLUDES += -I$(CBMC_ROOT)/include
+# You will want to decide what order that comes in relative to the other
+# include directories in your project.
+#
+# INCLUDES =
+
+# Preprocessor definitions -D...
+# DEFINES =
+
+# Path to arpa executable
+# ARPA =
+
+# Flags to pass to cmake for building the project
+# ARPA_CMAKE_FLAGS =

test/cbmc/proofs/Makefile-project-targets

@@ -0,0 +1,10 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+################################################################
+# Use this file to give project-specific targets, including targets
+# that may depend on targets defined in Makefile.common.
+################################################################

test/cbmc/proofs/Makefile-project-testing

@@ -0,0 +1,11 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+################################################################
+# Use this file to define project-specific targets and definitions for
+# unit testing or continuous integration that may depend on targets
+# defined in Makefile.common
+################################################################

test/cbmc/proofs/Makefile-template-defines

@@ -0,0 +1,17 @@
+
+# Absolute path to the root of the source tree.
+#
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../)
+
+# Absolute path to the litani script.
+#
+LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani)
+
+
+# Name of this proof project, displayed in proof reports. For example,
+# "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots,
+# this may be overridden on the command-line to Make, for example
+#
+# 	  make PROJECT_NAME="AWS IoT Over-the-air Update Library" report
+#
+PROJECT_NAME = "AWS IoT Over-the-air Update Library"