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 : 
      17      150000 :   initialize_bounded_aws_hash_table(&map, MAX_TABLE_SIZE);
      18      150000 :   assume(aws_hash_table_is_valid(&map));
      19      150000 : 
      20      150000 :   struct store_byte_from_buffer old_byte;
      21      150000 :   save_byte_from_hash_table(&map, &old_byte);
      22      150000 : 
      23      150000 :   struct aws_hash_iter iter = aws_hash_iter_begin(&map);
      24      150000 : 
      25      150000 :   sassert(aws_hash_iter_is_valid(&iter));
      26      150000 :   sassert(iter.status == AWS_HASH_ITER_STATUS_DONE ||
      27      150000 :           iter.status == AWS_HASH_ITER_STATUS_READY_FOR_USE);
      28      150000 :   sassert(aws_hash_table_is_valid(&map));
      29      150000 :   assert_hash_table_unchanged(&map, &old_byte);
      30      150000 :   return 0;
      31      150000 : }