Updates CBMC-proofs directory structure (#620)

Author: adpaco-aws

.gitmodules

@@ -2,5 +2,5 @@
 	path = aws-encryption-sdk-cpp/tests/test_vectors/aws-encryption-sdk-test-vectors
 	url = https://github.com/awslabs/aws-encryption-sdk-test-vectors.git
 [submodule ".cbmc-batch/aws-c-common"]
-	path = .cbmc-batch/aws-c-common
+	path = verification/cbmc/aws-c-common
 	url = https://github.com/awslabs/aws-c-common.git

.cbmc-batch/.gitignore renamed to verification/cbmc/.gitignore

@@ -22,17 +22,17 @@ fi
 while getopts ":sec" opt; do
     case $opt in
         s ) # Start CBMC Batch Jobs
-            for job in jobs/*/; do
+            for job in proofs/*/; do
                 job=${job%/} #remove trailing slash
                 job=${job#*/} #job name
                 echo "Starting job $job"
                 cbmc-batch \
                     --no-report \
                     --no-coverage \
-                    --wsdir jobs/$job \
+                    --wsdir proofs/$job \
                     --srcdir ../ \
                     --jobprefix $job-local \
-                    --yaml jobs/$job/cbmc-batch.yaml
+                    --yaml proofs/$job/cbmc-batch.yaml
             done
             ;;
         e ) # Check CBMC Batch Job Results
@@ -45,7 +45,7 @@ while getopts ":sec" opt; do
                 make -f $Makefile copy
                 dir=${Makefile#*-} # directory name from copy
                 job=${dir%-local-*-*} # original job name
-                check="$( ./check_result.py $dir jobs/$job/cbmc-batch.yaml )"
+                check="$( ./check_result.py $dir proofs/$job/cbmc-batch.yaml )"
                 echo "$job: $check" >> $result
             done
             ;;

.cbmc-batch/README.md renamed to verification/cbmc/README.md

@@ -14,7 +14,7 @@
  */
 
 #include <stdlib.h>
-#include <../source/header.c>
+#include <../../source/header.c>
 
 static inline void hdr_zeroize_verify(struct aws_cryptosdk_hdr *hdr) {
     // Assume hdr is allocated

.cbmc-batch/aws-c-common renamed to verification/cbmc/aws-c-common

@@ -84,8 +84,8 @@ DEFINES += -DCBMC=1
 # Setup directory aliases
 BASEDIR ?= $(abspath ../../../..)
 SRCDIR ?= $(abspath ./link-farm)
-SDKDIR ?= $(abspath ../../..)
-HELPERDIR ?= $(SDKDIR)/.cbmc-batch
+SDKDIR ?= $(abspath ../../../..)
+HELPERDIR ?= $(SDKDIR)/verification/cbmc
 LINKFARM = $(abspath ./link-farm)
 COMMON_REPO_NAME ?= aws-c-common
 COMMONDIR ?= $(HELPERDIR)/$(COMMON_REPO_NAME)
@@ -170,7 +170,7 @@ harness-symlink: linkfarm-dir
 
 helper-symlinks: linkfarm-dir
 	$(call make_symlink, $(LINKFARM), $(HELPERDIR)/include, helper-inc)
-	$(call make_symlink, $(LINKFARM), $(HELPERDIR)/source, helper-src)
+	$(call make_symlink, $(LINKFARM), $(HELPERDIR)/sources, helper-src)
 	$(call make_symlink, $(LINKFARM), $(HELPERDIR)/stubs, helper-stubs)
 
 
@@ -323,4 +323,4 @@ gitclean: veryclean
 
 .PHONY: setup_dependencies cbmc property coverage report clean veryclean
 
-include $(HELPERDIR)/jobs/Makefile.cbmc_batch
+include $(HELPERDIR)/proofs/Makefile.cbmc_batch