Line data    Source code

       1             : /**
       2             :  */
       3             : 
       4             : #include <aws/common/hash_table.h>
       5             : #include <aws/common/private/hash_table_impl.h>
       6             : 
       7             : #include <seahorn/seahorn.h>
       8             : 
       9             : #include <config.h>
      10             : #include <hash_table_helper.h>
      11             : #include <proof_allocators.h>
      12             : #include <utils.h>
      13             : 
      14      150000 : int main(void) {
      15      150000 :   struct aws_hash_table map;
      16      150000 :   initialize_bounded_aws_hash_table(&map, MAX_TABLE_SIZE);
      17      150000 :   assume(aws_hash_table_is_valid(&map));
      18      150000 :   assume(map.p_impl->destroy_key_fn == hash_proof_destroy_noop ||
      19      150000 :          map.p_impl->destroy_key_fn == NULL);
      20      150000 :   assume(map.p_impl->destroy_value_fn == hash_proof_destroy_noop ||
      21      150000 :          map.p_impl->destroy_value_fn == NULL);
      22      150000 : 
      23      150000 :   size_t empty_slot_idx;
      24      150000 :   assume(aws_hash_table_has_an_empty_slot(&map, &empty_slot_idx));
      25      150000 : 
      26      150000 :   struct hash_table_state *state = map.p_impl;
      27      150000 : 
      28      150000 :   struct aws_hash_iter iter;
      29      150000 :   mk_valid_aws_hash_iter(&iter, &map);
      30      150000 :   assume(iter.status == AWS_HASH_ITER_STATUS_READY_FOR_USE);
      31      150000 : 
      32      150000 :   aws_hash_iter_delete(&iter, nd_bool());
      33      150000 :   sassert(aws_hash_iter_is_valid(&iter));
      34      150000 :   sassert(iter.status == AWS_HASH_ITER_STATUS_DELETE_CALLED);
      35      150000 :   return 0;
      36      150000 : }