Update CBMC symlinks and makefile paths. (FreeRTOS#4)

sarenameas · web-flow · commit bc7c2da3343d · 2020-08-27T16:42:09.000-07:00
diff --git a/cbmc/.gitignore b/cbmc/.gitignore
@@ -9,6 +9,7 @@ TAGS-*
 
 # Emitted by Arpa
 arpa_cmake/
+arpa-validation-logs/
 Makefile.arpa
 
 # These files should be overwritten whenever prepare.py runs
diff --git a/cbmc/include/README.md b/cbmc/include/README.md
@@ -1 +1 @@
-../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/include/README.md
+../aws-templates-for-cbmc-proofs/template-for-repository/include/README.md
diff --git a/cbmc/include/http_config.h b/cbmc/include/http_config.h
@@ -22,30 +22,6 @@
 #ifndef HTTP_CONFIG_H
 #define HTTP_CONFIG_H
 
-/**************************************************/
-/******* DO NOT CHANGE the following order ********/
-/**************************************************/
-
-/* Include logging header files and define logging macros in the following order:
- * 1. Include the header file "logging_levels.h".
- * 2. Define the LIBRARY_LOG_NAME and LIBRARY_LOG_LEVEL macros depending on
- * the logging configuration for HTTP.
- * 3. Include the header file "logging_stack.h", if logging is enabled for HTTP.
- */
-
-#include "logging_levels.h"
-
-/* Logging configuration for the HTTP library. */
-#ifndef LIBRARY_LOG_NAME
-    #define LIBRARY_LOG_NAME    "HTTP"
-#endif
-
-#ifndef LIBRARY_LOG_LEVEL
-    #define LIBRARY_LOG_LEVEL    LOG_NONE
-#endif
-
-#include "logging_stack.h"
-
-/************ End of logging configuration ****************/
+/* Empty configuration header simply for compilation. */
 
 #endif /* ifndef HTTP_CONFIG_H */
diff --git a/cbmc/proofs/HTTPClient_AddHeader/Makefile b/cbmc/proofs/HTTPClient_AddHeader/Makefile
@@ -43,9 +43,9 @@ REMOVE_FUNCTION_BODY += memcpy
 UNWINDSET += strncmp.0:5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c 
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/stubs/memcpy.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/stubs/memcpy.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/HTTPClient_AddHeader/cbmc-viewer.json b/cbmc/proofs/HTTPClient_AddHeader/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "HTTPClient_AddHeader",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/HTTPClient_AddRangeHeader/Makefile b/cbmc/proofs/HTTPClient_AddRangeHeader/Makefile
@@ -32,8 +32,8 @@ UNWINDSET += __CPROVER_file_local_http_client_c_convertInt32ToAscii.0:11
 UNWINDSET += __CPROVER_file_local_http_client_c_convertInt32ToAscii.1:11
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/HTTPClient_AddRangeHeader/cbmc-viewer.json b/cbmc/proofs/HTTPClient_AddRangeHeader/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "HTTPClient_AddRangeHeader",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/HTTPClient_InitializeRequestHeaders/Makefile b/cbmc/proofs/HTTPClient_InitializeRequestHeaders/Makefile
@@ -42,9 +42,9 @@ REMOVE_FUNCTION_BODY += memcpy
 UNWINDSET += strncmp.0:5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/stubs/memcpy.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/stubs/memcpy.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/HTTPClient_InitializeRequestHeaders/cbmc-viewer.json b/cbmc/proofs/HTTPClient_InitializeRequestHeaders/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "HTTPClient_InitializeRequestHeaders",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/HTTPClient_ReadHeader/Makefile b/cbmc/proofs/HTTPClient_ReadHeader/Makefile
@@ -38,10 +38,10 @@ REMOVE_FUNCTION_BODY += http_parser_settings_init
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/stubs/HTTPClient_ReadHeader_http_parser_execute.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/stubs/HTTPClient_ReadHeader_http_parser_execute.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 
 include ../Makefile.common
diff --git a/cbmc/proofs/HTTPClient_ReadHeader/cbmc-viewer.json b/cbmc/proofs/HTTPClient_ReadHeader/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "HTTPClient_ReadHeader",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/HTTPClient_Send/Makefile b/cbmc/proofs/HTTPClient_Send/Makefile
@@ -54,10 +54,10 @@ UNWINDSET += __CPROVER_file_local_http_client_c_sendHttpData.0:10
 UNWINDSET += strncmp.0:5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/stubs/HTTPClient_Send_http_parser_execute.c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/stubs/transport_interface_stubs.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/stubs/HTTPClient_Send_http_parser_execute.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/stubs/transport_interface_stubs.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/HTTPClient_Send/cbmc-viewer.json b/cbmc/proofs/HTTPClient_Send/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "HTTPClient_Send",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/HTTPClient_strerror/Makefile b/cbmc/proofs/HTTPClient_strerror/Makefile
@@ -30,6 +30,6 @@ UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/HTTPClient_strerror/cbmc-viewer.json b/cbmc/proofs/HTTPClient_strerror/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "HTTPClient_strerror",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/Makefile-project-defines b/cbmc/proofs/Makefile-project-defines
@@ -1,33 +1,32 @@
-# -*- mode: makefile -*-
-# The first line sets the emacs major mode to Makefile
-
-################################################################
-# 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 += -fPIC
-COMPILE_FLAGS += -std=gnu90
-
-# Flags to pass to goto-cc for linking (typically those passed to gcc)
-# LINK_FLAGS =
-
-# Preprocessor include paths -I...
-INCLUDES += -I$(SRCDIR)/libraries/standard/http/cbmc/include
-INCLUDES += -I$(SRCDIR)/libraries/standard/http/include
-INCLUDES += -I$(SRCDIR)/libraries/standard/http/src
-INCLUDES += -I$(SRCDIR)/libraries/standard/http/third_party/http_parser
-INCLUDES += -I$(SRCDIR)/demos/logging-stack
-INCLUDES += -I$(SRCDIR)/platform/include
-
-# Preprocessor definitions -D...
-DEFINES += -Dhttp_EXPORTS
-
-# Ensure that all assumptions are sound by checking that "all pointers
-# in pointer primitives are valid or null"
-CHECKFLAGS += --pointer-primitive-check
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+################################################################
+# 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 += -fPIC
+COMPILE_FLAGS += -std=gnu90
+
+# Flags to pass to goto-cc for linking (typically those passed to gcc)
+# LINK_FLAGS =
+
+# Preprocessor include paths -I...
+INCLUDES += -I$(SRCDIR)/cbmc/include
+INCLUDES += -I$(SRCDIR)/source/include
+INCLUDES += -I$(SRCDIR)/source/portable
+INCLUDES += -I$(SRCDIR)/source
+INCLUDES += -I$(SRCDIR)/source/third_party/http_parser
+
+# Preprocessor definitions -D...
+DEFINES += -Dhttp_EXPORTS
+
+# Ensure that all assumptions are sound by checking that "all pointers
+# in pointer primitives are valid or null"
+CHECKFLAGS += --pointer-primitive-check
diff --git a/cbmc/proofs/Makefile-project-targets b/cbmc/proofs/Makefile-project-targets
@@ -1,6 +1,9 @@
 # -*- 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.
diff --git a/cbmc/proofs/Makefile-project-testing b/cbmc/proofs/Makefile-project-testing
@@ -1,6 +1,9 @@
 # -*- 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
diff --git a/cbmc/proofs/Makefile-template-defines b/cbmc/proofs/Makefile-template-defines
@@ -1 +1 @@
-SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../..)
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../..)
diff --git a/cbmc/proofs/Makefile.common b/cbmc/proofs/Makefile.common
@@ -1 +1 @@
-../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common
+../aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common
diff --git a/cbmc/proofs/README.md b/cbmc/proofs/README.md
@@ -1 +1 @@
-../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md
+../aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md
diff --git a/cbmc/proofs/findHeaderFieldParserCallback/Makefile b/cbmc/proofs/findHeaderFieldParserCallback/Makefile
@@ -15,8 +15,8 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET += strncmp.0:$(MAX_HEADER_FIELD_LENGTH)
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/findHeaderFieldParserCallback/cbmc-viewer.json b/cbmc/proofs/findHeaderFieldParserCallback/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "findHeaderFieldParserCallback",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/findHeaderOnHeaderCompleteCallback/Makefile b/cbmc/proofs/findHeaderOnHeaderCompleteCallback/Makefile
@@ -11,8 +11,8 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/findHeaderOnHeaderCompleteCallback/cbmc-viewer.json b/cbmc/proofs/findHeaderOnHeaderCompleteCallback/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "findHeaderOnHeaderCompleteCallback",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/findHeaderValueParserCallback/Makefile b/cbmc/proofs/findHeaderValueParserCallback/Makefile
@@ -11,8 +11,8 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/findHeaderValueParserCallback/cbmc-viewer.json b/cbmc/proofs/findHeaderValueParserCallback/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "findHeaderValueParserCallback",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/httpParserOnBodyCallback/Makefile b/cbmc/proofs/httpParserOnBodyCallback/Makefile
@@ -12,9 +12,9 @@ REMOVE_FUNCTION_BODY += memmove
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/stubs/memmove.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/stubs/memmove.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/httpParserOnBodyCallback/cbmc-viewer.json b/cbmc/proofs/httpParserOnBodyCallback/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "httpParserOnBodyCallback",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/httpParserOnHeaderFieldCallback/Makefile b/cbmc/proofs/httpParserOnHeaderFieldCallback/Makefile
@@ -11,9 +11,9 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/stubs/callback_stubs.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/stubs/callback_stubs.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/httpParserOnHeaderFieldCallback/cbmc-viewer.json b/cbmc/proofs/httpParserOnHeaderFieldCallback/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "httpParserOnHeaderFieldCallback",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/httpParserOnHeaderValueCallback/Makefile b/cbmc/proofs/httpParserOnHeaderValueCallback/Makefile
@@ -11,8 +11,8 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/httpParserOnHeaderValueCallback/cbmc-viewer.json b/cbmc/proofs/httpParserOnHeaderValueCallback/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "httpParserOnHeaderValueCallback",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/httpParserOnHeadersCompleteCallback/Makefile b/cbmc/proofs/httpParserOnHeadersCompleteCallback/Makefile
@@ -11,9 +11,9 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/sources/http_cbmc_state.c
-PROOF_SOURCES += $(SRCDIR)/libraries/standard/http/cbmc/stubs/callback_stubs.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/sources/http_cbmc_state.c
+PROOF_SOURCES += $(SRCDIR)/cbmc/stubs/callback_stubs.c
 
