File tree Expand file tree Collapse file tree 6 files changed +16
-16
lines changed
Expand file tree Collapse file tree 6 files changed +16
-16
lines changed Original file line number Diff line number Diff line change 6262#define NULL_CHARACTER '\0' /**< A NULL character to help with header validation. */
6363
6464/**
65- * @brief Indicator for function #httpHeaderStrncpy that the pSrc parameter is a
65+ * @brief Indicator for function #httpHeaderCpy that the pSrc parameter is a
6666 * header value.
6767 */
6868#define HTTP_HEADER_STRNCPY_IS_VALUE 0U
6969
7070/**
71- * @brief Indicator for function #httpHeaderStrncpy that the pSrc parameter is a
71+ * @brief Indicator for function #httpHeaderCpy that the pSrc parameter is a
7272 * header field.
7373 */
7474#define HTTP_HEADER_STRNCPY_IS_FIELD 1U
Original file line number Diff line number Diff line change @@ -45,7 +45,7 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMess
4545# because HTTPClient_AddHeader does not use the results of the copy later in the
4646# function.
4747REMOVE_FUNCTION_BODY += strncpy
48- REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderStrncpy
48+ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderCpy
4949
5050# strncmp is used to find if there exists "\r\n\r\n" at the end of the header
5151# buffer. Therefore, we need to unwind strncmp the length of "\r\n\r\n" + 1.
@@ -54,7 +54,7 @@ UNWINDSET += strncmp.0:5
5454PROOF_SOURCES += $(PROOFDIR ) /$(HARNESS_FILE ) .c
5555PROOF_SOURCES += $(SRCDIR ) /test/cbmc/sources/http_cbmc_state.c
5656PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/strncpy.c
57- PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/httpHeaderStrncpy .c
57+ PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/httpHeaderCpy .c
5858
5959PROJECT_SOURCES += $(SRCDIR ) /source/core_http_client.c
6060
Original file line number Diff line number Diff line change @@ -32,7 +32,7 @@ INCLUDES +=
3232# because HTTPClient_AddRangeHeader does not use the results of the copy later
3333# in the function.
3434REMOVE_FUNCTION_BODY += strncpy
35- REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderStrncpy
35+ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderCpy
3636
3737# strncmp is used to find if there exists "\r\n\r\n" at the end of the header
3838# buffer. Therefore, we need to unwind strncmp the length of "\r\n\r\n" + 1.
@@ -44,7 +44,7 @@ UNWINDSET += __CPROVER_file_local_core_http_client_c_convertInt32ToAscii.1:11
4444PROOF_SOURCES += $(PROOFDIR ) /$(HARNESS_FILE ) .c
4545PROOF_SOURCES += $(SRCDIR ) /test/cbmc/sources/http_cbmc_state.c
4646PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/strncpy.c
47- PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/httpHeaderStrncpy .c
47+ PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/httpHeaderCpy .c
4848
4949PROJECT_SOURCES += $(SRCDIR ) /source/core_http_client.c
5050
Original file line number Diff line number Diff line change @@ -44,7 +44,7 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMess
4444# because HTTPClient_InitializeRequestHeaders does not use the results of the
4545# copy later in the function.
4646REMOVE_FUNCTION_BODY += strncpy
47- REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderStrncpy
47+ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderCpy
4848
4949# strncmp is used to find if there exists "\r\n\r\n" at the end of the header
5050# buffer. Therefore, we need to unwind strncmp the length of "\r\n\r\n" + 1.
@@ -53,7 +53,7 @@ UNWINDSET += strncmp.0:5
5353PROOF_SOURCES += $(PROOFDIR ) /$(HARNESS_FILE ) .c
5454PROOF_SOURCES += $(SRCDIR ) /test/cbmc/sources/http_cbmc_state.c
5555PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/strncpy.c
56- PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/httpHeaderStrncpy .c
56+ PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/httpHeaderCpy .c
5757
5858PROJECT_SOURCES += $(SRCDIR ) /source/core_http_client.c
5959
Original file line number Diff line number Diff line change @@ -52,7 +52,7 @@ REMOVE_FUNCTION_BODY += http_parser_settings_init
5252# because all of the functions, in HTTPClient_Send, that would have used the
5353# results of the copy are stubbed out to be proven separately.
5454REMOVE_FUNCTION_BODY += strncpy
55- REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderStrncpy
55+ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderCpy
5656
5757# There is a total of 10 digits in INT32_MAX. These loops are unwound once more
5858# than the total possible iterations in the int32_t to ASCII converation.
@@ -71,7 +71,7 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/HTTPClient_Send_http_parser_execute.c
7171PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/transport_interface_stubs.c
7272PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/get_time_stub.c
7373PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/strncpy.c
74- PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/httpHeaderStrncpy .c
74+ PROOF_SOURCES += $(SRCDIR ) /test/cbmc/stubs/httpHeaderCpy .c
7575
7676PROJECT_SOURCES += $(SRCDIR ) /source/core_http_client.c
7777
Original file line number Diff line number Diff line change 2121 */
2222
2323/**
24- * @file httpHeaderStrncpy .c
25- * @brief Creates a stub for httpHeaderStrncpy so that the proofs for
24+ * @file httpHeaderCpy .c
25+ * @brief Creates a stub for httpHeaderCpy so that the proofs for
2626 * HTTPClient_AddHeader, HTTPClient_AddRangeHeader, and
2727 * HTTPClient_InitializeRequestHeaders run much faster. This stub checks if, for
2828 * the input copy length, the destination and source are valid accessible
3232#include <string.h>
3333#include <stdint.h>
3434
35- void * httpHeaderStrncpy ( char * pDest ,
36- const char * pSrc ,
37- size_t len ,
38- uint8_t isField )
35+ void * httpHeaderCpy ( char * pDest ,
36+ const char * pSrc ,
37+ size_t len ,
38+ uint8_t isField )
3939{
4040 __CPROVER_assert ( __CPROVER_w_ok ( pDest , len ), "write" );
4141 __CPROVER_assert ( __CPROVER_r_ok ( pSrc , len ), "read" );
You can’t perform that action at this time.
0 commit comments