updated test cbmc stubs - SigV4_EncodeURI()

aws · Nov 24, 2023 · 1b383aa · 1b383aa
1 parent 5cb1d6c
commit 1b383aa
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 1 deletion.
diff --git a/test/cbmc/include/sigv4_stubs.h b/test/cbmc/include/sigv4_stubs.h
@@ -50,6 +50,13 @@ SigV4Status_t writeLineToCanonicalRequest( const char * pLine,
  size_t lineLen,
  CanonicalContext_t * pCanonicalContext );
 
+SigV4Status_t SigV4_EncodeURI( const char * pUri,
+ size_t uriLen,
+ char * pCanonicalURI,
+ size_t * canonicalURILen,
+ bool encodeSlash,
+ bool doubleEncodeEquals );
+
 SigV4Status_t generateCanonicalQuery( const char * pQuery,
  size_t queryLen,
  const bool doubleEncodeEqualsInParmsValues,

diff --git a/test/cbmc/proofs/SigV4_GenerateHTTPAuthorization/Makefile b/test/cbmc/proofs/SigV4_GenerateHTTPAuthorization/Makefile
@@ -61,4 +61,4 @@ include ../Makefile-json.common
 
 # Substitution command to pass to sed for patching sigv4.c. The
 # characters " and # must be escaped with backslash.
-SIGV4_SED_EXPR = 1s/^/\#include \"sigv4_stubs.h\" /; s/^static //; s/SigV4Status_t (scanValue|generateCanonicalQuery|generateCanonicalAndSignedHeaders|copyHeaderStringToCanonicalBuffer)\b/&_/
+SIGV4_SED_EXPR = 1s/^/\#include \"sigv4_stubs.h\" /; s/^static //; s/SigV4Status_t (scanValue|SigV4_EncodeURI|generateCanonicalQuery|generateCanonicalAndSignedHeaders|copyHeaderStringToCanonicalBuffer)\b/&_/
diff --git a/test/cbmc/stubs/sigv4_stubs.c b/test/cbmc/stubs/sigv4_stubs.c
@@ -147,6 +147,31 @@ SigV4Status_t writeLineToCanonicalRequest( const char * pLine,
  return ret;
 }
 
+SigV4Status_t SigV4_EncodeURI( const char * pUri,
+ size_t uriLen,
+ char * pCanonicalURI,
+ size_t * canonicalURILen,
+ bool encodeSlash,
+ bool doubleEncodeEquals )
+{
+ SigV4Status_t returnStatus = SigV4Success;
+
+ assert( pUri != NULL );
+ assert( pCanonicalURI != NULL );
+ assert( canonicalURILen != NULL );
+
+ if( nondet_bool() )
+ {
+ returnStatus = SigV4Success;
+ }
+ else
+ {
+ returnStatus = SigV4InsufficientMemory;
+ }
+
+ return returnStatus;
+}
+
 SigV4Status_t generateCanonicalQuery( const char * pQuery,
  size_t queryLen,
  const bool doubleEncodeEqualsInParmsValues,