Remove {r,w}_ok from is_valid_IotResponseHandle

This commit attempts to preserve the functionality of the memory checks
in is_valid_IotResponseHandle until the issue in
diffblue/cbmc#5194 is sorted out. This commit
is needed because is_valid_IotResponseHandle uses the __CPROVER_r_ok and
__CPROVER_w_ok macros, and is_valid_IotResponseHandle itself is used
inside an assume statement, triggering the issue mentioned in that bug.

Author: karkhaz

tools/cbmc/proofs/HTTP/global_state_HTTP.c

@@ -296,21 +296,20 @@ int is_valid_IotResponseHandle(IotHttpsResponseHandle_t pResponseHandle) {
     pResponseHandle->pBodyCur <=  pResponseHandle->pBodyEnd;
   int valid_parserdata =
     pResponseHandle->httpParserInfo.readHeaderParser.data == pResponseHandle;
-  return
-    valid_headers &&
-    valid_header_order &&
-    valid_body &&
-    valid_body_order &&
-    valid_parserdata &&
-    // valid_order and short circuit evaluation prevents integer overflow
-    __CPROVER_r_ok(pResponseHandle->pHeaders,
-		   pResponseHandle->pHeadersEnd - pResponseHandle->pHeaders) &&
-    __CPROVER_w_ok(pResponseHandle->pHeaders,
-		   pResponseHandle->pHeadersEnd - pResponseHandle->pHeaders) &&
-    __CPROVER_r_ok(pResponseHandle->pBody,
-		   pResponseHandle->pBodyEnd - pResponseHandle->pBody) &&
-    __CPROVER_w_ok(pResponseHandle->pBody,
-		   pResponseHandle->pBodyEnd - pResponseHandle->pBody);
+
+  if(!( valid_headers &&
+        valid_header_order &&
+        valid_body &&
+        valid_body_order &&
+        valid_parserdata))
+      return false;
+
+  // Check that these are accessible. This is a workaround until
+  // https://github.com/diffblue/cbmc/issues/5194 is fixed.
+  (void *)(pResponseHandle->pHeaders);
+  (void *)(pResponseHandle->pBody);
+
+  return true;
 }
 
 /****************************************************************
@@ -349,16 +348,18 @@ int is_valid_IotRequestHandle(IotHttpsRequestHandle_t pRequestHandle) {
     pRequestHandle->pBody != NULL;
   int bounded_header_buffer =
     __CPROVER_OBJECT_SIZE(pRequestHandle->pHeaders) < CBMC_MAX_OBJECT_SIZE;
-  return
-    valid_headers &&
-    valid_order &&
-    valid_body &&
-    bounded_header_buffer &&
-    // valid_order and short circuit evaluation prevents integer overflow
-    __CPROVER_r_ok(pRequestHandle->pHeaders,
-		   pRequestHandle->pHeadersEnd - pRequestHandle->pHeaders) &&
-    __CPROVER_w_ok(pRequestHandle->pHeaders,
-		   pRequestHandle->pHeadersEnd - pRequestHandle->pHeaders);
+
+  if(!( valid_headers &&
+        valid_order &&
+        valid_body &&
+        bounded_header_buffer))
+      return false;
+
+  // Check that this is accessible. This is a workaround until
+  // https://github.com/diffblue/cbmc/issues/5194 is fixed.
+  (void *)(pRequestHandle->pHeaders);
+
+  return true;
 }
 
 /****************************************************************