Re-enabled unknown pragma warnings, wrapped CPROVER pragmas (#420)

* Re-enabled unknown pragma warnings, wrapped CPROVER pragmas
awslabs · Jun 14, 2019 · 76e2a61 · 76e2a61
1 parent 0e88fcb
commit 76e2a61
Show file tree

Hide file tree

Showing 3 changed files with 51 additions and 25 deletions.
diff --git a/cmake/AwsCFlags.cmake b/cmake/AwsCFlags.cmake
@@ -35,9 +35,7 @@ function(aws_set_common_properties target)
         # /volatile:iso relaxes some implicit memory barriers that MSVC normally applies for volatile accesses
         # Since we want to be compatible with user builds using /volatile:iso, use it for the tests.
         list(APPEND AWS_C_FLAGS /volatile:iso)
-        # Disable unknown pragma warnings
-        list(APPEND AWS_C_FLAGS /wd4068)
-
+
         string(TOUPPER "${CMAKE_BUILD_TYPE}" _CMAKE_BUILD_TYPE)
         if(STATIC_CRT)
             string(REPLACE "/MD" "/MT" _FLAGS "${CMAKE_C_FLAGS_${_CMAKE_BUILD_TYPE}}")
@@ -59,7 +57,7 @@ function(aws_set_common_properties target)
         endif()
 
         # Warning disables always go last to avoid future flags re-enabling them
-        list(APPEND AWS_C_FLAGS -Wno-long-long -Wno-unknown-pragmas)
+        list(APPEND AWS_C_FLAGS -Wno-long-long)
 
         # Avoid exporting symbols we don't intend to export
         list(APPEND AWS_C_FLAGS -fvisibility=hidden)

diff --git a/include/aws/common/byte_buf.h b/include/aws/common/byte_buf.h
@@ -533,8 +533,10 @@ AWS_STATIC_IMPL struct aws_byte_cursor aws_byte_cursor_from_array(const void *co
     return cur;
 }
 
-#pragma CPROVER check push
-#pragma CPROVER check disable "unsigned-overflow"
+#ifdef CBMC
+#    pragma CPROVER check push
+#    pragma CPROVER check disable "unsigned-overflow"
+#endif
 /**
  * If index >= bound, bound > (SIZE_MAX / 2), or index > (SIZE_MAX / 2), returns
  * 0. Otherwise, returns UINTPTR_MAX.  This function is designed to return the correct
@@ -599,7 +601,9 @@ AWS_STATIC_IMPL size_t aws_nospec_mask(size_t index, size_t bound) {
 
     return combined_mask;
 }
-#pragma CPROVER check pop
+#ifdef CBMC
+#    pragma CPROVER check pop
+#endif
 
 /**
  * Tests if the given aws_byte_cursor has at least len bytes remaining. If so,

diff --git a/source/hash_table.c b/source/hash_table.c
@@ -361,10 +361,14 @@ static int s_find_entry1(
      * transitions and the loop will exit (if it hasn't already)
      */
     while (1) {
-#pragma CPROVER check push
-#pragma CPROVER check disable "unsigned-overflow"
+#ifdef CBMC
+#    pragma CPROVER check push
+#    pragma CPROVER check disable "unsigned-overflow"
+#endif
         uint64_t index = (hash_code + probe_idx) & state->mask;
-#pragma CPROVER check pop
+#ifdef CBMC
+#    pragma CPROVER check pop
+#endif
         entry = &state->slots[index];
         if (!entry->hash_code) {
             rv = AWS_ERROR_HASHTBL_ITEM_NOT_FOUND;
@@ -376,10 +380,14 @@ static int s_find_entry1(
             break;
         }
 
-#pragma CPROVER check push
-#pragma CPROVER check disable "unsigned-overflow"
+#ifdef CBMC
+#    pragma CPROVER check push
+#    pragma CPROVER check disable "unsigned-overflow"
+#endif
         uint64_t entry_probe = (index - entry->hash_code) & state->mask;
-#pragma CPROVER check pop
+#ifdef CBMC
+#    pragma CPROVER check pop
+#endif
 
         if (entry_probe < probe_idx) {
             /* We now know that our target entry cannot exist; if it did exist,
@@ -444,16 +452,24 @@ static struct hash_table_entry *s_emplace_item(
     /* Since a valid hash_table has at least one empty element, this loop will always terminate in at most linear time
      */
     while (entry.hash_code != 0) {
-#pragma CPROVER check push
-#pragma CPROVER check disable "unsigned-overflow"
+#ifdef CBMC
+#    pragma CPROVER check push
+#    pragma CPROVER check disable "unsigned-overflow"
+#endif
         size_t index = (size_t)(entry.hash_code + probe_idx) & state->mask;
-#pragma CPROVER check pop
+#ifdef CBMC
+#    pragma CPROVER check pop
+#endif
         struct hash_table_entry *victim = &state->slots[index];
 
-#pragma CPROVER check push
-#pragma CPROVER check disable "unsigned-overflow"
+#ifdef CBMC
+#    pragma CPROVER check push
+#    pragma CPROVER check disable "unsigned-overflow"
+#endif
         size_t victim_probe_idx = (size_t)(index - victim->hash_code) & state->mask;
-#pragma CPROVER check pop
+#ifdef CBMC
+#    pragma CPROVER check pop
+#endif
 
         if (!victim->hash_code || victim_probe_idx < probe_idx) {
             /* The first thing we emplace is the entry itself. A pointer to its location becomes the rval */
@@ -854,10 +870,14 @@ bool aws_hash_iter_done(const struct aws_hash_iter *iter) {
 
 void aws_hash_iter_next(struct aws_hash_iter *iter) {
     AWS_PRECONDITION(aws_hash_iter_is_valid(iter));
-#pragma CPROVER check push
-#pragma CPROVER check disable "unsigned-overflow"
+#ifdef CBMC
+#    pragma CPROVER check push
+#    pragma CPROVER check disable "unsigned-overflow"
+#endif
     s_get_next_element(iter, iter->slot + 1);
-#pragma CPROVER check pop
+#ifdef CBMC
+#    pragma CPROVER check pop
+#endif
     AWS_POSTCONDITION(
         iter->status == AWS_HASH_ITER_STATUS_DONE || iter->status == AWS_HASH_ITER_STATUS_READY_FOR_USE,
         "The status of output aws_hash_iter [iter] must either be DONE or READY_FOR_USE.");
@@ -909,10 +929,14 @@ void aws_hash_iter_delete(struct aws_hash_iter *iter, bool destroy_contents) {
      * underflowing to SIZE_MAX; we have to take care in aws_hash_iter_done to avoid
      * treating this as an end-of-iteration condition.
      */
-#pragma CPROVER check push
-#pragma CPROVER check disable "unsigned-overflow"
+#ifdef CBMC
+#    pragma CPROVER check push
+#    pragma CPROVER check disable "unsigned-overflow"
+#endif
     iter->slot--;
-#pragma CPROVER check pop
+#ifdef CBMC
+#    pragma CPROVER check pop
+#endif
     iter->status = AWS_HASH_ITER_STATUS_DELETE_CALLED;
     AWS_POSTCONDITION(
         iter->status == AWS_HASH_ITER_STATUS_DELETE_CALLED,