Skip to content

Commit 61d5409

Browse files
danielsnfeliperodri
authored andcommitted
suppress undefined checks
1 parent d81f019 commit 61d5409

File tree

3 files changed

+15
-6
lines changed

3 files changed

+15
-6
lines changed

.cbmc-batch/jobs/aws_hash_c_string/aws_hash_c_string_harness.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@
2020
#include <proof_helpers/utils.h>
2121

2222
void aws_hash_c_string_harness() {
23-
const char* str = make_arbitrary_c_str(MAX_STRING_SIZE);
24-
/* This function has no pre or post conditions */
25-
uint64_t rval = aws_hash_c_string(str);
23+
const char *str = make_arbitrary_c_str(MAX_STRING_SIZE);
24+
/* This function has no pre or post conditions */
25+
uint64_t rval = aws_hash_c_string(str);
2626
}

.cbmc-batch/jobs/aws_hash_ptr/aws_hash_ptr_harness.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323
* Runtime: 4.5s
2424
*/
2525
void aws_hash_ptr_harness() {
26-
void* ptr;
27-
/* This function has no pre or post conditions */
28-
uint64_t rval = aws_hash_ptr(ptr);
26+
void *ptr;
27+
/* This function has no pre or post conditions */
28+
uint64_t rval = aws_hash_ptr(ptr);
2929
}

include/aws/common/private/lookup3.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,11 @@ on 1 byte), but shoehorning those bytes into integers efficiently is messy.
5858
#pragma warning(disable:4127) /*Disable "conditional expression is constant" */
5959
#endif /* _MSC_VER */
6060

61+
#ifdef CBMC
62+
# pragma CPROVER check push
63+
# pragma CPROVER check disable "unsigned-overflow"
64+
#endif /* CBMC */
65+
6166
/*
6267
* My best guess at if you are big-endian or little-endian. This may
6368
* need adjustment.
@@ -1017,3 +1022,7 @@ int main()
10171022
#if _MSC_VER
10181023
#pragma warning(pop)
10191024
#endif /* _MSC_VER */
1025+
1026+
#ifdef CBMC
1027+
# pragma CPROVER check pop
1028+
#endif /* CBMC */

0 commit comments

Comments
 (0)