From 24da21d2fc46c6e172496f17aade5683a32b76bb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 Apr 2024 23:17:15 +0200 Subject: [PATCH] chore: make CBMC stubs with zero parameters proper declarations (#1107) --- .../proof_helpers/aws_byte_cursor_read_common.h | 2 +- .../proof_helpers/make_common_data_structures.h | 2 +- verification/cbmc/include/proof_helpers/nondet.h | 16 ++++++++-------- .../cbmc/sources/make_common_data_structures.c | 2 +- .../cbmc/stubs/abort_override_assert_false.c | 2 +- 5 files changed, 12 insertions(+), 12 deletions(-) diff --git a/verification/cbmc/include/proof_helpers/aws_byte_cursor_read_common.h b/verification/cbmc/include/proof_helpers/aws_byte_cursor_read_common.h index ab159dcbd..2ff5b8919 100644 --- a/verification/cbmc/include/proof_helpers/aws_byte_cursor_read_common.h +++ b/verification/cbmc/include/proof_helpers/aws_byte_cursor_read_common.h @@ -6,7 +6,7 @@ #include #include -void aws_byte_cursor_read_common_harness() { +void aws_byte_cursor_read_common_harness(void) { /* parameters */ struct aws_byte_cursor cur; DEST_TYPE *dest = malloc(sizeof(*dest)); diff --git a/verification/cbmc/include/proof_helpers/make_common_data_structures.h b/verification/cbmc/include/proof_helpers/make_common_data_structures.h index dde63ae35..139a9f7f5 100644 --- a/verification/cbmc/include/proof_helpers/make_common_data_structures.h +++ b/verification/cbmc/include/proof_helpers/make_common_data_structures.h @@ -127,7 +127,7 @@ void hash_proof_destroy_noop(void *p); /** * Ensures a valid string is allocated, with as much nondet as possible */ -struct aws_string *ensure_string_is_allocated_nondet_length(); +struct aws_string *ensure_string_is_allocated_nondet_length(void); /** * Ensures a valid string is allocated, with as much nondet as possible, but len < max diff --git a/verification/cbmc/include/proof_helpers/nondet.h b/verification/cbmc/include/proof_helpers/nondet.h index 2fc4ac306..5a960ba3e 100644 --- a/verification/cbmc/include/proof_helpers/nondet.h +++ b/verification/cbmc/include/proof_helpers/nondet.h @@ -12,11 +12,11 @@ /** * Non-determinstic functions used in CBMC proofs */ -bool nondet_bool(); -int nondet_int(); -size_t nondet_size_t(); -uint16_t nondet_uint16_t(); -uint32_t nondet_uint32_t(); -uint64_t nondet_uint64_t(); -uint8_t nondet_uint8_t(); -void *nondet_voidp(); +bool nondet_bool(void); +int nondet_int(void); +size_t nondet_size_t(void); +uint16_t nondet_uint16_t(void); +uint32_t nondet_uint32_t(void); +uint64_t nondet_uint64_t(void); +uint8_t nondet_uint8_t(void); +void *nondet_voidp(void); diff --git a/verification/cbmc/sources/make_common_data_structures.c b/verification/cbmc/sources/make_common_data_structures.c index b2e4ef457..16bfb467d 100644 --- a/verification/cbmc/sources/make_common_data_structures.c +++ b/verification/cbmc/sources/make_common_data_structures.c @@ -189,7 +189,7 @@ bool hash_table_state_has_an_empty_slot(const struct hash_table_state *const sta */ void hash_proof_destroy_noop(void *p) {} -struct aws_string *ensure_string_is_allocated_nondet_length() { +struct aws_string *ensure_string_is_allocated_nondet_length(void) { /* Considers any size up to the maximum possible size for the array [bytes] in aws_string */ return nondet_allocate_string_bounded_length(SIZE_MAX - 1 - sizeof(struct aws_string)); } diff --git a/verification/cbmc/stubs/abort_override_assert_false.c b/verification/cbmc/stubs/abort_override_assert_false.c index 79798c3bc..e3b3a4b8a 100644 --- a/verification/cbmc/stubs/abort_override_assert_false.c +++ b/verification/cbmc/stubs/abort_override_assert_false.c @@ -11,6 +11,6 @@ #include -void abort() { +void abort(void) { assert(0); }