Update CBMC starter kit (#753)

* ci(cbmc): Update CBMC starter kit to v2.5

* ci(cbmc): Remove starter-kit and Litani submodules

* ci(cbmc): Update README to include a section on CBMC

Author: angelonakos

.gitmodules

@@ -4,12 +4,6 @@
 [submodule ".cbmc-batch/aws-c-common"]
 	path = verification/cbmc/aws-c-common
 	url = https://github.com/awslabs/aws-c-common.git
-[submodule "verification/cbmc/templates"]
-	path = verification/cbmc/templates
-	url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git
-[submodule "verification/litani"]
-	path = verification/litani
-	url = https://github.com/awslabs/aws-build-accumulator
 [submodule "aws-encryption-sdk-specification"]
 	path = aws-encryption-sdk-specification
 	url = https://github.com/awslabs/aws-encryption-sdk-specification.git

README.md

@@ -197,6 +197,14 @@ logic by setting `-DBUILD_AWS_ENC_SDK_CPP=OFF` to never build the C++ components
 by setting `-DBUILD_AWS_ENC_SDK_CPP=ON` to require building the C++ components (and
 fail if the C++ dependencies are not found.)
 
+## CBMC
+
+To learn more about CBMC and proofs specifically, review the training material [here](https://model-checking.github.io/cbmc-training).
+
+The `verification/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).
+
 ## License
 
 This library is licensed under the Apache 2.0 License.

verification/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.

verification/cbmc/include/README.md

@@ -6,7 +6,7 @@ SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..)
 
 # Absolute path to the litani script.
 #
-LITANI ?= $(abspath $(PROOF_ROOT)/../../litani/litani)
+LITANI ?= litani
 
 
 # Name of this proof project, displayed in proof reports. For example,