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 : 
      19      150000 :   struct aws_hash_iter iter;
      20      150000 :   mk_valid_aws_hash_iter(&iter, &map);
      21             :   #ifdef __KLEE__
      22             :   if (iter.status == AWS_HASH_ITER_STATUS_DELETE_CALLED)
      23             :        return 0;
      24             :   #else
      25      150000 :   assume(iter.status == AWS_HASH_ITER_STATUS_DONE ||
      26      150000 :          iter.status == AWS_HASH_ITER_STATUS_READY_FOR_USE);
      27      150000 :   #endif
      28      150000 :   enum aws_hash_iter_status old_status = iter.status;
      29      150000 :   struct store_byte_from_buffer old_byte;
      30      150000 :   save_byte_from_hash_table(&map, &old_byte);
      31      150000 : 
      32      150000 :   bool rval = aws_hash_iter_done(&iter);
      33      150000 : 
      34      150000 :   sassert(aws_hash_iter_is_valid(&iter));
      35      150000 :   sassert(rval == (iter.status == AWS_HASH_ITER_STATUS_DONE));
      36      150000 :   sassert(iter.status == old_status);
      37      150000 :   sassert(aws_hash_table_is_valid(&map));
      38      150000 :   assert_hash_table_unchanged(&map, &old_byte);
      39      150000 :   return 0;
      40      150000 : }