Line data Source code
1 : #include <aws/common/hash_table.h>
2 : #include <aws/common/private/hash_table_impl.h>
3 :
4 : #include <hash_table_helper.h>
5 : #include <seahorn/seahorn.h>
6 : #include <utils.h>
7 :
8 150000 : int main(void) {
9 150000 : struct aws_hash_table map;
10 150000 : initialize_bounded_aws_hash_table(&map, MAX_TABLE_SIZE);
11 150000 : assume(aws_hash_table_is_valid(&map));
12 150000 : map.p_impl->destroy_key_fn = nd_bool() ? NULL : hash_proof_destroy_noop;
13 150000 : map.p_impl->destroy_value_fn = nd_bool() ? NULL : hash_proof_destroy_noop;
14 150000 :
15 150000 : size_t empty_slot_idx;
16 150000 : assume(aws_hash_table_has_an_empty_slot(&map, &empty_slot_idx));
17 150000 : void *key = nd_voidp();
18 150000 : struct aws_hash_element p_elem;
19 150000 : bool get_p_elem = nd_bool();
20 150000 : bool track_was_present = nd_bool();
21 150000 : int was_present;
22 150000 :
23 150000 : struct hash_table_state old_state = *map.p_impl;
24 150000 :
25 150000 : /* assume the preconditions */
26 150000 : assume(aws_hash_table_is_valid(&map));
27 150000 : assume(AWS_OBJECT_PTR_IS_WRITABLE(&p_elem));
28 150000 : assume(AWS_OBJECT_PTR_IS_WRITABLE(&was_present));
29 150000 :
30 150000 : int rval = aws_hash_table_remove(&map, key, get_p_elem ? &p_elem : NULL,
31 150000 : track_was_present ? &was_present : NULL);
32 150000 : sassert(aws_hash_table_is_valid(&map));
33 150000 : if (rval == AWS_OP_SUCCESS) {
34 0 : if (track_was_present) {
35 0 : sassert(map.p_impl->entry_count == old_state.entry_count - was_present);
36 0 : } else {
37 0 : sassert(map.p_impl->entry_count == old_state.entry_count ||
38 0 : map.p_impl->entry_count == old_state.entry_count - 1);
39 0 : }
40 : #ifdef __SEA_UNINTERP_FN__
41 : if (get_p_elem && track_was_present && was_present == 1) {
42 : sassert(uninterpreted_equals(p_elem.key, key));
43 : }
44 : #endif
45 150000 : } else {
46 150000 : sassert(map.p_impl->entry_count == old_state.entry_count);
47 150000 : }
48 150000 : return 0;
49 150000 : }
|