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       50000 : int main(void) {
      15       50000 :   struct aws_hash_table map;
      16       50000 :   initialize_bounded_aws_hash_table(&map, MAX_TABLE_SIZE);
      17       50000 :   assume(aws_hash_table_is_valid(&map));
      18       50000 : 
      19       50000 :   struct aws_hash_iter iter;
      20       50000 :   mk_valid_aws_hash_iter(&iter, &map);
      21       50000 : 
      22       50000 :   enum aws_hash_iter_status old_status = iter.status;
      23       50000 :   struct store_byte_from_buffer old_byte;
      24       50000 :   save_byte_from_hash_table(&map, &old_byte);
      25       50000 : 
      26       50000 :   aws_hash_iter_next(&iter);
      27       50000 : 
      28       50000 :   sassert(aws_hash_iter_is_valid(&iter));
      29             :   #ifdef __KLEE__
      30             :   if (iter.status == AWS_HASH_ITER_STATUS_DELETE_CALLED)
      31             :        return 0;
      32             :   #else
      33       50000 :   assume(iter.status == AWS_HASH_ITER_STATUS_DONE ||
      34       50000 :          iter.status == AWS_HASH_ITER_STATUS_READY_FOR_USE);
      35       50000 :   #endif
      36       50000 :   sassert(IMPLIES(old_status == AWS_HASH_ITER_STATUS_DONE,
      37       50000 :                   iter.status == AWS_HASH_ITER_STATUS_DONE));
      38       50000 :   sassert(aws_hash_table_is_valid(&map));
      39       50000 :   assert_hash_table_unchanged(&map, &old_byte);
      40       50000 :   return 0;
      41       50000 : }