Skip to content

Commit

Permalink
chore: make CBMC stubs with zero parameters proper declarations (#1107)
Browse files Browse the repository at this point in the history
  • Loading branch information
tautschnig authored Apr 23, 2024
1 parent 85c0873 commit 24da21d
Show file tree
Hide file tree
Showing 5 changed files with 12 additions and 12 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
#include <aws/common/byte_buf.h>
#include <proof_helpers/make_common_data_structures.h>

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));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
16 changes: 8 additions & 8 deletions verification/cbmc/include/proof_helpers/nondet.h
Original file line number Diff line number Diff line change
Expand Up @@ -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);
2 changes: 1 addition & 1 deletion verification/cbmc/sources/make_common_data_structures.c
Original file line number Diff line number Diff line change
Expand Up @@ -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));
}
Expand Down
2 changes: 1 addition & 1 deletion verification/cbmc/stubs/abort_override_assert_false.c
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,6 @@

#include <assert.h>

void abort() {
void abort(void) {
assert(0);
}

0 comments on commit 24da21d

Please sign in to comment.