1 /** 2 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. 3 * SPDX-License-Identifier: Apache-2.0. 4 */ 5 6 #include <aws/common/hash_table.h> 7 #include <aws/common/private/hash_table_impl.h> 8 #include <proof_helpers/make_common_data_structures.h> 9 #include <proof_helpers/utils.h> 10 aws_hash_iter_delete_harness()11void aws_hash_iter_delete_harness() { 12 struct aws_hash_table map; 13 14 ensure_allocated_hash_table(&map, MAX_TABLE_SIZE); 15 __CPROVER_assume(aws_hash_table_is_valid(&map)); 16 __CPROVER_assume(map.p_impl->destroy_key_fn == hash_proof_destroy_noop || !map.p_impl->destroy_key_fn); 17 __CPROVER_assume(map.p_impl->destroy_value_fn == hash_proof_destroy_noop || !map.p_impl->destroy_value_fn); 18 19 size_t empty_slot_idx; 20 __CPROVER_assume(aws_hash_table_has_an_empty_slot(&map, &empty_slot_idx)); 21 22 struct hash_table_state *state = map.p_impl; 23 24 struct aws_hash_iter iter; 25 iter.map = ↦ 26 __CPROVER_assume(aws_hash_iter_is_valid(&iter)); 27 __CPROVER_assume(iter.status == AWS_HASH_ITER_STATUS_READY_FOR_USE); 28 29 aws_hash_iter_delete(&iter, nondet_bool()); 30 assert(aws_hash_iter_is_valid(&iter)); 31 assert(iter.status == AWS_HASH_ITER_STATUS_DELETE_CALLED); 32 } 33