FreeRTOS · paulbartell · Jul 15, 2022 · Jul 14, 2022 · Jul 13, 2022 · Jul 13, 2022
diff --git a/.gitmodules b/.gitmodules
@@ -1,12 +1,6 @@
 [submodule "test/unit-test/CMock"]
 	path = test/unit-test/CMock
 	url = https://github.com/ThrowTheSwitch/CMock
-[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
-[submodule "test/cbmc/litani"]
-	path = test/cbmc/litani
-	url = https://github.com/awslabs/aws-build-accumulator
 [submodule "modules/ThirdParty/Community-Supported-Ports"]
 	path = modules/ThirdParty/Community-Supported-Ports
 	url = https://github.com/FreeRTOS/FreeRTOS-Cellular-Interface-Community-Supported-Ports
diff --git a/README.md b/README.md
@@ -115,6 +115,14 @@ git submodule update --checkout --init --recursive test/unit-test/CMock
 
 1. Run `cd build && ctest` to execute all tests and view the test run summary.
 
+## CBMC
+
+To learn more about CBMC and proofs specifically, review the training material [here](https://model-checking.github.io/cbmc-training).
+
+The `test/cbmc/proofs` directory contains CBMC proofs.
+
+In order to run these proofs you will need to install CBMC and other tools by following the instructions [here](https://model-checking.github.io/cbmc-training/installation.html).
+
 ## Reference examples
 
 Please refer to the demos of the Cellular Interface library [here](https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS-Plus/Demo/FreeRTOS_Cellular_Interface_Windows_Simulator) using FreeRTOS on the Windows simulator platform. These can be used as reference examples for the library API.

diff --git a/test/cbmc/aws-templates-for-cbmc-proofs b/test/cbmc/aws-templates-for-cbmc-proofs
diff --git a/test/cbmc/include/README.md b/test/cbmc/include/README.md
diff --git a/test/cbmc/include/README.md b/test/cbmc/include/README.md
@@ -0,0 +1,6 @@
+CBMC proof include files
+========================
+
+This directory contains include files written for CBMC proof.  It is
+common to write some code to model aspects of the system under test,
+and the header files for this code go here.
diff --git a/test/cbmc/litani b/test/cbmc/litani
diff --git a/test/cbmc/proofs/Makefile-project-defines b/test/cbmc/proofs/Makefile-project-defines
@@ -14,7 +14,7 @@
 COMPILE_FLAGS += -fPIC
 COMPILE_FLAGS += -std=gnu90
 
-LITANI = $(SRCDIR)/test/cbmc/litani/litani
+LITANI ?= litani
 PROJECT_NAME = "FreeRTOS cellular"
 
 # Flags to pass to goto-cc for linking (typically those passed to gcc)

diff --git a/test/cbmc/proofs/Makefile-project-targets b/test/cbmc/proofs/Makefile-project-targets
@@ -2,7 +2,7 @@
 # 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
+# SPDX-License-Identifier: MIT-0
 
 ################################################################
 # Use this file to give project-specific targets, including targets

diff --git a/test/cbmc/proofs/Makefile-project-testing b/test/cbmc/proofs/Makefile-project-testing
@@ -2,7 +2,7 @@
 # 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
+# SPDX-License-Identifier: MIT-0
 
 ################################################################
 # Use this file to define project-specific targets and definitions for

diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common