-PROJECT_SOURCES += $(SRCDIR)/libraries/standard/http/src/http_client.c
+PROJECT_SOURCES += $(SRCDIR)/source/http_client.c
 
 include ../Makefile.common
diff --git a/cbmc/proofs/httpParserOnHeadersCompleteCallback/cbmc-viewer.json b/cbmc/proofs/httpParserOnHeadersCompleteCallback/cbmc-viewer.json
@@ -3,5 +3,5 @@
 
   ],
   "proof-name": "httpParserOnHeadersCompleteCallback",
-  "proof-root": "libraries/standard/http/cbmc/proofs"
+  "proof-root": "cbmc/proofs"
 }
diff --git a/cbmc/proofs/httpParserOnMessageBeginCallback/Makefile b/cbmc/proofs/httpParserOnMessageBeginCallback/Makefile
diff --git a/cbmc/proofs/httpParserOnMessageBeginCallback/cbmc-viewer.json b/cbmc/proofs/httpParserOnMessageBeginCallback/cbmc-viewer.json
diff --git a/cbmc/proofs/httpParserOnMessageCompleteCallback/Makefile b/cbmc/proofs/httpParserOnMessageCompleteCallback/Makefile
diff --git a/cbmc/proofs/httpParserOnMessageCompleteCallback/cbmc-viewer.json b/cbmc/proofs/httpParserOnMessageCompleteCallback/cbmc-viewer.json
diff --git a/cbmc/proofs/httpParserOnStatusCallback/Makefile b/cbmc/proofs/httpParserOnStatusCallback/Makefile
diff --git a/cbmc/proofs/httpParserOnStatusCallback/cbmc-viewer.json b/cbmc/proofs/httpParserOnStatusCallback/cbmc-viewer.json
diff --git a/cbmc/proofs/prepare.py b/cbmc/proofs/prepare.py
diff --git a/cbmc/sources/README.md b/cbmc/sources/README.md
diff --git a/cbmc/stubs/README.md b/cbmc/stubs/README.md

Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/include/README.md`
	`1`	`+../aws-templates-for-cbmc-proofs/template-for-repository/include/README.md`
Original file line number	Diff line number	Diff line change
`@@ -3,5 +3,5 @@`
`3`	`3`
`4`	`4`	`],`
`5`	`5`	`"proof-name": "HTTPClient_AddHeader",`
`6`		`- "proof-root": "libraries/standard/http/cbmc/proofs"`
	`6`	`+ "proof-root": "cbmc/proofs"`
`7`	`7`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,5 +3,5 @@`
`3`	`3`
`4`	`4`	`],`
`5`	`5`	`"proof-name": "HTTPClient_AddRangeHeader",`
`6`		`- "proof-root": "libraries/standard/http/cbmc/proofs"`
	`6`	`+ "proof-root": "cbmc/proofs"`
`7`	`7`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,5 +3,5 @@`
`3`	`3`
`4`	`4`	`],`
`5`	`5`	`"proof-name": "HTTPClient_InitializeRequestHeaders",`
`6`		`- "proof-root": "libraries/standard/http/cbmc/proofs"`
	`6`	`+ "proof-root": "cbmc/proofs"`
`7`	`7`	`}`